13 nov. 2014
Induction is a pervasive tool in Computer Science and Mathematics for defining objects and for proving properties on them.
Coinduction is the dual of induction, and as such it brings in tools for defining and reasoning on objects that are new and quite different from the tools provided by induction. In particular, with coinduction objects need not be hierarchically, or hereditarily, constructed.Today coinduction is widely used in Computer Science, but also in other fields, including Artificial Intelligence, Cognitive Science, Mathematics, Modal Logics, Philosophy.
In the talk I will review the basics of coinduction, with an emphasis on the difference and the duality with induction. I will also discuss bisimulation, one of best known instances of coinduction, mainly employed to prove equalities among potentially infinite objects: processes or software applications that may continuously interact with their environment, streams, non-well-founded sets, and so on.
Davide Sangiorgi (University of Bologna / Inria)
Vidéo indisponible – Télécharger présentation pdf
