# * Reflecting the Open-Ended Computation System of Constructive Type Theory *

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

1990

Logic Algebra and Computation (NATO ASI Series)

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

**bibTex ref: CAH90**

cite link