4 papers
Revisiting the duality of computation: an algebraic analysis of classical realizability models
Étienne Miquey
In an impressive series of papers, Krivine showed at the edge of the last decade how classical realizability provides a surprising technique to build models for classical theories.…
A constructive proof of dependent choice in classical arithmetic via memoization
Étienne Miquey
In a recent paper, Herbelin developed dPA, a calculus in which constructive proofs for the axioms of countable and dependent choices could be derived via the memoization of c…
A sequent calculus with dependent types for classical arithmetic
Étienne Miquey
In a recent paper, Herbelin developed a calculus dPA in which constructive proofs for the axioms of countable and dependent choices could be derived via the encoding of a proof…
Realizability Interpretation and Normalization of Typed Call-by-Need -calculus With Control
Étienne Miquey, Hugo Herbelin
We define a variant of realizability where realizers are pairs of a term and a substitution. This variant allows us to prove the normalization of a simply-typed call-by-need $$λ…