/coq-course

Coq course at Chalmers CSE

Primary LanguageCoq

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 is planned as a self-reading course. As such, each person is individually responsible for fulfiling the goals set by the examiner. No assistance is provided beyond what other participants are willing and able to give.

Dates

The course will take place during 2017 LP3.

  • Kick-off meeting: Thu 2nd Feb, 3:15pm-5pm, room 6128. Plan, Notes
  • Session 2: Thu 16th Feb, 3:15-5pm, room 6128. Agenda

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 and plan.md for more details.

Reference material

General reference material for the course.

Books

From Coq at nLab:

  • Benjamin Pierce’s Software Foundations 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 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 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 by Andrew W. Appel. "Volume 3 of the Software Foundations series".

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 is required. This entails attending the meetings, doing the exercises and presenting some of them.

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

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.

If you have questions, issues or patches, and do not want to use a Github, you can e-mail project-coq-course@lopezjuan.com instead.

Edit this file