Metalevel Programming in Constructive Type Theory
by Robert L. Constable
Programming and Mathematical Method (NATO ASI Series F: Computer and Systems Sciences)
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