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.
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.
