This seminar is an introduction to bisimulation and coinduction - techniques for reasoning about, possibly infinite, computing processes that interact with other processes and/or the environment in which they are run. The goal of the seminar is to familiarize the students with the mathematical foundations of bisimulation and coinduction, and to present their applications in various areas, including the semantics of infinite data structures (e.g., streams) and the theory of program equivalence in sequential languages (e.g., the Lambda-Calculus) as well as the theory of concurrent (mobile) communicating processes (e.g., CCS, the Pi-Calculus).
