BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Type Checking is Proof Reductions in Classical Linear Logic - Aria
 dne Si Suo  (University of Cambridge)
DTSTART:20250602T101500Z
DTEND:20250602T111500Z
UID:TALK232942@talks.cam.ac.uk
CONTACT:Dr Meven Lennon-Bertrand
DESCRIPTION:I will try to convince you type checkers can be seen as logic 
 programs with ‘directions’\, and doing type checking corresponds to do
 ing proof reductions in classical linear logic. This gives us implementati
 ons of type checking algorithms for free\, by writing bidirectional typing
  rules as directional logic programs. Based on joint work with Neel Krishn
 aswami and Vikraman Choudhury.\n\nIf time permits\, I might also tell you 
 a bit about my (preliminary) understanding of transcendental syntax (by Je
 an-Yves Girard) and Existence vs. Essence\, and why it might be useful to 
 think about these things sometimes.\n\n
LOCATION:FW26\, Computer Laboratory
END:VEVENT
END:VCALENDAR