Title

Type theory, in and around computer science

Abstract

This talk concerns my work on type theory, a family of statically typed functional programming languages originally developed as a foundation for mathematics. This tension between "programming language" and "foundation for mathematics" has resulted in type theory's peculiar character, as well as its utility as the foundation for proof assistants like Rocq, Agda, and Lean. This talk has two goals. The first is to introduce type theory itself and gloss my expository work on this front. The second is to touch on the various flavours of type theory my research has explored as well as the uses to which they have been put.

----------------

Everyone is welcome! 

There will be refreshments after the lecture.