unofficial copies [PDF], [PS]

by James Caldwell and Judith Underwood

Proceedings of the CADE-13 Workshop on Proof Search in Type-Theoretic Languages, D. Galmiche (ed.), Rutgers:NJ, 1996.

In this paper, we compare program development by extraction from a constructive proof with direct verification of a function. Motivated by the development of a decision procedure for intuitionistic propositional logic, we have taken first steps toward considering how classical type systems might be used in support of constructive systems. To this end we explore two statements of theorems asserting the existence of the tableau decision procedure. The constructive proof of one has a tableau decision procedure as its extraction; the other, if proved classically by providing a explicit witness, results in a verified decision procedure. The systems considered are the classical type theory of the PVS system and the constructive type theory of the Nuprl system. Since lambda terms encode constructive proofs, the question of what the explicit witness of the PVS theorem might prove on the constructive side is also considered.