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, hencein programming language semantics, program logics. This is motivated by the appropriateness ofcoinduction for analyzing infinity, so also infinity in computation structures, the prime examplebeing 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 infiniteconstruction 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., inductivereasoning about finite initial fragments thereof is unnatural or inadequate. For instance, one maywant 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.