TDs

• CM0
• TD0
• TD1
• TD2
• TD3 et la correction étendue de la preuve du weakening
• TD4 (màj avec corection des typos)
• TD4v2 seconde version du TD4 avec une syntaxe des références plus proche de OCaml (j'avais testé quelque chose que ne marchait pas bien dans le premier).
• TD5

Examens passés

• exam 2022-2023
• partiel 2022-2023 et la correction des deux preuves par induction
• 2nde session 2021-2022
• 1ière session 2021-2022
• 1ière session 2021-2022l et son corrigé

Références

• "Practical Foundations for Programming Languages" par Robert HARPER
• "Formal Semantics of Programming Languages" par Glynn WINSKEL
• "Discrete Mathematics II: Set Theory for Computer Science" par Glynn WINSKEL; chapitres 5 et 6
• "Logic for Computer Science: Foundations of Automatic Theorem Proving" par Jean GALLIER
• "Discrete Structures, Logic, and Computability" par James L.HEIN, chapitres 3 et 4
• "Sets, Logic and Maths for Computing", de David MAKINSON, chapitres 4.6 e 4.7
• "OCaml Programming: Correct + Efficient + Beautiful", de Michael R. Clarkson et. all., chapitres 3.9, 4.1, 6.7, 6.8, 9.3, 9.4, 9.5 et 9.6