Skip to main content
PRL Project

Metalevel Programming in Constructive Type Theory

by Robert L. Constable

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

  • unofficial copies PDF, PS

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