Proofs verifying programs and programs producing proofs
a conceptual analysis
pp. 81-94
in: Rossella Lupacchini, Giovanna Corsi (eds), Deduction, computation, experiment, Berlin, Springer, 2008Abstract
I shall deal here with conceptual questions concerning two related phenomena: 1) the use of deductive machinery to verify the correctness of computer programs, and 2) the running of programs on computers to produce proofs.