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.


Each course consisted of a 1 hour lecture and a 1 hour 1/2 practical class

Download the program.


All the .v files have been developed using Coq 8.4pl6

External Resources