BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Andy Pitts Says 'Type Soundness proofs are two a penny!' but I thi
 nk they're cheaper than that. - Conor Mc Bride
DTSTART:20260416T130000Z
DTEND:20260416T140000Z
UID:TALK246556@talks.cam.ac.uk
CONTACT:Jon Sterling
DESCRIPTION:In this episode of my continuing adventures into metametatheor
 y\, I will show how to reduce type soundness (or "subject reduction") proo
 fs for a considerable class of dependent type theories to their sine qua n
 on: the type correctness of the computation rules.\n\nOn the way\, I'll an
 alyse the flow of information through typing rules\, making an "input/outp
 ut" distinction\, and the not always coincident flow of trust\, making a "
 citizen/subject" distinction. I'll extract from this analysis a "pattern/e
 xpression" distinction for the formulae we write in typing rules and thus 
 deliver a condition sufficient to push through all the structural cases of
  the type soundness proof. The notion of "residuation" which plays such a 
 key role in confluence proofs will be central to this argument\, also.\n\n
 I'll sketch the road map to the typechecker which checks itself!\n
LOCATION:FW26\, Computer Laboratory
END:VEVENT
END:VCALENDAR