The convergence of deduction and computation STRL Annual Distinguished Seminar

Title
The convergence of deduction and computation

Abstract
Deductive proof, property checking and program execution are traditionally implemented by distinct tools: theorem provers, model checkers and interpreters, respectively. However, several proof assistants support these activities within a single framework, blurring the distinctions between them. I will describe how the HOL-4 platform integrates theorem proving, BDD and SAT based algorithmic verification and efficient execution. Recent work on exploiting this integration will be outlined and we will discuss how it represents a modern realisation of the principle "Computation = Logic + Control" developed by Kowalski and Hayes in the 1970s.

[postscript | pdf ]