Catalogue des formations

Diplômes intégrant cet élément pédagogique :

• Ingénieur de Polytech Grenoble spécialité Informatique (RICM)

Descriptif

L'objectif de ce cours est double.
1) Une introduction à l'assistant de preuve Coq, qui fait autorité dans le domaine de la vérification notamment pour des compilateurs et OS certifiés.
2) L'étude des concepts mis en œuvre pour compiler des langages de programmation, notamment les principaux formalismes utilises pour définir leur sémantique. La mise en pratique s'effectue en s'appuyant sur Coq.

- Architecture d'un compilateur et phases de compilation
- Logique typée d'ordre supérieur, règles de déduction
- Récurrence structurelle, récurrence sur une relation inductive
- Pratique de l'assistant à la preuve Coq
- Arbres de syntaxe abstraite
- Sémantique informatique

 

The objective of this course is twofold.
1) An introduction to the Coq proof assistant, which is authoritative in the field of verification especially for certified compilers and OS.
2) The study of the concepts underlying the compilation of programming languages, in particular the main formalisms used to define their semantics. The practice is based on Coq.

- Compiler architecture and compilation steps
- higher-order typed logic, deduction rules
- structural induction, induction on an inductive relation
- practice of the Coq proof assistant
- abstract syntax trees
- computational and relational semantic

Pré-requis recommandés

Langages et automates
Connaissance pratique d'au moins un langage de programmation
Analyse syntaxique

 

Automata and Languages
Knowledge of at least one programming language
Parsing

Bibliographie

- B. C. Pierce. Types and Programming Languages, MIT press, 2002

- Software Foundantions, https://softwarefoundations.cis.upenn.edu/index.html

-  A. Aho, R. Sethi, J. Ullman, Compilateurs : Principes, techniques et outils, InterEditions

- W. Waite and

Informations complémentaires

Lieu(x) : Grenoble
Langue(s) : Français