Journal of Functional Programming

Table of Contents - 2009 - Volume 19, Issue 3-4  

Articles

Implementing a normalizer using sized heterogeneous types

ANDREAS ABELa1*

a1 Institut für Informatik, Ludwig-Maximilians-Universität München, Oettingenstraße 67, D-80538 München, Germany (e-mail: andreas.abel@ifi.lmu.de)

Abstract

In the simply typed λ-calculus, a hereditary substitution replaces a free variable in a normal form r by another normal form s of type a, removing freshly created redexes on the fly. It can be defined by lexicographic induction on a and r, thus giving rise to a structurally recursive normalizer for the simply typed λ-calculus. We implement hereditary substitutions in a functional programming language with sized heterogeneous inductive types $\Fhat$, arriving at an interpreter whose termination can be tracked by the type system of its host programming language.

Footnotes

* This research was supported by the coordination action TYPES (510996) and thematic network Applied Semantics II (IST-2001-38957) of the European Union and the project Cover of the Swedish Foundation of Strategic Research (SSF).