inria-00160309, version 2
Theorem proving support in programming language semantics
N° RR-6242 (2007)
Résumé : We describe several views of the semantics of a simple programming language as formal documents in the calculus of inductive constructions that can be verified by the Coq proof system. Covered aspects are natural semantics, denotational semantics, axiomatic semantics, and abstract interpretation. Descriptions as recursive functions are also provided whenever suitable, thus yielding a a verification condition generator and a static analyser that can be run inside the theorem prover for use in reflective proofs. Extraction of an interpreter from the denotational semantics is also described. All different aspects are formally proved sound with respect to the natural semantics specification.
- 1 : MARELLE (INRIA Sophia Antipolis)
- INRIA
- Domaine : Informatique/Logique en informatique
Informatique/Langage de programmation - Mots-clés : Coq – natural semantics – structural operational semantics – denotational semantics – axiomatic semantics – abstract interpretation – formal verification – calculus of inductive constructions – proof by reflection – program extraction
- Référence interne : RR-6242
- Commentaire : Proposé pour publication dans l'ouvrage à la mémoire de Gilles Kahn
- Versions disponibles : v1 (06-07-2007) v2 (10-07-2007)
- inria-00160309, version 2
- http://hal.inria.fr/inria-00160309
- oai:hal.inria.fr:inria-00160309
- Contributeur : Rapport De Recherche Inria
- Soumis le : Mardi 10 Juillet 2007, 10:09:17
- Dernière modification le : Mercredi 15 Octobre 2008, 17:14:28
Documents associés
Exporter