T4: Programs and Proofs in the Coq Proof Assistant (Advanced Material)
This tutorial will focus on functional programming and mathematical proofs using the Coq proof assistant. Coq is a dependently typed functional programming language that can be used to write programs and verify that they meet a variety of given specifications. This allows to develop software that is correct by construction, in which a variety of possible bugs and exceptions are ruled out a priori.
By the end of the first session, participants should be able to
- Write simple functional programs in Coq
- Write precise program specifications
- Connect 1 and 2 via formal proofs.
The second (advanced) session will focus on verifying complex data structures such as Red-Black Trees.
Please come with Coq and either CoqIDE or Proof General pre-installed on your machine. Try running the first lines of the Proofs and Programs file to be sure everything is working.