Thursday, August 02, 2007

The Coq Proof Assistant

Coq
Coq is a formal proof management system: a proof done with Coq is mechanically checked by the machine. In particular, Coq allows:
  • to define functions or predicates,
  • to state mathematical theorems and software specifications,
  • to develop interactively formal proofs of these theorems,
  • to check these proofs by a relatively small certification "kernel".

No comments: