Table of Contents
LANGAGES ET TRADUCTEURS – Chapitre 0 Jean-François Monin & Pierre Corbineau, 2023
Présentation
1 Objectifs
- Qu'est-ce qu'un langage ?
- Langage Humain : construction culturelle conventionnelle
Langage informatique : aussi culturel et conventionnel mais aussi formel/standardisé : ensemble mathématique de suites de caractères admissibles défini par une spécification/norme/description formelle (cf PF)
En LT on utilisera une représentation arborescente.
- Comprendre, fabriquer
- Compilation, traduction, interprétation
- Analyses lexicales, syntaxiques
- Sémantique statique (typage…)
- Sémantique dynamique
Raisonnement : pratique de Rocq
2 Outils
- Théorie des langages : syntaxe, sémantique
- Assistant logiciel à la preuve : Rocq Parfait pour définir des langages et raisonner dessus
- Compilation certifiée : pour apprendre et pour l'industrie
3 Équipe pédagogique
- Cours/TP : Pierre Corbineau
- TD/TP : Pierre Corbineau et Martin Bodin
4 Plan général du cours
4.1 Compréhension des outils conceptuels
- arbres de syntaxe abstraite (AST)
- récursion structurelle: définir des fonctions récursives
- raisonnements par récurrence structurelle
4.2 Initiation à Rocq
Rocq 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