A Simple Take on Typed Abstract Syntax in Haskell-like Languages

  • Olivier Danvy
  • Morten Rhiger

Abstract

We present a simple way to program typed abstract syntax in a
language following a Hindley-Milner typing discipline, such as Haskell and ML, and we apply it to automate two proofs about normalization functions as embodied in type-directed partial evaluation for the simply typed lambda calculus: normalization functions (1) preserve types and (2) yield long beta-eta normal forms.

Keywords: Type-directed partial evaluation, normalization functions, simply-typed lambda-calculus, higher-order abstract syntax, Haskell.

Published
2000-06-04
How to Cite
Danvy, O., & Rhiger, M. (2000). A Simple Take on Typed Abstract Syntax in Haskell-like Languages. BRICS Report Series, 7(34). https://doi.org/10.7146/brics.v7i34.20169