Anupam Das (University of Birmingham) – Fixed points in computational models and fragments of arithmetic

Notes: unusual room.

In the last 20 years there has been a resurgence of interest in fixed points in both mathematical and computational logic. At the interface of both these traditions is the extension of type theories with (co)induction. Similar theories now underlie popular proof assistants such as Coq and Lean. However, until recently, little was known about the expressivity of theories with fixed points: what can they prove? what can they compute? In this talk I will talk about a recent line of work that classifies the expressivity of type theories with fixed points. This talk is based on joint work with Gianluca Curzi.