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

Étienne Miquey 1, 2, 3 Hugo Herbelin 2
2 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique, 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.
Type de document :
Pré-publication, Document de travail
2017
Liste complète des métadonnées

Littérature citée [35 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01624839
Contributeur : Étienne Miquey <>
Soumis le : jeudi 26 octobre 2017 - 18:18:03
Dernière modification le : jeudi 11 janvier 2018 - 06:28:03

Fichier

cbncps.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01624839, version 1

Collections

Citation

Étienne Miquey, Hugo Herbelin. Realizability interpretation and normalization of typed call-by-need λ-calculus with control. 2017. 〈hal-01624839〉

Partager

Métriques

Consultations de la notice

61

Téléchargements de fichiers

20