Abstract

This paper describes a particular version of constructive type theory, a subset of the one underlying the Nuprl proof development system, and it examines its role as a programming environment. Special attention is given to the property of the theory to talk about itself. This reflective capability is the basis for automating proof development and for metalevel programming.