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.