Implementing a normalizer using sized heterogeneous types

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 Fω, arriving at an interpreter whose termination can be tracked by the type system of its host programming language. © 2009 Copyright Cambridge University Press 2009.