Coq tutorial @ ITP'15
The Coq ITP 2015 tutorial was held in Nanjing, China, from the 27th of August to the 29th of August.
The tutorial was dedicated to beginners and introduced the basics of the Coq proof assistant. The tutorial consisted of a mixture of lectures and practical classes where the participants were given practical problems to be solved in Coq.
Participants brought their own laptops with Coq already installed on it.
Speakers
- Reynald Affeldt (AIST)
- Sandrine Blazy (IRISA - University of Rennes 1)
- Cyril Cohen (Inria - Marelle team)
- Hugo Herbelin (Inria - πr2 team)
- Gregory Malecha (University of California, San Diego)
- Enrico Tassi (Inria - Marelle team)
Program
Each course consisted of a 1 hour lecture and a 1 hour 1/2 practical class
Download the program.
Resources
All the .v files have been developed using Coq 8.4pl6
- Coq Survival Kit
- Introduction to the Coq system: course-1.pdf, course-1.v, exercises-1.v, solutions-1.v, faq-1.pdf
- Programming in Coq: exercises-2.v, solutions-2.v
- Inductive Types and Induction: course-3.v, exercices-3.v
- Dependent Programming: slides-4.pdf, course-4.v, exercices-4.v, solutions-4.v
- Proving Properties on Programs: course-5.pdf, exercises-5.v, solutions-5.v
- Type Classes - Setoids: course-6.v, exercises-6.v, solutions-6.v
External Resources
- Documentation links
- Cocorico! - a wiki about Coq that contains numerous examples
Organizers