zbMATH — the first resource for mathematics

Normalization by evaluation for \(\lambda ^{\rightarrow 2}\). (English) Zbl 1122.68393
Kameyama, Yukiyoshi (ed.) et al., Functional and logic programming. 7th international symposium, FLOPS 2004, Nara, Japan, April 7–9, 2004. Proceedings. Berlin: Springer (ISBN 3-540-21402-X/pbk). Lecture Notes in Computer Science 2998, 260-275 (2004).
Summary: We show that the set-theoretic semantics of \(\lambda ^{\rightarrow 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.
For the entire collection see [Zbl 1048.68005].
Reviewer: Reviewer (Berlin)

68N18 Functional programming and lambda calculus
Full Text: DOI