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.