Talk "Towards a Metalanguage for Corecursive Definitions"

by Sergey Goncharov

Sat, 27 June 2015 at 10:00 am in Nijmegen, The Netherlands

Abstract: In recent decades, the theory of coalgebras has proven to provide a suitable general platform for defining and reasoning by corecursion and coinduction. Various results in automata theory, game theory, functional programming can be couched in coalgebraic terms and generic coalgebraic arguments can be applied to ensure existence and uniqueness of the defined concepts. A well-established umbrella principle for coalgebraic definitions is guarded corecursion. Here we propose a syntactic calculus for formalizing and reasoning about guarded corecursion. In particular, we show how this calculus can be used for defining operations by guarded corecursion. We compare this approach with the traditional GSOS-style semantics and clarify connections to the theories of completely iterative monads and complete Elgot monads introduced and actively studied recently.