PRL Seminars

I will contrast the predicative (or ramified, Nuprl-like) higher-order PROPOSITIONAL logic with the impredicative (Coq-like) propositional calculus. I will relate this to the well-known polymorphic lambda calculus of Girard/Reynolds, and then discuss its extension to predicate logic and type theory.

I may also discuss contructive set theory and its role in providing models for the polymorphic calculus and its foundation role vis a vis type theory.

I hope to also discuss the relationship of foundational concerns to the on-going projects using Nuprl.