14 citations · 46 across the 8 of their papers we have counts for
9 papers
Cut elimination for Zermelo set theory
Gilles Dowek, Alexandre Miquel
We show how to express intuitionistic Zermelo set theory in deduction modulo (i.e. by replacing its axioms by rewrite rules) in such a way that the corresponding notion of proof en…
Relative normalization
Gilles Dowek, Alexandre Miquel
G{ö}del's second incompleteness theorem forbids to prove, in a given theory U, the consistency of many theories-in particular, of the theory U itself-as well as it forbids to prove…
Completions of Implicative Assemblies
Alexandre Miquel, Krzysztof Worytkiewicz
We continue our work on implicative assemblies by investigating under which circumstances a subset gives rise to a lex full subcategory o…
Implicative Assemblies
Félix Castro, Alexandre Miquel, Krzysztof Worytkiewicz
Implicative algebras, recently discovered by Miquel, are combinatorial structures unifying classical and intuitionistic realizability as well as forcing. In this paper we introduce…
Implicative algebras II: completeness w.r.t. Set-based triposes
Alexandre Miquel
We prove that all Set-based triposes are implicative triposes.
Realizability in the Unitary Sphere
Alejandro Díaz-Caro, Mauricio Guillermo, Alexandre Miquel +1
In this paper we present a semantics for a linear algebraic lambda-calculus based on realizability. This semantics characterizes a notion of unitarity in the system, answering a lo…
Implicative algebras: a new foundation for realizability and forcing
Alexandre Miquel
We introduce the notion of implicative algebra, a simple algebraic structure intended to factorize the model constructions underlying forcing and realizability (both in intuitionis…
Ordered combinatory algebras and realizability
Walter Ferrer Santos, Jonas Frey, Mauricio Guillermo +2
We consider different classes of combinatory structures related to Krivine realizability. We show, in the precise sense that they give rise to the same class of triposes, that they…
Existential witness extraction in classical realizability and via a negative translation
Alexandre Miquel
We show how to extract existential witnesses from classical proofs using Krivine's classical realizability---where classical proofs are interpreted as lambda-terms with the call/cc…