Skip to main content
PRL Project

Constructive Univalent Foundations

An NSF EAGER Project


Introduction

We investigate concepts unique to Nuprl's constructive type theory that are playing a critical role in the formalization of homotopy type theory, a proposed theoretical basis for next generation proof assistants.

...more