KnowledgeBase » SEMINAR » ID = 501

Reflection Mechanisms in Nuprl

by Stuart F. Allen, Robert L. Constable
1998-1999

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.