6 citations · 6 across the 6 of their papers we have counts for
6 papers
Stateful Realizers for Nonstandard Analysis
Bruno Dinis, Étienne Miquey
In this paper we propose a new approach to realizability interpretations for nonstandard arithmetic. We deal with nonstandard analysis in the context of (semi)intuitionistic realiz…
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 $$λ…
Classical realizability and arithmetical formulæ
Mauricio Guillermo, Étienne Miquey
In this paper we treat the specification problem in classical realizability (as defined in [20]) in the case of arithmetical formulæ. In the continuity of [10] and [11], we charact…