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

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.

http://www.cis.upenn.edu/~bcpierce/sf/

This book should be good for people with a CS background (and some PL on top of that).
Adam Chlipala’s Certified Programming with Dependent Types explains more advanced Coq techniques.

http://adam.chlipala.net/cpdt/

It relies heavily on tactics, which can be an impediment if one actually cares about the proof.

Exercises Written for "Certified Programming with Dependent Types":
- Snapshot of exercises that were included in CPDT when I decided to stop maintaining exercises (Adam Chlipala) http://adam.chlipala.net/cpdt/ex/exercises.pdf
- Homeworks from CIS 670 at Penn in Fall 2012 (Benjamin Pierce and students in the class) http://www.cis.upenn.edu/~bcpierce/courses/670Fall12/
Exercises from the 2012 International Spring School on FORMALIZATION OF MATHEMATICS

http://www-sop.inria.fr/manifestations/MapSpringSchool/program.html

Examiner: TBD

Full participation is required. This entails attending the meetings, doing the exercises and presenting some of them.

If you want to take part in the course, or add something to this document, feel welcome to edit this file online and send a pull request!

You can also clone the repository locally and/or e-mail patches to victor@lopezjuan.com .