Coq course at the Chalmers CSE department, in principle for PhD students.
Disclaimer:
The course took place during 2017 LP3 and LP4.
During the couse, we covered inductive propositions (Víctor L.), the calculus of constructions (Simon R.), coinduction and codatatypes (Andreas L.), the AutoSubst library (Andrea V.), Ltac (Fabian R.) and proof by reflection/ssreflect (Daniel S.).
Coq files with solutions to the exercises. Deliverables are uploaded to a separate, private repository.
Participants are expected to be familiar with a functional language with a rich type system, such as Agda, Haskell or Scala. They should also be able to use induction to prove properties about the natural numbers, or any other inductively defined set.
See syllabus.md, suggestions.md and plan.md for more details.
General reference material for the course.
Partly based on Coq at nLab:
Benjamin Pierce’s Software Foundations (SF) is probably the most elementary introduction to Coq and functional progamming. The book is written in Coq so you can directly open the source files in CoqIDE and step through them to see what is going on and solve the exercises.
This book should be good for people with a CS background (and some PL on top of that).
SF uses Coq for the formalization of programming languages.
Adam Chlipala’s Certified Programming with Dependent Types (CPDT) explains more advanced Coq techniques.
It relies heavily on tactics, which can be an impediment if one actually cares about the proof.
CPDT uses Coq as a programming language with a rich type system.
Mathematical Components (MCB) by Assia Mahboubi, Enrico Tassi with contributions by Yves Bertot and Georges Gonthier:
This books targets two classes of public. On one hand newcomers, even the more mathematical inclined ones, find a soft introduction to the programming language of Coq, Gallina, and the Ssreflect proof language. On the other hand accustomed Coq users find a substantial account of the formalization style that made the Mathematical Components library possible.
Mathcomp focuses on practical math, more on the discrete algebra side (natural and polynomial arithmetic, finite dimensional linear algebra, finite group theory, representations, ... + some finite graph theory).
Verified Functional Algorithms (VFA) by Andrew W. Appel. "Volume 3 of the Software Foundations series".
Coq'Art
Formal Reasoning About Programs (FRAP), another book by Chlipala. Similar to SF in the sense that it's also about PLT, see course web page for more info. Has exercises.
Comparison between SF, CPDT and Coq’Art.
Exercises written for Certified Programming with Dependent Types:
Snapshot of exercises that were included in CPDT when Chlipala decided to stop maintaining them
Homeworks from CIS 670 at Penn in Fall 2012 -- Benjamin Pierce and students in the class
Exercises from the 2012 International Spring School on FORMALIZATION OF MATHEMATICS
There are quite many exercises in the SF books (SF and VFA) and Coq'Art.
Modelling and verifying algorithms in Coq: an introduction -- yet another introductory tutorial, has some exercises.
Coq Math Problems -- growing collection of "interesting, challenging, or fun math problems formalized in Coq"
(Exercism.io -- currently only trivial exercises.)
Examiner: Thierry Coquand
Credits: 7.5, but the final decision about how many credits the course gives rests with each participant’s respective examiner.
Full participation in the course entails:
How to claim credit for the course:
We set up an IRC channel for discussing the course:
##coq@chalmers on freenodeNote that there are two hashes in the channel name.
If you don't want to run your own server for running a client continuously, you can use riot's IRC bridge:
The course has started. If you still want to take part, you can add your name to the list of participants by editing this file online and sending in a pull request. Be aware that you might have to work harder in the beginning in order to catch up. The course is over.
If you have questions, issues or patches, and do not want to use a Github account, you can e-mail project-coq-course@lopezjuan.com instead.