unofficial copies [PDF], [PS]

by Robert L. Constable

Programming and Mathematical Method (NATO ASI Series F: Computer and Systems Sciences), M. Broy (ed.), vol. 88, pp. 45-93, Springer-Verlag, 1992.

**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.