Alexandre Miquel

23 papers A* 3B 3Journal 9Unranked 7
YearRankTypeTitle / Venue / Authors
2023 J jnl
Cut elimination for Zermelo set theory.
CoRR
Gilles Dowek, Alexandre Miquel
2023 B conf
Implicative models of set theory.
MFPS
Samuele Maschio, Alexandre Miquel
2023 J jnl
Relative normalization.
CoRR
Gilles Dowek, Alexandre Miquel
2020 J jnl
Implicative algebras: a new foundation for realizability and forcing.
Math. Struct. Comput. Sci.
Alexandre Miquel
2019 A* conf
Realizability in the Unitary Sphere.
LICS
Alejandro Díaz-Caro, Mauricio Guillermo, Alexandre Miquel, Benoît Valiron
2019 J jnl
Realizability in the Unitary Sphere.
CoRR
Alejandro Díaz-Caro, Mauricio Guillermo, Alexandre Miquel, Benoît Valiron
2018 — ed.
Proceedings Seventh International Workshop on Classical Logic and Computation, CL&C 2018, Oxford (UK), 7th of July 2018.
CL&C
Stefano Berardi, Alexandre Miquel
2017 J jnl
Ordered combinatory algebras and realizability.
Math. Struct. Comput. Sci.
Walter Ferrer Santos, Jonas Frey, Mauricio Guillermo, Octavio Malherbe, Alexandre Miquel
2016 J jnl
Specifying Peirce's law in classical realizability.
Math. Struct. Comput. Sci.
Mauricio Guillermo, Alexandre Miquel
2011 — conf
A Survey of Classical Realizability.
TLCA
Alexandre Miquel
2011 J jnl
Existential witness extraction in classical realizability and via a negative translation
Log. Methods Comput. Sci.
Alexandre Miquel
2011 A* conf
Forcing as a Program Transformation.
LICS
Alexandre Miquel
2010 — conf
Specifying Imperative ML-Like Programs Using Dynamic Logic.
FoVeOOS
Séverine Maingaud, Vincent Balat, Richard Bubel, Reiner Hähnle, Alexandre Miquel
2009 — conf
Relating Classical Realizability and Negative Translation for Existential Witness Extraction.
TLCA
Alexandre Miquel
2009 J jnl
The lambda-calculus with constructors: Syntax, confluence and separation.
J. Funct. Program.
Ariel Arbiser, Alexandre Miquel, Alejandro Ríos
2008 J jnl
Classical F
Ann. Pure Appl. Log.
Stéphane Lengrand, Alexandre Miquel
2007 B conf
Classical Program Extraction in the Calculus of Constructions.
CSL
Alexandre Miquel
2006 — conf
A Lambda-Calculus with Constructors.
RTA
Ariel Arbiser, Alexandre Miquel, Alejandro Ríos
2004 — conf
lamda-Z: Zermelo's Set Theory as a PTS with 4 Sorts.
TYPES
Alexandre Miquel
2003 B conf
A Strongly Normalising Curry-Howard Correspondence for IZF Set Theory.
CSL
Alexandre Miquel
2002 — conf
The Not So Simple Proof-Irrelevant Model of CC.
TYPES
Alexandre Miquel, Benjamin Werner
2001 — conf
The Implicit Calculus of Constructions.
TLCA
Alexandre Miquel
2000 A* conf
A Model for Impredicative Type Systems, Universes, Intersection Types and Subtyping.
LICS
Alexandre Miquel