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.

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/

Mon 18 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

14:00 - 15:30
T4: Programs and Proofs in the Coq Proof AssistantTutorials at Room HTC 3
14:00
90m
Talk
T4: Programs and Proofs in the Coq Proof Assistant (Advanced Material)
Tutorials
Robert Rand University of Pennsylvania, Arthur Azevedo de Amorim University of Pennsylvania
Link to publication