Semantics for programming languages with Coq encodings: First part: natural semantics

Yves Bertot 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : This course is devised as an introduction to different techniques used in studying programming language semantics. It is inspired from the first chapters of a book written in 1993 by Glynn Winskel, The formal semantics of programming languages, an introduction and published by MIT Press in the series Foundations of Computing. We will present the following aspects: 1. Natural semantics: presenting program execution as a logical system, 2. Proofs by induction: applications to programming languages, 3. Executing semantic specifications, 4. Proofs in semantics. All our work will be illustrated on the study of a very small language, which represents a fragment present in C, Java or C++: the language of assignments and while-loops. The various semantic concept will then be illustrated and implemented in the Coq system.
Type de document :
Cours
Master. France. 2015
Liste complète des métadonnées

https://hal.inria.fr/cel-01130272
Contributeur : Yves Bertot <>
Soumis le : mercredi 11 mars 2015 - 14:56:26
Dernière modification le : jeudi 11 janvier 2018 - 16:48:46
Document(s) archivé(s) le : lundi 17 avril 2017 - 08:50:41

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

  • HAL Id : cel-01130272, version 1

Collections

Citation

Yves Bertot. Semantics for programming languages with Coq encodings: First part: natural semantics. Master. France. 2015. 〈cel-01130272〉

Partager

Métriques

Consultations de la notice

374

Téléchargements de fichiers

287