INFO3104 : Théorie de la programmation
Theory of programming
- Responsable(s) :
-
- Eric Thierry
- Enseignant(s) :
-
- Daniel Hirschkoff
Niveau
L3 / 1e année
Discipline
Informatique
Public externe (ouverts aux auditeurs de cours)
Informations générales sur le cours : INFO3104
Ce cours présente un ensemble de méthodes permettant de définir mathématiquement ce qu'est un programme, et comment il s'exécute. Une telle approche permet de formuler et prouver des propriétés portant sur le comportement des programmes (absence de bugs, conformité vis-à-vis d'une spécification attendue).
Voici une liste indicative des notions couvertes en cours :
- définitions inductives d'ensemble et de relations ; preuves par induction
- sémantique opérationnelle, sémantique détnotationnelle
- éléments de réécriture : terminaison, confluence, paires critiques, unification du premier ordre
- typage pour un petit langage fonctionnel
- logique de Floyd-Hoare, logique séparante
- preuve formelle à l'aide de l'assistant de preuves Coq
Une familiarité avec OCaml, ou avec un autre langage de programmation fonctionnelle, est utile pour suivre le cours.
2h de cours par semaine, 2h de TD ou de TP sur machine par semaine.
Une partie des TPs consiste en une initiation à l'assistant de preuves Coq. Les autres TPs sont fait en OCaml.
Les horaires du cours et des séances de TD/TP sont à définir.
- G. Winskel, The Formal Semantics of Programming Languages, MIT Press.
Programming Language Foundations, volume 2 de la collection Software Foundations,
https://softwarefoundations.cis.upenn.edu/