Typeful Normalization by Evaluation

Abstract : We present the first typeful implementation of Normalization by Evaluation for the simply typed λ-calculus with sums and control operators: we guarantee type preservation and η-long (modulo commuting conversions), β-normal forms using only Generalized Algebraic Data Types in a general-purpose programming language, here OCaml; and we account for sums and control operators with Continuation-Passing Style. Our presentation takes the form of a typed functional pearl. First, we implement the standard NbE algorithm for the implicational fragment in a typeful way that is correct by construction. We then derive its continuation-passing counterpart, in call-by-value and call-by-name, that maps a λ-term with sums and call/cc into a CPS term in normal form, which we express in a typed, dedicated syntax. Beyond showcasing the expressive power of GADTs, we emphasize that type inference gives a smooth way to re-derive the encodings of the syntax and typing of normal forms in Continuation-Passing Style.
Type de document :
Communication dans un congrès
20th International Conference on Types for Proofs and Programs, TYPES 2014, May 2014, Paris, France. 〈10.4230/LIPIcs.xxx.yyy.p〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01397929
Contributeur : Chantal Keller <>
Soumis le : mercredi 16 novembre 2016 - 14:32:18
Dernière modification le : samedi 14 avril 2018 - 11:14:02
Document(s) archivé(s) le : jeudi 16 mars 2017 - 14:45:24

Fichier

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

Identifiants

Collections

Citation

Olivier Danvy, Chantal Keller, Matthias Puech. Typeful Normalization by Evaluation. 20th International Conference on Types for Proofs and Programs, TYPES 2014, May 2014, Paris, France. 〈10.4230/LIPIcs.xxx.yyy.p〉. 〈hal-01397929〉

Partager

Métriques

Consultations de la notice

158

Téléchargements de fichiers

199