Skip to main content
PRL Project

Using Reflection to Explain and Enhance Type Theory

by Robert L. Constable

From Proof and Computation (NATO ASI Series F)

  • unofficial copies PDF, PS
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.

bibTex ref: Con94

cite link