Normalization by Evaluation for λ→2

Thorsten Altenkirch*, Tarmo Uustalu

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

12 Citations (Scopus)

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.

Original languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
EditorsYukiyoshi Kameyama, Peter J. Stuckey
PublisherSpringer-Verlag
Pages260-275
Number of pages16
ISBN (Electronic)354021402X, 9783540214021
DOIs
Publication statusPublished - 2004

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2998
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint

Dive into the research topics of 'Normalization by Evaluation for λ→2'. Together they form a unique fingerprint.

Cite this