Normalization by evaluation with typed abstract syntax

Abstract

In higher-order abstract syntax, the variables and bindings of an object language are represented by variables and bindings of a meta-language. Let us consider the simply typed λ-calculus as object language and Haskell as meta-language. For concreteness, we also throw in integers and addition, but only in this section.