Skip to content

Latest commit

 

History

History
167 lines (104 loc) · 8.06 KB

README.md

File metadata and controls

167 lines (104 loc) · 8.06 KB
Raw

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

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:

  • 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:

  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

  • 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 project-coq-course@lopezjuan.com instead.

Edit this file