## Metric Coinduction

**Lecturer:**
Prof. Dexter Kozen (Cornell University, USA).

About the lecturer | Course Summary | Assignment

**About the lecturer:**
(From Wikipedia.)
Dexter Kozen is a renowned American theoretical computer scientist.
He is currently Joseph Newton Pew, Jr. Professor in Engineering at Cornell University.
He received his B.A. from Dartmouth College in 1974 and his PhD in computer
science from Cornell University in 1976, where he was advised by Juris Hartmanis.

He is a Fellow of the Association of Computing Machinery, a Guggenheim Fellow, and has received a Outstanding Innovation Award from IBM Corporation. He has also been named Faculty of the Year by the Association of Computer Science Undergraduates at Cornell.

He is known for his seminal work at the intersection of logic and complexity. He is one of the fathers of dynamic logic and developed the version of the mu calculus most used today. Moreover, he has written several textbooks on the theory of computation, automata theory, dynamic logic, and algorithms.

Advised 17 PhD students.

**Course summary:**

Mathematical induction is firmly entrenched as a fundamental and ubiquitous
proof principle for proving properties of inductively defined objects.
Mathematics and computer science abound with such objects, and mathematical
induction is certainly one of the most important tools at our disposal.
Somewhat less well known is the notion of coinduction. Despite recent
interest, coinduction is still not fully established in our collective
mathematical consciousness. A contributing factor is that coinduction is
often presented in a relatively restricted form. It is often considered
synonymous with bisimulation and is used to establish equality or other
relations on infinite data objects such as streams or recursive types.
In these lectures I will introduce the notion of metric coinduction as a
general proof principle and illustrate its use in some nonstandard
application areas, including coin-flipping protocols, streams, Markov
chains, Markov decision processes, and non-well-founded sets.

**Assignment**

Tasks are here: [PDF].

Please solve problems 1, 2, and either 3 or 4. Some useful definitions are
given at the end. Please use LaTeX and and submit a .pdf file by June 15, 2009
to kowalik AT mimuw DOT edu DOT pl. Please include your name and email
address.