Normalization by evaluation with typed abstract syntax
Olivier Danvy, Morten Rhiger, Kristoffer H. Rose · Journal of Functional Programming · 2001
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.