Skip to main content
PRL Project

Impredicative vs Predicative Type Theory

by Robert L. Constable, Mark Bickford, Richard Eaton

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