# * Metalevel Programming in Constructive Type Theory *

## by Robert L. Constable

1992

Programming and Mathematical Method (NATO ASI Series F: Computer and Systems Sciences)

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

**bibTex ref: Con92a**

cite link