Talk by Ulrik Buchholtz

Short Title: 
Talk by U. Buchholtz
Event Date(s): 
Thursday, 20. September 2018 - 10:15 to 11:30

Room A097, ExWi, Sidlerstrasse 5, 3012 Bern

Dr. Ulrik Buchholtz (TU Darmstadt)

Modal type theories and universes of infinity-categories

In the first part I shall survey some recent developments concerning modal type theories, describing work by Licata, Shulman, and Riley. Part of this is a sequent-calculus with good structural rules that can capture ordered/linear/affine logic, bunched implications, and constructive S4 and other modal calculi in a single framework. In the second part I shall describe some applications of the dependently typed version, including a description of universes of infinity-categories in a spatial type theory. (This part is joint work with Jonathan Weinberger.)