Title: Proof Producing Algorithms
Speaker: Sean McLaughlin, CSD
Location: NSH 1507
Time: 12-1 pm
Date: Friday, April 06, 2007
Abstract:
The design and implementation of algorithms is a fundamental task in computer science. But the process is error-prone, and historically many important programs and algorithms have contained serious errors.# While
often we can live with the bugs lurking in our algorithms and code, in some domains it is essential that the programs we write be error-free.
In this talk I will survey strategies for designing algorithms that, in addition to computing a result, produce a proof of the correctness of that result. I will then focus on the application of these strategies to a number of areas, such as automated reasoning, programming language semantics, and formalized mathematics.
