Coinduction for Computation Structures and Programming Languages

NII Shonan Meeting:

@ Shonan Village Center, October 7-10, 2013

NII Shonan Meeting Report (ISSN 2186-7437):No.2013-11

Organizers

  • Ichiro Hasuo, U. of Tokyo, (JP)
  • Keiko Nakata, Institute of Cybernetics at TUT, Tallinn (EE)
  • Tarmo Uustalu, Institute of Cybernetics at TUT, Tallinn (EE)

Overview

You can see the seminar detail in the following web page.

https://sites.google.com/site/shonanmeeting026/home

This meeting has as its aim to study the applications of coinduction (coinductive data/predicates,
bisimilarity, corecursion and coinduction) to reasoning about computation and programs, hence
in programming language semantics, program logics. This is motivated by the appropriateness of
coinduction for analyzing infinity, so also infinity in computation structures, the prime example
being infinitely running computations, e.g., of machines or programs, especially in the context of
reactive computation.

Induction and coinduction are, by themselves, dual notions. But in typical non-self-dual settings of
actual interest they come out as quite different. The most important outcome of the asymmetries
is that induction is about finite construction and infinite use, but coinduction is about infinite
construction and finite use of data.

Lately there is a growing interest in coinduction in the areas of programming semantics and
formal verification of software systems, in part thanks to advances in type-theoretical programming
languages and proof assistants. There are many important and practical examples where one needs
to reason about finitely observable infinite computations and replacing this by, e.g., inductive
reasoning about finite initial fragments thereof is unnatural or inadequate. For instance, one may
want to prove that some program transformations do not change the observational behavior of
possibly nonterminating transformational programs or of infinitely running reactive programs.

Although coinduction should be very useful, in reality it is not really well understood. In fact,
coinduction is surrounded by quite some popular confusions and has become a standard tool only
in concurrency theory and coalgebra. The theory of coinduction is on many occasions subtle
and challenging. It is often difficult to translate between the vocabularies developed in different
disciplines (e.g., coalgebra, proof theory, type theory). The applications are sometimes not supported
well by tools. For example, it is by no means clear how to best support coinductive data
and predicates in type-theoretical programming languages and proof assistants. Unfortunately,
the mechanisms offered by the current systems are weak and/or cumbersome. As a result, the
corresponding applications are underdeveloped.

Of interest for the meeting are at least the following topics:

? coinductive computation structures, in particular for possibly infinite behaviors (of machines,
programs etc), interaction, concurrency,
? coinductive program semantics, type systems, program logics,
? computability for coinductive data,
? theory of coinductive types, bisimilarity, corecursion/coinduction in type theory, proof theory,
category theory,
? support for coinductive types in dependently typed programming languages, type-theoretic
proof assistants.

Coinduction is applied by researchers from different communities, with diverse technical backgrounds.
There are multiple approaches to coinduction, it is used in different applications. The
meeting encourages exchanges between researchers representing different areas and communities:
programming languages design, implementation, semantics, functional programming, theory of
concurrency, category theory (coalgebra), proof theory, type theory.