Theorem proving support in programming language semantics - INRIA - Institut National de Recherche en Informatique et en Automatique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2007

Theorem proving support in programming language semantics

Yves Bertot

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.
Fichier principal
Vignette du fichier
RR-6242.pdf (247.73 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00160309 , version 1 (05-07-2007)
inria-00160309 , version 2 (10-07-2007)

Identifiants

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

Citer

Yves Bertot. Theorem proving support in programming language semantics. [Research Report] RR-6242, INRIA. 2007, pp.23. ⟨inria-00160309v2⟩
685 Consultations
854 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More