Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [53 references]  Display  Hide  Download
Contributor : Chantal Keller <>
Submitted on : Wednesday, November 16, 2016 - 2:32:18 PM
Last modification on : Thursday, June 18, 2020 - 12:32:05 PM
Document(s) archivé(s) le : Thursday, March 16, 2017 - 2:45:24 PM


Files produced by the author(s)




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/⟩. ⟨hal-01397929⟩



Record views


Files downloads