Admiring Proof Reflections and Working with Them
Robert L. Constable, Cornell University
This talk will discuss the role of reflection in
the work of reasoning about programs and protocols
using a proof development system such as Nuprl. The
talk discusses the kind of proof really used in applications.
They are called tactic-tree proofs. The talk discusses
the role of reflection in specifying the computational
complexity of programs synthesized from constructive
proofs. I note several points at which Sol Feferman's
results have shaped the design of Nuprl.