Substitution, Normalization, and Formalization

Add to your list(s) Download to your calendar using vCal

• Yulong Huang (University of Cambridge)
• Monday 02 December 2024, 13:00-14:00
• FS07, Computer Laboratory.

If you have a question about this talk, please contact Dr Meven Lennon-Bertrand.

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)

This talk is part of the SANDWICH Seminar (Computer Laboratory) series.

This talk is included in these lists:

• FS07, Computer Laboratory
• tcw57’s list

Note that ex-directory lists are not shown.