University of Cambridge > > Logic and Semantics Seminar (Computer Laboratory) > Bidirectional typing is not just an implementation technique

Bidirectional typing is not just an implementation technique

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


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