Skip to Main content Skip to Navigation
Conference papers

Realizability Interpretation and Normalization of Typed Call-by-Need λ-calculus With Control

Étienne Miquey 1, 2 Hugo Herbelin 2
1 GALLINETTE - Gallinette : vers une nouvelle génération d'assistant à la preuve
Inria Rennes – Bretagne Atlantique , LS2N - Laboratoire des Sciences du Numérique de Nantes
2 PI.R2 - Design, study and implementation of languages for proofs and programs
UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique, IRIF (UMR_8243) - Institut de Recherche en Informatique Fondamentale, Inria de Paris
Abstract : 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 λ-calculus with control due to Ariola et al. Indeed, in such call-by-need calculus, substitutions have to be delayed until knowing if an argument is really needed. In a second step, we extend the proof to a call-by-need λ-calculus equipped with a type system equivalent to classical second-order predicate logic, representing one step towards proving the normalization of the call-by-need classical second-order arithmetic introduced by the second author to provide a proof-as-program interpretation of the axiom of dependent choice.
Document type :
Conference papers
Complete list of metadata

Cited literature [35 references]  Display  Hide  Download
Contributor : Étienne Miquey Connect in order to contact the contributor
Submitted on : Friday, March 2, 2018 - 4:38:31 PM
Last modification on : Friday, January 21, 2022 - 3:20:15 AM
Long-term archiving on: : Thursday, May 31, 2018 - 12:44:27 PM



Étienne Miquey, Hugo Herbelin. Realizability Interpretation and Normalization of Typed Call-by-Need λ-calculus With Control. FOSSACS 18 - 21st International Conference on Foundations of Software Science and Computation Structures, Apr 2018, Thessalonique, Greece. pp.276-292, ⟨10.1007/978-3-319-89366-2_15⟩. ⟨hal-01624839v2⟩



Les métriques sont temporairement indisponibles