Deals with effectively machine-checked formal mathematics. In practice, this includes the study of mathematical formalisms well-suited for implementations, the implementations themselves and the use of these for various applications. Focuses on software correctness proofs.
Authored by
at
, Added: Mar 8, 2004
http://pauillac.inria.fr/coq/
