Alexandre Miquel

According to our database, Alexandre Miquel authored at least 21 papers between 2000 and 2023.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2023

Cut elimination for Zermelo set theory.

Gilles Dowek, Alexandre Miquel

CoRR, 2023

Relative normalization.

Gilles Dowek, Alexandre Miquel

CoRR, 2023

Implicative models of set theory.

Samuele Maschio, Alexandre Miquel

Proceedings of the 39th Conference on the Mathematical Foundations of Programming Semantics, 2023

2020

Implicative algebras: a new foundation for realizability and forcing.

Alexandre Miquel

Math. Struct. Comput. Sci., 2020

2019

Realizability in the Unitary Sphere.

Alejandro Díaz-Caro, Mauricio Guillermo, Alexandre Miquel, Benoît Valiron

Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, 2019

2017

Ordered combinatory algebras and realizability.

Walter Ferrer Santos, Jonas Frey, Mauricio Guillermo, Octavio Malherbe, Alexandre Miquel

Math. Struct. Comput. Sci., 2017

2016

Specifying Peirce's law in classical realizability.

Mauricio Guillermo, Alexandre Miquel

Math. Struct. Comput. Sci., 2016

2011

Existential witness extraction in classical realizability and via a negative translation

Alexandre Miquel

Log. Methods Comput. Sci., 2011

A Survey of Classical Realizability.

Alexandre Miquel

Proceedings of the Typed Lambda Calculi and Applications - 10th International Conference, 2011

Forcing as a Program Transformation.

Alexandre Miquel

Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, 2011

2010

Specifying Imperative ML-Like Programs Using Dynamic Logic.

Séverine Maingaud, Vincent Balat, Richard Bubel, Reiner Hähnle, Alexandre Miquel

Proceedings of the Formal Verification of Object-Oriented Software, 2010

2009

The lambda-calculus with constructors: Syntax, confluence and separation.

Ariel Arbiser, Alexandre Miquel, Alejandro Ríos

J. Funct. Program., 2009

Relating Classical Realizability and Negative Translation for Existential Witness Extraction.

Alexandre Miquel

Proceedings of the Typed Lambda Calculi and Applications, 9th International Conference, 2009

2008

Classical F_omega, orthogonality and symmetric candidates.

Stéphane Lengrand, Alexandre Miquel

Ann. Pure Appl. Log., 2008

2007

Classical Program Extraction in the Calculus of Constructions.

Alexandre Miquel

Proceedings of the Computer Science Logic, 21st International Workshop, 2007

2006

A Lambda-Calculus with Constructors.

Ariel Arbiser, Alexandre Miquel, Alejandro Ríos

Proceedings of the Term Rewriting and Applications, 17th International Conference, 2006

2004

lamda-Z: Zermelo's Set Theory as a PTS with 4 Sorts.

Alexandre Miquel

Proceedings of the Types for Proofs and Programs, International Workshop, 2004

2003

A Strongly Normalising Curry-Howard Correspondence for IZF Set Theory.

Alexandre Miquel

Proceedings of the Computer Science Logic, 17th International Workshop, 2003

2002

The Not So Simple Proof-Irrelevant Model of CC.

Alexandre Miquel, Benjamin Werner

Proceedings of the Types for Proofs and Programs, Second International Workshop, 2002

2001

The Implicit Calculus of Constructions.

Alexandre Miquel

Proceedings of the Typed Lambda Calculi and Applications, 5th International Conference, 2001

2000

A Model for Impredicative Type Systems, Universes, Intersection Types and Subtyping.

Alexandre Miquel

Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science, 2000