**21 Nov 2011
Nijmegen, The Netherlands**

COIN, or Coalgebra in the Netherlands, is a newly organized seminar planned to take place alternating at the Radboud University Nijmegen and the CWI in Amsterdam. The aim of COIN is to bring together coalgebra researchers from various locations in the Netherlands, and share current results and questions in the world of coalgebra. We welcome presentations on any subject related to coalgebra. COIN is coordinated by Marcello Bonsangue (Leiden University/CWI), Bart Jacobs (Radboud Universiteit Nijmegen), and Jan Rutten (CWI/Radboud Universiteit Nijmegen), and its website can be found at http://homepages.cwi.nl/~winter/coin.html The first COIN meeting is scheduled for Monday, 21 November 2011, at CWI, in room L120. The schedule is as follows: 14:30 - 15:15 Dimitri Hendriks (VU) and Jörg Endrullis (VU) Equational Reasoning and Bisimulation in Coq 15:15 - 16:00 Jan Rutten (CWI/RU) On the Final Coalgebra of Automatic Sequences 16:15 - 17:00 Marcello Bonsangue (Leiden/CWI) Coalgebraic Characterizations of Regular and Context-Free Languages Abstracts ========= Dimitri Hendriks (VU) and Jörg Endrullis (VU) Equational Reasoning and Bisimulation in Coq -------------------------------------------- We investigate methods for proving in Coq bisimilarity of infinite objects using coinduction and equational reasoning. To avoid the introduction of non-normalizable terms, in Coq the construction of a coinductive object is subjected to a simple syntactic criterion called guarded corecursion. Every corecursive call has to be guarded by (to be an argument of) at least one constructor of the coinductive type we are building a term in, and only by such constructors. Guardedness ensures productivity (the unique existence of infinite constructor normal forms), but rejects many productive specifications. In Coq, proofs are terms, and bisimilarity is defined as a coinductive type, and so also bisimilarity proofs are forced to be guarded. However equational reasoning (i.e., rewriting) usually obstructs guardedness. Typically, applications of transitivity are in between the guard and the coinduction hypothesis. We adopt techniques from process algebra and employ the notion of bisimulations-up-to. Let R be a binary relation on streams, and F a function from relations to relations. Then R is a bisimulation up-to F if s R t implies s(0) = t(0) and s' F(R) t'. For certain F this is sufficient to conclude that R is a subset of ~ (bisimilarity). Typically R is a subset of F(R), and thus, in comparison with a full bisimulation, less diagrams have to be checked. We take F(R) to be the least relation including R and ~, and closed under causal contexts, and under transitivity and symmetry. For this F we show that if R is a bisimulation up-to F, then F(R) is a subset of ~. We show that causality can be proved using techniques to prove productivity. This method allows for an elegant rendering of equational, coinductive proofs, and avoids the troubles with guardedness. Jan Rutten (CWI/Radboud Universiteit Nijmegen) On the Final Coalgebra of Automatic Sequences --------------------------------------------- Streams are omnipresent in both mathematics and theoretical computer science. Automatic sequences form a particularly interesting class of streams that live in both worlds at the same time: they are defined in terms of finite automata, which are basic computational structures in computer science; and they appear in mathematics in many different ways, for instance in number theory. Examples of automatic sequences include the celebrated Thue- Morse sequence and the Rudin-Shapiro sequence. In this talk, we shall apply the coalgebraic perspective on streams to automatic sequences. We shall show that the set of automatic sequences carries a final coalgebra structure, consisting of the operations of head, even, and odd. This will allow us to show that automatic sequences are to (general) streams what rational languages are to (arbitrary) languages. This is joint work with Clemens Kupke, Oxford University. Marcello Bonsangue (Leiden University/CWI) Coalgebraic Characterizations of Regular and Context-Free Languages ------------------------------------------------------------------- In this lecture we present coalgebraic characterizations of regular and context free languages using grammars, behavioural differential equations and generalized regular expressions in which the Kleene star is replaced by a unique fixed point operator.