Résumé | 4 sessions for learning Coq (2/4):
Modelling and verifying algorithms in Coq: an introduction
The Coq system provides a functional programming language and a
reasoning framework based on higher order logic to perform proofs on
programs. The expressive power of the language is such that
advanced notions of mathematics (such as the graph theory in the four
color theorem) or programs of high complexity (such as a compiler for
a significant kernel of the C Programming language) can be described
formally. In this school, we address the basic programming techniques
and approaches to prove properties of the programs. The covered
notions involve structural recursive programming, list and integer
handling, proof by induction, in the key definition of data-types,
pattern matching constructs and case-based reasoning, and inductive
properties. |