a1 Institut für Informatik, Ludwig-Maximilians-Universität München, Oettingenstraße 67, D-80538 München, Germany (e-mail: firstname.lastname@example.org)
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 , arriving at an interpreter whose termination can be tracked by the type system of its host programming language.
* 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).