Metalevel Programming in Constructive Type Theory

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.