Teaching in 2014-2015

Analyses de Programmes et Vérification des Systèmes

Lectures done by Philippe Audebaud. Exercise session on Fridays, at 10:15, in room B1.

Exercise sheets:

Homework assignments:

Preuves

DM1 (to hand in for October, 7th): Prove Glivenko's theorem in Coq (cf. TD2). Starting point for the homework.

DM2 (to hand in for October, 24th to Colin Riba): Prove Friedman's theorem (questions).

DM3 (to hand in for November, 25th): Omniscience (Coq starting point).

(Optional) DM4 (to hand in for December, 19th): end of previous sheets or the paradox of Girard-Hurkens.