Sémantique opérationnelle et typage

Ce cours est donné à la prépa agreg de Sorbonne Universite.

Supports de cours

Les notes de cours (et la feuille de règles).

Les slides :

1. Sémantique opérationnelle
2. Typage
3. Typage (suite)

Les travaux dirigés :

1. Évaluation et réduction dans le langage IMP
2. Inférence de type et évaluation en mini-ML
3. Types principaux en mini-ML

Bibliographie

Sémantique opérationnelle :

• Glynn Winskel, The Formal Semantics of Programming Languages: An Introduction, The MIT Press, 1993.
• Hanne Riis Nielson, Flemming Nielson, Semantics with Applications, Springer, 2006.
• Samuel Mimram, Program = proof, 2020.

Typage :

• Xavier Leroy, cours Typage et Programmation.
• Benjamin Pierce, Types and Programming Languages, MIT Press, 2002.

Autres supports

• les notes de David Baelde

Liens

• Le moodle
• Les épreuves
• Le site du jury