Admiring Proof Reflections and Working with Them
Robert L. Constable, Cornell University
Abstract
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.