Publications

Revues internationales

• M. Guillermo, A. Miquel. Specifying Peirce's law in classical realizability. Mathematical Structures in Computer Science. 2014.
• A. Miquel. Existential witness extraction in classical realizability and via a negative translation. Version longue (47 p.) de l'article publié à TLCA'09. In Selected Papers of the Conference: Typed Lambda Calculi and Applications 2009, Special issue of Logical Methods in Computer Science, 2011.
• A. Arbiser, A. Ríos, A. Miquel. The lambda-calculus with constructors: syntax, confluence and separation. In Journal of Functional Programming (JFP) 19(5), pp. 581-631, 2009.
• S. Lengrand, A. Miquel. Classical Fω, orthogonality and symmetric candidates. In Annals of Pure and Applied Logic (APAL) 153(1-3), pp. 3-20, 2008.

Conférences internationales

• A. Miquel. Forcing as a program transformation. In Logic In Computer Science (LICS'11), p. 197-206. 2011.
• S. Maingaud, V. Balat, R. Bubel, R. Hähnle, A. Miquel. Specifying Imperative ML-Programs Using Dynamic Logic. In Formal Verification of Object-Oriented Software (FoVeOOS'10), p. 314-329, 2010.
• A. Miquel. Relating classical realizability and negative translation for existential witness extraction. In Typed Lambda Calculi and Applications (TLCA'09), pp. 188-202, 2009.
• A. Miquel. Classical program extraction in the calculus of constructions. In Computer Science Logic (CSL'07), pp. 313-327, 2007.
• A. Arbiser, A. Ríos, A. Miquel. A lambda-calculus with constructors. In Term Rewriting and Applications (RTA'06), pp. 181-196, 2006.
• A. Miquel. Lambda-Z: Zermelo's set theory as a PTS with 4 sorts. In Types for Proofs and Programs (TYPES'04), pp. 232-251, 2004.
• A. Miquel. A strongly normalizing Curry-Howard correspondence for IZF set theory. In Computer Science Logic (CSL'03), pp. 441-454, 2003.
• A. Miquel, B. Werner. The not so simple proof-irrelevant model of CC. In Types for Proofs and Programs (TYPES'02), pp. 240-258, 2002.
• A. Miquel. The Implicit Calculus of Constructions. In Typed Lambda Calculi and Applications (TLCA'01), pp. 344-359, 2001.
• A. Miquel. A model for impredicative type systems with universes, intersection types and subtyping. In Logic In Computer Science (LICS'00), pp. 18-29. 2000.

Workshop, conférence nationale

• S. Lengrand, A. Miquel. A classical version of system Fω. In Classical Logic and Computation (CL&C'06), satellite workshop of ICALP'06, 2006.
• A. Miquel. Un afficheur générique d'arbres à l'aide de la géométrie hyperbolique. In Journées francophones des langages applicatifs (JFLA'00), pp. 49-62, 2000.

Chapitre de livre

• A. Miquel. The reasonable effectiveness of mathematical proof. Chapitre du livre Anachronismes logiques, à paraître dans la collection Logique, Langage, Sciences, Philosophie, aux Publications de la Sorbonne. Éd.: Myriam Quatrini et Samuel Tronçon, 2010.

Rapports de recherche

• A. Miquel. On Skolemising Zermelo's Set Theory, Rapport de recherche, hal-00425474, 2008.
• G. Faure, A. Miquel. A categorical semantics for the parallel lambda-calculus. Rapport de recherche RR-7063, INRIA, 2009.

Article de vulgarisation

• 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.

Articles soumis (revues internationales)

• A. Miquel. Forcing as a program transformation. Version longue (56 p.) de l'article publié à LICS'11. Soumis à Mathematical Structures in Computer Science (LMCS). 2012.
• G. Dowek, A. Miquel. Cut elimination for Zermelo's set theory. Soumis à Archive for Mathematical Logic.

Thèses

• A. Miquel, Le calcul des constructions implicite: syntaxe et sémantique. Thèse de doctorat (338 p.) Université Paris 7, décembre 2001.
• A. Miquel, De la formalisation des preuves à l'extraction de programmes. Mémoire d'habilitation (150 p.) Université Paris 7, décembre 2009.