Bidirectional typing is not just an implementation technique

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

• Meven Lennon-Bertrand, University of Cambridge
• Friday 03 February 2023, 14:00-15:00
• SS03, Computer Laboratory.

If you have a question about this talk, please contact Jamie Vicary.

In 2000, Pierce and Turner introduced a new technique to perform type inference for ML-like languages, whose main idea was to carefully understand the local flow of information in typing rules. This technique, which came to be referred to as bidirectional typing, did not come out of a void: similar ideas had appeared independently in other contexts. In particular, bidirectional typing has been a part of the folklore of dependently typed languages implementers since the dawn of time.

But even in that context where it has a long history, bidirectional typing was missing an understanding that would detach from implementations to focus on the type-theoretic structure. Fortunately, such a type-theoretic bidirectional structure turns out to be a very interesting tool when studying (dependent) type systems.

In my talk, I will try and give some of my understanding of bidirectional typing, how it is both rooted in type-checker implementations but is more than just this, and how it can be used to make the infamously painful meta-theory of dependent type systems a bit less painful.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• SS03, Computer Laboratory
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• tcw57’s list
• yk373's list

Note that ex-directory lists are not shown.