Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2014.72
URN: urn:nbn:de:0030-drops-54921
URL: https://drops.dagstuhl.de/opus/volltexte/2015/5492/
Danvy, Olivier ; Keller, Chantal ; Puech, Matthias
Typeful Normalization by Evaluation
| pdf-format: |
|
Abstract
We present the first typeful implementation of Normalization by Evaluation for the simply typed lambda-calculus with sums and control operators: we guarantee type preservation and eta-long (modulo commuting conversions), beta-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. First, we implement the standard NbE algorithm for the implicational fragment in a typeful way that is correct by construction. We then derive its call-by-value continuation-passing counterpart, that maps a lambda-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.
BibTeX - Entry
@InProceedings{danvy_et_al:LIPIcs:2015:5492,
author = {Olivier Danvy and Chantal Keller and Matthias Puech},
title = {{Typeful Normalization by Evaluation}},
booktitle = {20th International Conference on Types for Proofs and Programs (TYPES 2014)},
pages = {72--88},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-88-0},
ISSN = {1868-8969},
year = {2015},
volume = {39},
editor = {Hugo Herbelin and Pierre Letouzey and Matthieu Sozeau},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2015/5492},
URN = {urn:nbn:de:0030-drops-54921},
doi = {10.4230/LIPIcs.TYPES.2014.72},
annote = {Keywords: Normalization by Evaluation, Generalized Algebraic Data Types, Continuation-Passing Style, partial evaluation}
}
| Keywords: | Normalization by Evaluation, Generalized Algebraic Data Types, Continuation-Passing Style, partial evaluation | |
| Seminar: | 20th International Conference on Types for Proofs and Programs (TYPES 2014) | |
| Issue date: | 2015 | |
| Date of publication: | 12.10.2015 |
