Accès: La soutenance a eu lieu le mercredi 9 décembre à 10h dans les locaux de l'antenne parisienne de l'INRIA Paris-Rocquencourt (23 avenue d'Italie, Paris 13^e) au 5^e étage, salle verte.

Le mémoire (150 p., version du 27/11/2009)

Les transparents sont ici

La liste des travaux présentés:

• A. Miquel. Classical realizability with forcing and the axiom of countable choice. Manuscript. PDF
• A. Arbiser, A. Ríos, A. Miquel. The lambda-calculus with constructors: syntax, confluence and separation. Journal of Functional Programming (JFP), 19(5), pp. 581-631. 2009. PDF
• A. Miquel. Relating classical realizability and negative translation for existential witness extraction. Typed Lambda Calculi and Applications (TLCA'09), pp. 188-202. 2009. PDF
• S. Lengrand, A. Miquel. Classical F-omega, orthogonality and symmetric candidates. Annals of Pure and Applied Logic (APAL), 153(1-3), pp. 3-20. 2008. PDF
• A. Miquel. Classical program extraction in the calculus of constructions. Computer Science Logic (CSL'07), pp. 313-327. 2007. PDF
• A. Miquel. L'intuitionnisme: où l'on construit une preuve. In Les chemins de la logique (les Dossiers de Pour la Science), pp. 30-36. Octobre 2005. PDF
• A. Miquel. Lambda-Z: Zermelo's set theory as a PTS with 4 sorts. Types for Proofs and Programs (TYPES'04), pp. 232-251. 2004. PDF
• A. Miquel. A strongly normalizing Curry-Howard correspondence for IZF set theory. Computer Science Logic (CSL'03), pp. 441-454. 2003. PDF
• A. Miquel, B. Werner. The not so simple proof-irrelevant model of CC. Types for Proofs and Programs (TYPES'02), pp. 240-258. 2002. PDF