Reflection Mechanisms in Nuprl

Stuart Allen, Robert Constable



November 10, 1998
Abstract

We will talk about how terms, evaluation and proofs are reflected in Nuprl 4. The reflection mechanism is the basis for reasoning about evaluation and computational complexity, and it is the basis for reflected proof.

Subsequent seminars this semester will pursue applications of reflection, so we want to provide some of the basic ideas first.