14 citations · 46 across the 8 of their papers we have counts for
4 papers · 1 filter
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…
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…
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…