Abstract

The usual capture-avoiding substitution is closed for well-typed STLC terms but not for the normal forms. However, we can still define a hereditary substitution that keeps beta-reducing the new redexes that appear after the usual substitution. This gives rise to a normalization algorithm, which was first introduced by [Watkins et al.] and later formalized in Agda by [Keller and Altenkirch].

In this talk, I will explain precisely what it means for hereditary substitution to be the “correct” substitution structure on normal forms, using an algebraic point of view. I will also mention how that relates to the correctness of normalization by hereditary substitution, and how that and an “amazing right adjoint” from category theory could help to formalize substitution and normalization in Agda.

[Watkins et al.] A concurrent logical framework: the propositional fragment. (2003) [Keller and Altenkirch] Hereditary substitution for simple types, formalized. (2010)