Implementing a normalizer using sized heterogeneous types

Abstract

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.