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 ]