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.
|Title of host publication||Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|
|Editors||Yukiyoshi Kameyama, Peter J. Stuckey|
|Number of pages||16|
|ISBN (Electronic)||354021402X, 9783540214021|
|Publication status||Published - 2004|
|Name||Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|