Impredicative vs Predicative Type Theory
by Robert L. Constable, Mark Bickford, Richard Eaton
2011-2012
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