Realizability interpretation and normalization of typed call-by-need λ-calculus with control - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Pré-Publication, Document De Travail Année : 2017

Realizability interpretation and normalization of typed call-by-need λ-calculus with control

Résumé

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.
Fichier principal
Vignette du fichier
cbncps.pdf (427.73 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01624839 , version 1 (26-10-2017)
hal-01624839 , version 2 (02-03-2018)

Identifiants

  • HAL Id : hal-01624839 , version 1

Citer

Étienne Miquey, Hugo Herbelin. Realizability interpretation and normalization of typed call-by-need λ-calculus with control. 2017. ⟨hal-01624839v1⟩
379 Consultations
249 Téléchargements

Partager

Gmail Facebook X LinkedIn More