Using Reflection to Explain and Enhance Type Theory

unofficial copies [PDF], [PS]

by Robert L. Constable

Proof and Computation (NATO ASI Series F), H. Schwichtenberg (ed.), vol. 139, pp. 65-100, Springer-Verlag:Berlin, 1994.


The five lectures at Marktoberdorf on which these notes are based were about the architecture of problem solving environments which use theorem provers. Experience with these systems over the past two decades has shown that the prover must be extensible, yet it must be kept. We examine a way to safely add new decision procedures to the Nuprl prover. It relies on a reflection mechanism and is applicable to any tactic-oriented prover with sufficient reflection. The lectures explain reflection in the setting of constructive type theory, the core logic of Nuprl.