Automatic Transformation from Ecore Metamodels towards Gallina Inductive Types

Abstract : When engineering a language (and its compiler), it is convenient to use widespread and easy-to-use MDE frameworks like Xtext that automatically generate a compiler infrastructure, and even a full-featured IDE. At the same time, a formal workbench such as a proof assistant is helpful to ensure the language specification is sound. Unfortunately, the two technical spaces hardly integrate. In this paper, we propose a transformation from Ecore's metametamodel to Coq's language named Gallina/Vernacular. The structural fragment of Ecore is fully handled. At the cost of not being bijective, our transformation has relaxed constraints over the input metamodel, in comparison to previous state of the art. To validate, we have used the proposed transformation with a complete and representative test suite, as well as a proof-carrying code type checker.
Type de document :
Communication dans un congrès
MODELSWARD 2018, Jan 2018, Santa Cruz, Portugal. 〈10.5220/0006608604880495〉
Liste complète des métadonnées

Littérature citée [19 références]  Voir  Masquer  Télécharger

https://hal.archives-ouvertes.fr/hal-01693939
Contributeur : Jérémy Buisson <>
Soumis le : vendredi 26 janvier 2018 - 16:28:36
Dernière modification le : mercredi 16 mai 2018 - 11:24:04

Fichier

Modelsward2018_Model__Camera_r...
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Jeremy Buisson, Seidali Rehab. Automatic Transformation from Ecore Metamodels towards Gallina Inductive Types. MODELSWARD 2018, Jan 2018, Santa Cruz, Portugal. 〈10.5220/0006608604880495〉. 〈hal-01693939〉

Partager

Métriques

Consultations de la notice

208

Téléchargements de fichiers

59