Examen: 26 mars, 14h30 -- 17h30 salle 1003
Documents autorisés: deux feuilles A4 manuscrites et strictement personelles.
Soutenance projet: 27 mai, 13h00 -- 17h00, salle 2018, bât Sophie Germain Modalité soutenance: exposé oral de ~15min sur le projet (en utilisant votre ordinateur), plus ~5 min de questions.
Project: to share the code with me, use a git repository, either on
moule or github.
Syllabus
All material in slides, except the ones of 13-03-2019, and in particular
Different semantics for lambda
How to define functions as fixed-points (think of fact...)
Kleene fixed point theorem, Knaster-Tarski theorem
Coinductive definition of equivalence for closed recursive types
How to convert inference rules into functions and vice versa
Inference rules for subtyping (sections 21.3 and 21.8 TAPL)
How to use them inductively and coinductively
How to prove that two types are equivalent (i.e. coinduction proof method)