Write a Blog >>

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.

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

Mon 18 Jan

POPL-2016-tutorials
10:30 - 12:00: Tutorials - T4: Programs and Proofs in the Coq Proof Assistant at Room HTC 3
POPL-2016-tutorials145310940000010:30 - 12:00
Talk
Link to publication