Language Definitions as Rewrite Theories

Arusoaie, Andrei; Lucanu, Dorel; Rusu, Vlad; Serbanuta, Traian-Florin; Stefanescu, Andrei; Rosu, Grigore

Document type :

Communication dans un congrès avec actes

Title :

Language Definitions as Rewrite Theories

Author(s) :

Arusoaie, Andrei [Auteur]
Lucanu, Dorel [Auteur]
Department of Computer Science [Lasi]
Rusu, Vlad [Auteur]
Dynamic Reconfigurable Massively Parallel Architectures and Languages [DREAMPAL]
Serbanuta, Traian-Florin [Auteur]
Stefanescu, Andrei [Auteur]
Rosu, Grigore [Auteur]

Conference title :

International Workshop on Rewriting Logic and Application

City :

Grenoble

Country :

France

Start date of the conference :

2014-04-05

Publication date :

2014-02-22

HAL domain(s) :

Informatique [cs]/Systèmes embarqués

English abstract : [en]

K is a formal framework for defining the operational semantics of programming languages. It includes software tools for compiling K language definitions to Maude rewrite theories, for executing programs in the defined ...
Show more >K is a formal framework for defining the operational semantics of programming languages. It includes software tools for compiling K language definitions to Maude rewrite theories, for executing programs in the defined languages based on the Maude rewriting engine, and for analyzing programs by adapting various Maude analysis tools. A recent extension to the K tool suite is an automatic transformation of language definitions that enables the symbolic execution of programs, i.e., the execution of programs with symbolic inputs. In this paper we investigate the theoretical relationships between K language definitions and their translations to Maude, between symbolic extensions of K definitions and their Maude encodings, and how the relations between K definitions and their symbolic extensions are reflected on their respective representations in Maude. These results show, in particular, how analyses performed with Maude tools can be formally lifted up to the original language definitions.Show less >

Language :

Anglais

Peer reviewed article :

Oui

Audience :

Internationale

Popular science :

Non

Comment :

(To appear in Springer LNCS)

Collections :

Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189

Source :

Harvested from HAL

Files

https://hal.inria.fr/hal-00950775/document
Open access
Access the document

https://hal.inria.fr/hal-00950775/document
Open access
Access the document

https://hal.inria.fr/hal-00950775/document
Open access
Access the document

document
Open access
Access the document

wrla2014.pdf
Open access
Access the document

document
Open access
Access the document

wrla2014.pdf
Open access
Access the document

Language Definitions as Rewrite Theories BibTeX CSV Excel RIS

Files

Language Definitions as Rewrite Theories

BibTeX

CSV

Excel

RIS