Theorem proving support in programming language semantics

Yves Bertot 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : 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.
Type de document :
Rapport
[Research Report] RR-6242, INRIA. 2007, pp.23
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00160309
Contributeur : Rapport de Recherche Inria <>
Soumis le : mardi 10 juillet 2007 - 10:09:17
Dernière modification le : samedi 17 septembre 2016 - 01:36:48
Document(s) archivé(s) le : mardi 21 septembre 2010 - 13:39:08

Fichiers

RR-6242.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00160309, version 2
  • ARXIV : 0707.0926

Collections

Citation

Yves Bertot. Theorem proving support in programming language semantics. [Research Report] RR-6242, INRIA. 2007, pp.23. 〈inria-00160309v2〉

Partager

Métriques

Consultations de
la notice

653

Téléchargements du document

383