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

1 GALLINETTE - GALLINETTE
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
Inria de Paris, CNRS - Centre National de la Recherche Scientifique, UPD7 - Université Paris Diderot - Paris 7, PPS - Preuves, Programmes et Systèmes
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 :
Communication dans un congrès
Christel Baier; Ugo Dal Lago. FOSSACS 18 - 21st International Conference on Foundations of Software Science and Computation Structures, Apr 2018, Thessalonique, Greece. Springer, 10803, pp.276-292, LNCS. 〈10.1007/978-3-319-89366-2_15〉

Littérature citée [35 références]

https://hal.inria.fr/hal-01624839
Contributeur : Étienne Miquey <>
Soumis le : vendredi 2 mars 2018 - 16:38:31
Dernière modification le : jeudi 15 novembre 2018 - 20:27:45
Document(s) archivé(s) le : jeudi 31 mai 2018 - 12:44:27

### Citation

Étienne Miquey, Hugo Herbelin. Realizability Interpretation and Normalization of Typed Call-by-Need $λ$-calculus With Control. Christel Baier; Ugo Dal Lago. FOSSACS 18 - 21st International Conference on Foundations of Software Science and Computation Structures, Apr 2018, Thessalonique, Greece. Springer, 10803, pp.276-292, LNCS. 〈10.1007/978-3-319-89366-2_15〉. 〈hal-01624839v2〉

### Métriques

Consultations de la notice

## 264

Téléchargements de fichiers