MCP: Mechanised Coinductive Proofs
ECNU, Shanghai, nov 7-11, 2016
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:
inductive and coinductive definitions, the coinduction proof
method and bisimulation;
examples: automata, process calculi;
simple coinductive proofs in the Coq Proof Assistant;
time permitting, enhancements of the bisimulation proof method.
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.
Robin Milner, “Communication and Concurrency”, Prentice Hall.
Davide Sangiorgi, “Introduction to Bisimulation and Coinduction”, Cambridge University Press.
D. Pous and D. Sangiorgi, “Enhancements of the coinductive proof method”,
chapter in the book "Advanced Topics in Bisimulation and Coinduction", D. Sangiorgi and J.
Rutten, editors. Cambridge University Press.
