A Model for Impredicative Type Systems, Universes, Intersection Types and Subtyping. - Alexandre Miquel (LICS, 2000)

The Implicit Calculus of Constructions. - Alexandre Miquel (TLCA, 2001)

The Not So Simple Proof-Irrelevant Model of CC. - Alexandre Miquel; Benjamin Werner (TYPES, 2002)

A Strongly Normalising Curry-Howard Correspondence for IZF Set Theory. - Alexandre Miquel (CSL, 2003)

lamda-Z: Zermelo's Set Theory as a PTS with 4 Sorts. - Alexandre Miquel (TYPES, 2004)

A Lambda-Calculus with Constructors. - Ariel Arbiser; Alexandre Miquel; Alejandro Ríos 001 (RTA, 2006)

Classical Program Extraction in the Calculus of Constructions. - Alexandre Miquel (CSL, 2007)

Classical Fomega, orthogonality and symmetric candidates. - Stéphane Lengrand; Alexandre Miquel (Ann. Pure Appl. Log., 2008)

Relating Classical Realizability and Negative Translation for Existential Witness Extraction. - Alexandre Miquel (TLCA, 2009)

The lambda-calculus with constructors: Syntax, confluence and separation. - Ariel Arbiser; Alexandre Miquel; Alejandro Ríos 001 (J. Funct. Program., 2009)

Specifying Imperative ML-Like Programs Using Dynamic Logic. - Séverine Maingaud; Vincent Balat; Richard Bubel; Reiner Hähnle; Alexandre Miquel (FoVeOOS, 2010)

Forcing as a Program Transformation. - Alexandre Miquel (LICS, 2011)

A Survey of Classical Realizability. - Alexandre Miquel (TLCA, 2011)

Existential witness extraction in classical realizability and via a negative translation - Alexandre Miquel (Log. Methods Comput. Sci., 2011)

Specifying Peirce's law in classical realizability. - Mauricio Guillermo; Alexandre Miquel (Math. Struct. Comput. Sci., 2016)

Ordered combinatory algebras and realizability. - Walter Ferrer Santos; Jonas Frey; Mauricio Guillermo; Octavio Malherbe; Alexandre Miquel (Math. Struct. Comput. Sci., 2017)

Realizability in the Unitary Sphere. - Alejandro Díaz-Caro; Mauricio Guillermo; Alexandre Miquel; Benoît Valiron (LICS, 2019)

Implicative algebras: a new foundation for realizability and forcing. - Alexandre Miquel (Math. Struct. Comput. Sci., 2020)

Implicative models of set theory. - Samuele Maschio; Alexandre Miquel (MFPS, 2023)

Relative normalization. - Gilles Dowek; Alexandre Miquel (CoRR, 2023)

Cut elimination for Zermelo set theory. - Gilles Dowek; Alexandre Miquel (CoRR, 2023)