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.

More at http://www.cis.upenn.edu/~rrand/popl_2016/