Home

Awesome

Coq @ Chalmers

Coq course at the Chalmers CSE department, in principle for PhD students.

Disclaimer:

Dates

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.).

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:

Comparison between SF, CPDT and Coq’Art.

Tutorials

Fun links

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:

How to claim credit for the course:

  1. Check that you fulfill the criteria for full participation. This is an honor system. In case of doubt, open an issue.
  2. 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

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.

Edit this file