Table of Contents
LANGAGES ET TRADUCTEURS – Chapitre 0 Jean-François Monin, 2021
Présentation
1 Objectifs
Qu'est-ce qu'un langage Comprendre, fabriquer Compilation, traduction, interprétation Analyses lexicales, syntaxiques Sémantique statique (typage…) Sémantique dynamique
Raisonnement : pratique de Coq
2 Outils
- Théorie des langages : syntaxe, sémantique
- Assistant logiciel à la preuve : Coq Parfait pour définir des langages et raisonner dessus
- Compilation certifiée : pour apprendre et pour l'industrie
3 Équipe pédagogique
- Cours/TP : JF Monin
- TD/TP : Pierre Corbineau et JF Monin
4 Plan général du cours
4.1 Compréhension des outils conceptuels
- arbres de syntaxe abstraite (AST)
- récursion structurelle
- raisonnements par récurrence structurelle
4.2 Initiation à Coq
Coq est un assistant à la preuve (qui fait autorité dans le monde)
- on écrit des définitions dans un langage mathématique et fonctionnel proche de OCaml (mais plus complexe)
- on démontre des théorèmes formules logiques principalement écrites avec l'implication -> et la quantification universelle ∀ preuves assistées par ordinateur
- Les arbres sont fondamentaux
- structures de données (listes, AST, …)
- règles de sémantique
- démonstration d'un théorème = arbre de preuve
- langage fonctionnel "Ocaml ++"
- preuves assistées par ordinateur
4.3 Sémantique formelle de petits langages impératifs
- sémantique fonctionnelle
- sémantique opérationnelle à grand pas
- sémantique opérationnelle à petit pas
4.4 Principes de compilation
- syntaxe, analyse syntaxique : délégué à PF
- compilation certifiée