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.