Meven Lennon-Bertrand: Bidirectional Dependent Types, Bidirectional Elaboration, Bidirectional Conversion
Note the extra-ordinary time & place: Tuesday May 10th 2022 at 15:00 in 3.04.
Abstract: Bidirectional typing is a presentation of type systems which makes explicit the difference, well-known to implementers, between type inference, where the type is unknown and should be guessed, and type checking, where it is known and should be used. While bidirectional ideas appear in almost all type-checkers for dependent types, and despite advocacy by e.g. Conor McBride to make it explicit in pen-and-paper presentations, the literature on type systems remains largely undirected.
In this talk, I will try and give an overview of bidirectional typing in the context of dependent types: how to design a well-behaved bidirectional type system, what it can be used for, and how conversion fits into the landscape.