Mechanized semantics

Abstract : The goal of this lecture is to show how modern theorem provers---in this case, the Coq proof assistant---can be used to mechanize the specification of programming languages and their semantics, and to reason over individual programs and over generic program transformations, as typically found in compilers. The topics covered include: operational semantics (small-step, big-step, definitional interpreters); a simple form of denotational semantics; axiomatic semantics and Hoare logic; generation of verification conditions, with application to program proof; compilation to virtual machine code and its proof of correctness; an example of an optimizing program transformation (dead code elimination) and its proof of correctness.
Type de document :
Chapitre d'ouvrage
J. Esparza and B. Spanfelner and O. Grumberg. Logics and languages for reliability and security, 25, IOS Press, pp.195-224, 2010, NATO Science for Peace and Security Series D: Information and Communication Security, 〈10.3233/978-1-60750-100-8-195〉
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00529848
Contributeur : Xavier Leroy <>
Soumis le : mardi 26 octobre 2010 - 17:26:32
Dernière modification le : mardi 17 avril 2018 - 11:30:35
Document(s) archivé(s) le : jeudi 27 janvier 2011 - 03:02:05

Fichiers

notes.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Xavier Leroy. Mechanized semantics. J. Esparza and B. Spanfelner and O. Grumberg. Logics and languages for reliability and security, 25, IOS Press, pp.195-224, 2010, NATO Science for Peace and Security Series D: Information and Communication Security, 〈10.3233/978-1-60750-100-8-195〉. 〈inria-00529848〉

Partager

Métriques

Consultations de la notice

159

Téléchargements de fichiers

169