1. Coq development example: proof of correctness of a simple algorithm
The proof of correctness of a simple functional program allows us to present some essential aspects of the Coq software: mathematical statements and formal specification of programs, tools for interactive proof, etc. The proposed example consists of the definition of a sorting function on lists, accompanied by a formal proof of its correctness. The proposed example consists of the definition of a sorting function on lists, accompanied by a formal proof of its correctness.
-
Typographical conventions
We adopt the following conventions so that the reader can easily recognize which text a user should submit to Coq and what the system's responses are.
The text submitted to Coq is written in light blue inserts.
Coq's answers are presented in...
Exclusive to subscribers. 97% yet to be discovered!
Already subscribed? Log in!
Coq development example: proof of correctness of a simple algorithm
Main applications
Article included in this offer
"Software technologies and System architectures"
(
230 articles
)
Updated and enriched with articles validated by our scientific committees
A set of exclusive tools to complement the resources
Bibliography
- (1) - - The CompCert compiler. http://compcert.inria.fr .
- (2) - - OCaml page. http://www.ocaml.org/...
Exclusive to subscribers. 97% yet to be discovered!
Already subscribed? Log in!
