![[Search]](/static/images/search.gif){kind=small}
![[A-Z Index]](/static/images/az.gif){kind=small}
![[Contact]](/static/images/contact.gif){kind=small}
![[University of Cambridge]](/static/images/identifier2.gif){kind=small}
![[Talks.cam]](/static/images/talkslogosmall.gif)
Conor Mc Bride
Thursday 16 April 2026, 14:00-15:00
Andy Pitts Says 'Type Soundness proofs are two a penny!' but I think they're cheaper than that.
- đ¤ Speaker: Conor Mc Bride
- đ Date & Time: Thursday 16 April 2026, 14:00 - 15:00
- đ Venue: FW26, Computer Laboratory
Abstract
In this episode of my continuing adventures into metametatheory, I will show how to reduce type soundness (or “subject reduction”) proofs for a considerable class of dependent type theories to their sine qua non: the type correctness of the computation rules.
On the way, I’ll analyse the flow of information through typing rules, making an “input/output” distinction, and the not always coincident flow of trust, making a “citizen/subject” distinction. I’ll extract from this analysis a “pattern/expression” 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.
I’ll sketch the road map to the typechecker which checks itself!
Series This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.
Included in Lists
- All Talks (aka the CURE list)
- bld31
- Cambridge talks
- Computing and Mathematics
- Department of Computer Science and Technology talks and seminars
- FW26, Computer Laboratory
- Interested Talks
- Logic and Semantics Seminar (Computer Laboratory)
- Martin's interesting talks
- School of Technology
- tcw57âs list
- Trust & Technology Initiative - interesting events
- yk373's list
- yk449
Note: Ex-directory lists are not shown.