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

https://hal.inria.fr/hal-01397929
Contributor : Chantal Keller <>
Submitted on : Wednesday, November 16, 2016 - 2:32:18 PM
Last modification on : Saturday, April 14, 2018 - 11:14:02 AM
Long-term archiving on: Thursday, March 16, 2017 - 2:45:24 PM

File

types14.pdf
Files produced by the author(s)

Identifiers

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⟩

Share

Metrics

Record views

180

Files downloads

590