6 citations · 6 across the 6 of their papers we have counts for
Showing 2018Show all
2 papers · 1 filter
cs.LO2018★ 6 cited
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…
cs.LO2018
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 $$λ…