The proof and denition principle of induction is standard in mathematics and computer science. Recently, it is becoming increasingly clear that coinduction, which is formally dual to induction, provides a foundation for the behaviour of many kinds of structures in computer science, including: various calculi in process algebra; innite data structures in functional programming and theorem provers; automata and formal languages; dynamical systems; behavioural and modal logics; and many more.
Originally, coinduction was studied and developed in the context of process algebra, typically phrased as the bisimulation proof method. The athematical tools for the study of coinduction were complete lattices, monotone operators and greatest xed points. Since the arrival of coalgebra in the arena of the foundations of computer science, coinduction has been captured in terms of nality and coalgebraic bisimulation. These coalgebraic generalisations have increased the scope and applicability of coinduction enormously.

Since the early days of coinduction, several extensions and generalisations {typically referred to as \enhancements” { of coinduction have been developed. These extended techniques involve generalisations of the notion of bisimulation, such as bisimulation up to equivalence, bisimulation up to congruence, and bisimulation up to bisimilarity. These techniques all have in common that they strongly enhance the applicability of coinduction by allowing the bisimulation proof method to be based on much smaller bisimulation relations.
As it turned out, the generalisations that the coalgebraic approach have brought to the eld of coinduction, also apply to these enhanced coinductive techniques. This has led to a very general and widely applicable formulation of up-to techniques, with very recent, new applications in, for instance, automata theory, the theory of innite streams (Moessner’s theorem), and theorem proving.
In the light of these recent new and exciting developments in both the theory and applications of coinduction, this workshop seeks to bring together world leading experts from the relevant disciplines in computer science, notably 

• process algebra
• coalgebra
• automata theory
• functional programming
• logic and type theory

The aims of the workshop can then be summarised as follows:

• advancing the understanding of coinduction and its enhancements, both in terms of lattice theory and coalgebra;
• discussing recent applications of enhanced coinduction and looking for new areas and problems where applications can be found;
• all of this through a cross-fertilisation between the dierent disciplines mentioned above.