Abstract
We show that the set-theoretic semantics of λ→2- simply typed lambda calculus with a boolean type but no type variables-is complete by inverting evaluation using decision trees. This leads to an implementation of normalization by evaluation which is witnessed by the source of part of this paper being a literate Haskell script. We show the correctness of our implementation using logical relations. © Springer-Verlag 2004.
Cite
CITATION STYLE
Altenkirch, T., & Uustalu, T. (2004). Normalization by Evaluation for λ→2. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2998, 260–275. https://doi.org/10.1007/978-3-540-24754-8_19
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
