BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY: Substitution\, Normalization\, and Formalization - Yulong Huang (
 University of Cambridge)
DTSTART:20241202T130000Z
DTEND:20241202T140000Z
UID:TALK224752@talks.cam.ac.uk
CONTACT:Dr Meven Lennon-Bertrand
DESCRIPTION: The usual capture-avoiding substitution is closed for well-ty
 ped STLC terms but not for the normal forms. However\, we can still define
  a hereditary substitution that keeps beta-reducing the new redexes that a
 ppear after the usual substitution. This gives rise to a normalization alg
 orithm\, which was first introduced by [Watkins et al.] and later formaliz
 ed in Agda by [Keller and Altenkirch].\n\nIn this talk\, I will explain pr
 ecisely what it means for hereditary substitution to be the "correct" subs
 titution structure on normal forms\, using an algebraic point of view. I w
 ill also mention how that relates to the correctness of normalization by h
 ereditary substitution\, and how that and an "amazing right adjoint" from 
 category theory could help to formalize substitution and normalization in 
 Agda.\n\n[Watkins et al.] A concurrent logical framework: the propositiona
 l fragment. (2003)\n[Keller and Altenkirch] Hereditary substitution for si
 mple types\, formalized. (2010)
LOCATION:FS07\, Computer Laboratory
END:VEVENT
END:VCALENDAR