University of Cambridge > Talks.cam > SANDWICH Seminar (Computer Laboratory) > Type Checking is Proof Reductions in Classical Linear Logic

  Browse A-Z

Log in

Googledetails Microsoftdetails

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹ️ Information

Type Checking is Proof Reductions in Classical Linear Logic

Download to your calendar using vCal

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:

Note that ex-directory lists are not shown.

Other lists

Seminar Room, Henry Wellcome Building & on Zoom -https://zoom.us/meeting/register/tJAsduigrTwtEtMPh6m9S7OnOef5SaPcSYOn Senior Parlour, Gonville & Caius College Department of Pathology Lecture Theatre

Other talks

LMB Seminar - Mechanisms of mRNA packaging and export Director's Briefing Group Presentation 2 Ensemble inequivalence for systems with long-range interactions The Neurophenomenology of Surrender: Agency, Renewal, and Social Engagement in Speaking in Tongues Title TBC
 

© 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity