Proofs and Programs

This talk will show the use of programs for the proving of theorems. Its purpose is to show how our experience gained in the derivations of programs might be transferred to the derivation of proofs in general. The examples will go beyond the (traditional) existence theorems.

Dijkstra is known for early graph-theoretical algorithms, the first implementation of ALGOL 60, the first operating system composed of explicitly synchronized processes, the invention of guarded commands and of predicate transformers as a means for defining semantics, and programming methodology in the broadest sense of the word.

His current research interests focus on the formal derivation of proofs and programs, and the streamlining of the mathematical argument in general.

Dijkstra held the Schlumberger Centennial Chair in Computer Sciences at The University of Texas at Austin until retiring in October.