Enhancing efficiency and expressiveness of the coinduction proof method

Coalgebraic coinduction generalises the bisimulation proof method from labelled transition systems to a large variety of dynamical systems, including automata, streams, trees etc. Now that the applications of coalgebra and coinduction are rapidly increasing both in size and in scope, ranging from software engineering to automata theory to ecology, limitations of efficiency and expressiveness are becoming an obstacle. We set out to help practisioners overcome this problem by providing them with enhancements of the coinduction proof method, in three different ways. Our first method comes from process theory, where systematic relaxations of bisimulation are used called up-to-context, up-to-bisimilarity, etc., typically leading to much smaller proofs. Secondly, there are recent applications and generalisations of classical greatest-fixed-point reasoning making coinduction both compositional and parametric. Thirdly, there exist quantitative versions of coinductive reasoning, by which processes equivalence can be proved up-to a certain degree of precision. In this proposal, we explain why and how it is feasible to generalise these three families of enhancements to the general level of coalgebra. As a result, we expect to arrive at new coinductive proof methods, at a coalgebraic level of generality, that will be much more efficient and expressive than existing methods. By including some of the leading researchers in the field of classical coinductive enhancements (Sangiorgi, Pous, Van Breugel) in the project team, we expect to make a substantial contribution to the enhancement of coalgebraic coinduction, thereby making its use in practical applications more feasible.