Coq @ Chalmers
Coq course at the Chalmers CSE department, in principle for PhD students.
Disclaimer:
This course is not guaranteed to take place. Times, contents and evaluation form are provisional and subject to change.This course took place.- This course is planned as a self-reading course. As such, each person is individually responsible for fulfilling the goals set by the examiner. No assistance is provided beyond what other participants are willing and able to give.
Dates
The course took place during 2017 LP3 and LP4.
- Kick-off meeting: Thu 2nd Feb, 3:15pm-5pm, room 6128. Plan, Notes
- Session 2: Thu 16th Feb, 3:15-5pm, room 6128. Notes
- Session 3: Thu 2nd Mar, 3:15-5pm, room 6128. Notes
- Session 4: Thu 16th Mar, 3:15-5pm, room 6128. Notes
- Session 5: Thu 6th Apr, 3:15-5pm, room 6128. Notes
- Session 6: Wed 12th Apr, 3:15-5pm, room 4128. Notes
- Session 7: Thu 27th Apr, 3:15-5pm, room 6128. Notes
- Session 8: Thu 11th May, 3:15-5pm, room 6128. Notes
- Final meeting: Wed 7th June, 3:15-5pm, room 4128.
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.).
Deliverables
Coq files with solutions to the exercises. Deliverables are uploaded to a separate, private repository.
Prerequisites
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.
Course plan
See syllabus.md, suggestions.md and plan.md for more details.
Reference material
General reference material for the course.
Books
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.
Tutorials
- Coq tutorial @ ITP 2015
- Basic Coq tutorial by Yves Bertot
- Advanced mathcomp tutorial (1 week) -- contains non-trivial maths
- Short mathcomp tutorial @ ITP 2016
- Coq is covered in some Oregon Programming Languages Summer School iterations, e.g. Chlipala's sessions from 2015 (video format)
Fun links
Exercises
-
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.)
Examination
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:
- Attending a majority of the sessions.
- Doing the exercises for each session, even those which you did not attend, and uploading your solutions to the exercise repo.
- Presenting a topic of your choice during a session.
How to claim credit for the course:
- Check that you fulfill the criteria for full participation. This is an honor system. In case of doubt, open an issue.
- TBA
IRC channel
We set up an IRC channel for discussing the course:
##coq@chalmers on freenode
Note 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:
Participants
- Fabian Ruch
- Andrea Vezzosi
- Víctor López Juan
- Herbert Lange
- Daniel Schoepe
- Irene Lobo Valbuena
- YuTing Chen (jeff)
- Andreas Lööw
- Simon Robillard
- Marco Vassena
- Simon Huber
- João Pizani (visiting until 2017-04-07)
- Youyou Cong (visiting until 2017-06-19)
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 [email protected] instead.