BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Confluence of Term Rewriting Systems with Variable Binding - Grego
 r Feierabend (University of Cambridge)
DTSTART:20250602T134500Z
DTEND:20250602T144500Z
UID:TALK232948@talks.cam.ac.uk
CONTACT:Dr Meven Lennon-Bertrand
DESCRIPTION:In this talk\, we will consider a generalised confluence theor
 em in the spirit of Aczel [1] in the context of the model of second-order 
 abstract syntax in the category of presheaves over the category of finite 
 cardinals [2\, 3].\nWe will recall from Fiore et al [2\, 3] that a signatu
 re with variable-binding operators induces a strong term monad\, T\, on th
 is category.\nA rewrite rule\, ρ\, can then be defined to be a pair of te
 rms in T(M)(0) for some presheaf of meta-variables\, M. Every ρ inductive
 ly defines a reduction relation ⤳ ⊆ T(0) × T(0).\nClosely following A
 czel's approach\, we will establish a coherence property for ρ and show t
 hat it yields the confluence of the reduction relation ⤳. As an applicat
 ion\, we will examine the confluence of β-reduction in the λ-calculus.\n
 \n(Joint work with Marcelo Fiore)\n\n[1] P. Aczel\, A General Church–Ros
 ser Theorem. Unpublished note\, 1978.\n[2] M. Fiore\, Second-Order and Dep
 endently-Sorted Abstract Syntax\, In Proceedings of the 23rd Annual ACM/IE
 EE Symposium on Logic in Computer Science (LICS 2008)\, pages 57–68. IEE
 E\nComputer Society\, 2008.\n[3] M. Fiore\, G. Plotkin\, and D. Turi\, Abs
 tract Syntax and Variable Binding\, In Proceedings of the 14th Annual ACM/
 IEEE Symposium on Logic in Computer Science (LICS 1999)\, pages 193–202.
  IEEE Computer Society\, 1999.
LOCATION:FW26\, Computer Laboratory
END:VEVENT
END:VCALENDAR