We will discuss impredicative vs predicative type theory. Bob will give an introduction and Mark will describe some new work he just finished and Rich Eaton is implementing to make it easier to manage the restrictions imposed by predicative theories like the computational type theory (CTT) of Nuprl.
Friday Apr 13 Noon-1:00PM
Meet in Upson 215