# No.026 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.