Reflecting the Open-Ended Computation System of Constructive Type Theory

unofficial copies [PDF], [PS]


by Robert L. Constable, Stuart F. Allen, and Douglas J. Howe

Logic Algebra and Computation (NATO ASI Series), H. Schwichtenberg (ed.), vol. F79, 1990.

Abstract

The computation system of constructive type theory is open-ended so that theorems about computation will hold for a broad class of extensions to the system. We show that despite this openness it is possible to completely reflect the computation system into itself in a clear way by adding simple primitive concepts that anticipate the reflection. This work provides a method to modify the built-in evaluator and to treat the issues of intensionality and computational complexity in programming logics and provides a basis for reflecting the deductive apparatus of type theory.