Volumes horaires
- CM 15.0
- Projet -
- TD 15.0
- Stage -
- TP -
- DS 2.0
Crédits ECTS
Crédits ECTS 0.4
Objectif(s)
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 oeuvre 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.
Contenu(s)
- 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 abstraits
- sémantiques calculatoires et relationnelles des langages de programmation (sémantique fonctionnelle, sémantique naturelle, sémantique opérationnelle structurelle)
- compilation correcte par construction
Langages et automates
Connaissance pratique d'au moins un langage de programmation
Analyse syntaxique
Contrôle des connaissances
100% évaluation projet :
* Évaluation basée sur les livrables suivants:
**# Compte-rendus de TD intermédiaires
**# Rendu final de projet (par groupe)
**# Entretien individuel d'évaluation
En cas de non validation d’une UE, le jury peut autoriser l’élève ingénieur à passer des épreuves complémentaires pour la valider.
Informations complémentaires
Code de l'enseignement : KAIN7M03
Langue(s) d'enseignement : 
Vous pouvez retrouver ce cours dans la liste de tous les cours.
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 G. Goos, Compiler Construction, Springer Verlag