MCP: Mechanised Coinductive Proofs       ECNU, Shanghai, nov 7-11, 2016

Group picture
Contents of the course (tentative)
This course is an introduction to coinductive reasoning in computer science, and to the formalisation of proofs by coinduction in a theorem prover.
The following topics will be covered:

Prerequisites: all students following the course should have access to a computer for the exercises.
The computer should have the Coq Proof Assistant (which includes the CoqIDE interface) installed on the computer. Please make sure that installation is done successfully before the beginning of the course.

Teaching personnel
Daniel Hirschkoff      Jean-Marie Madiot      Damien Pous