Skip to main content
PRL Project

Reflection Mechanisms in Nuprl

by Stuart F. Allen, Robert L. Constable

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.