Practical Reflection for Nuprl

These are some materials from my reflection & quotation work in Nuprl:

• The Reflection theory, as rendered by Nuprl. (Note that the “Fiat” proofs should be considered as axioms.)
• My example of using it: a formalization of the Tarski result about truth not being reflected, as sketched by Stuart Allen. Formalized as a Nuprl theory.
• The Tarski proof is also available in HTML format made by Stuart's Nuprl magic tricks, with either my notations or Stuart's.
• My thesis and talk are also available.

(Papers are found on the previous page.)