Language Definitions as Rewrite Theories

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

Type de document :

Communication dans un congrès avec actes

Titre :

Language Definitions as Rewrite Theories

Auteur(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]

Titre de la manifestation scientifique :

International Workshop on Rewriting Logic and Application

Ville :

Grenoble

Pays :

France

Date de début de la manifestation scientifique :

2014-04-05

Date de publication :

2014-02-22

Discipline(s) HAL :

Informatique [cs]/Systèmes embarqués

Résumé en anglais : [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 ...
Lire la suite >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.Lire moins >

Langue :

Anglais

Comité de lecture :

Oui

Audience :

Internationale

Vulgarisation :

Non

Commentaire :

(To appear in Springer LNCS)

Collections :

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

Source :

Harvested from HAL

Fichiers

https://hal.inria.fr/hal-00950775/document
Accès libre
Accéder au document

https://hal.inria.fr/hal-00950775/document
Accès libre
Accéder au document

https://hal.inria.fr/hal-00950775/document
Accès libre
Accéder au document

document
Accès libre
Accéder au document

wrla2014.pdf
Accès libre
Accéder au document

document
Accès libre
Accéder au document

wrla2014.pdf
Accès libre
Accéder au document

Language Definitions as Rewrite Theories BibTeX CSV Excel RIS

Fichiers

Language Definitions as Rewrite Theories

BibTeX

CSV

Excel

RIS