Title: An Introduction to the Coq Proof Assistant
Speaker:Samuel E. Moelius III
Department of Computer & Information Sciences, University of Delaware
Abstract:
There is tremendous benefit in having a proof checked by a machine. In
particular, it offers a high degree of certainty that the proof is
actually correct --- much higher than if the proof were merely checked
by humans.
Coq [1] is a proof assistant tailored to doing proof checking. Coq has been used, for example, to check proofs of non-trivial properties of certain programming languages and their implementations [2,3].
This talk will be an introduction to Coq. The talk will feature a demonstration of the CoqIDE.
The Coq source code that I plan to use during the talk is available here:
http://www.cis.udel.edu/~moelius/sigsys_talk.v
Participants are welcome to download the CoqIDE beforehand, and follow along.
The latest release of the CoqIDE is 8.1pl3. Binaries for Linux and
Windows are available here:
http://coq.inria.fr/distrib-eng.html
A Mac version is available here:
http://coq.darwinports.com
References:
[1] The Coq proof assistant. http://coq.inria.fr
[2] Xavier Leroy and Sandrine Blazy. Formal verification of a C-like
memory model and its uses for verifying program transformations.
Journal of Automated Reasoning, 41(1):1-31, 2008.
[3] Adam Chlipala. Parametric Higher-Order Abstract Syntax for
Mechanized Semantics. ICFP'08. To appear.