Type Checking is Proof Reductions in Classical Linear Logic

Add to your list(s) Download to your calendar using vCal

• Ariadne Si Suo (University of Cambridge)
• Monday 02 June 2025, 11:15-12:15
• FW26, Computer Laboratory.

If you have a question about this talk, please contact Dr Meven Lennon-Bertrand.

I will try to convince you type checkers can be seen as logic programs with ‘directions’, and doing type checking corresponds to doing proof reductions in classical linear logic. This gives us implementations of type checking algorithms for free, by writing bidirectional typing rules as directional logic programs. Based on joint work with Neel Krishnaswami and Vikraman Choudhury.

If time permits, I might also tell you a bit about my (preliminary) understanding of transcendental syntax (by Jean-Yves Girard) and Existence vs. Essence, and why it might be useful to think about these things sometimes.

This talk is part of the SANDWICH Seminar (Computer Laboratory) series.

This talk is included in these lists:

• FW26, Computer Laboratory
• tcw57’s list

Note that ex-directory lists are not shown.