Colloquium Details
Proofs as programs and proof of programs, an introduction to the Coq system
| Author: | Hugo Herbelin INRIA-Rocquencourt |
|---|---|
| Date: | May 31, 2001 |
| Time: | 15:30 |
| Location: | 220 Deschutes |
Abstract
There is a strong correspondence between a mathematical proof and a program: applying a lemma is the same as applying a function and generalization a statement is the same as abstracting a computation over formal parameters.
This correspondence, known as Curry-Howard isomorphism, has been exploited in the mid 80's to build proof-checkers (e.g. NuPrl and MetaPrl, developed at Cornell University, and Coq, of which I am a contributor) allowing automatic extraction of programs from a proof of their specification.
The Coq system has grown into a fairly large general-purpose proof assistant and it is now significantly used for protocol verification, Java code certification, computer algebra systems certification and formalization of mathematical contents.
The main strengths of Coq are
- a powerful specification language (the logical strength of set theory and the expressiveness of both Prolog and ML - with side-effects)
- user-assisted proof search through certified tactics and decision procedures