Proving language inclusion and equivalence by coinduction.

Information and Computation, 2015. To appear.

Full paper (pdf).

Extended version of "Coinductive proof techniques for language equivalence", LATA 2013, below.

Stream differential equations: specification formats and solution methods.

CWI Technical Report report FM-1404, 2014, pp. 1--54.

Full paper (pdf).

A Final Coalgebra for k-regular Sequences.

In Franck van Breugel et al (eds.), Horizons of the mind: a tribute to Prakash Panangaden.

LNCS 8464, pp. 363--383, Springer, 2014.

Full paper (pdf).

(Co)Algebraic Characterizations of Signal Flow Graphs.

In Franck van Breugel et al (eds.), Horizons of the mind: a tribute to Prakash Panangaden.

LNCS 8464, pp. 124--145, Springer, 2014.

Full paper (pdf).

Horizons of the mind: a tribute to Prakash Panangaden.

Essays dedicated to Prakash Panangaden on the occasion of his 60th Birthday.

LNCS 8464, pp. 1--514, Springer, 2014.

Full paper (pdf).

A coalgebraic foundation for coinductive union types.

Proceedings ICALP 2014, to appear.

Full paper (pdf).

The dual equivalence of equations and coequations for automata.

CWI Technical Report report FM-1403, 2014, pp. 1--30.

Full paper (pdf).

Algebra-coalgebra duality in Brzozowski's minimization algorithm.

ACM Transactions on Computational Logic (TOCL). Vol. 15, number 1, 2014.

Full paper (pdf).

Dorel Lucanu, Jan Rutten, Alexandra Silva.

Automatic equivalence proofs for non-deterministic coalgebras.

Science of Computer Programming, 2013, pp. 1324--1345.

Full paper (pdf).

Context-free coalgebras.

To appear in the Journal of Computer and System Sciences.

This is an extended version of "Defining context-free power series coalgebraically", CMCS 2012, below.

Coalgebraic characterizations of context-free languages.

Logical methods in Computer Science, Vol. 9 (3:14), 2013, pp. 1--39.

Full paper (pdf).

This is an extended version of "Context-free languages, coalgebraically", CALCO 2011, below.

Stream processing coalgebraically.

Science of Computer Programming Vol. 78, Issue 11, 2013, pp. 2192--2215.

Full paper (pdf).

Proving language inclusion and equivalence by coinduction.

CWI Technical Report FM-1302, 2013, pp. 1--24.

Full paper (pdf).

Extended version of "Coinductive proof techniques for language equivalence", LATA 2013, below.

Varieties and covarieties of languages (preliminary version).

In proceedings of MFPS 2013, ENTCS 298, pp. 7-28.

Full paper (pdf).

Generalizing determinization from automata to coalgebras.

Logical Methods in Computer Science Vol. 9(1:09), 2013, pp. 1--27.

Full paper (pdf).

Coinductive proof techniques for language equivalence.

In A.-H. Dediu, C. Martin-Vide and B. Truthes, eds.,

Proceedings LATA 2013, LNCS 7810.

Full paper (pdf).

Coalgebraic Bisimulation-Up-To.

In P. van Emde Boas, F. Groen, G. Italiano, J. Nawrocki and H. Sack, eds.,

Proceedings SOFSEM 2013, LNCS 7741, pp. 369-381.

Defining context-free power series coalgebraically.

In: D. Pattinson and L. Schroeder (Eds.), Proceedings of CMCS 2012, LNCS 7399, 2012, pp. 20--39.

Full paper (pdf).

A proof of Moessner's theorem by coinduction.

Higher-Order and Symbolic Computation, Volume 24, Number 3, pages 191-206.

Full paper (pdf).

On the final coalgebra of automatic sequences.

In Robert L. Constable and Alexandra Silva (eds.), Logic and Program Semantics.

Essays dedicated to Dexter Kozen on the occasion of his 60th Birthday.

LNCS 7230, pp. 149-164, Springer, 2012.

Full paper (pdf).

Brzozowski's algorithm (co)algebraically.

In Robert L. Constable and Alexandra Silva (eds.), Logic and Program Semantics.

Essays dedicated to Dexter Kozen on the occasion of his 60th Birthday.

LNCS 7230, pp. 12-23, Springer, 2012.

Full paper (pdf).

Final semantics for decorated traces.

Accepted for MFPS 2012.

A coalgebraic perspective on linear weighted automata.

Information and Computation Vol. 211, pp. 77--105, 2012.

Full paper (pdf).

Stream Differential Equations: concrete formats for coinductive definitions.

Technical Report No. RR-11-10, Oxford University, 2011, pp. 1 - 28.

Full paper (pdf).

Brzozowski's algorithm (co)algebraically.

CWI Technical Report SEN-1114, 2011, pp. 1 - 13.

Full paper (pdf).

Automatic equivalence proofs for non-deterministic coalgebras (revised and extended).

CWI Technical Report SEN-1113, 2011, pp. 1 - 38.

Full paper (pdf).

On the final coalgebra of automatic sequences.

CWI Technical Report SEN-1112, 2011, pp. 1 - 14.

Full paper (pdf).

A decision procedure for bisimilarity of generalized regular expressions.

In J. Davies, L. Silva and A. da Silva Simao (eds.), Formal Methods: Foundations and Applications.

Revised lectures of the 13th Brazilian Symposium of Formal Methods (SBMF 2010).

LNCS 6527, pages 226--241, Springer, 2011.

Advanced topics in bisimulation and coinduction.

Cambridge Tracts in Theoretical Computer Science Volume 52, Cambridge University Press, 2011.

The book's website at Cambridge University Press.

An introduction to (co)algebras and (co)induction.

In: Advanced topics in bisimulation and coinduction (see above), pp. 38-99, 2011.

This book chapter is a (modestly) updated version of our 1997 tutorial.

Full paper (pdf).

A coalgebraic perspective on linear weighted automata.

CWI Technical Report SEN-1104, 2011, pp. 1 - 31.

Full paper (pdf).

Accepted for Information and Computation.

An exercise in coinduction: Moessner's theorem.

CWI Technical Report SEN-1103, 2011, pp. 1 - 10.

Full paper (pdf).

Quantitative Kleene coalgebras.

Information and Computation Vol. 209(5), pp. 822--846, 2011.

Special issue with selected papers from CONCUR 2009.

This is an extended version of our CONCUR'09 paper below.

Full paper (pdf).

Context-free languages, coalgebraically.

In Proceedings of CALCO 2011 (A. Corradini, B. Klin, and C. Cirstea (Eds.)),

LNCS 6859, pp. 359--376, 2011.

Full paper (pdf).

Kleene coalgebra - an overview.

Nieuwsbrief van de Nederlandse Vereniging voor Theoretische Informatica (NVTI).

Nummer 15, 2011.

Full paper (pdf).

Intentional automata: a context-dependent model for component connectors.

In proceedings Fundamentals of Software Engineering 2011 (FSEN'11).

LNCS, to appear.

Full paper (pdf).

Complete sets of cooperations.

Information and Computation 208, 2010, pp. 1398-1420.

Full paper (pdf).

Generalizing the powerset construction, coalgebraically.

Proceedings IARCS Annual Conference on Foundations of Software Technology

and Theoretical Computer Science (FSTTCS 2010),

Kamal Lodaya and Meena Mahajan (Eds.), 2010, pp. 272--283.

Full paper (pdf).

A decision procedure for bisimilarity of generalized regular expressions.

In Proceedings of the 13th Brazilian Symposium on Formal Methods (SBMF 2010).

To appear.

Full paper (pdf).

Non-deterministic Kleene coalgebras.

Logical Method in Computer Science, Vol. 6(3) 2010, pp. 1 - 39.

Special issue with selected papers from LICS 2009.

Full paper (pdf).

An earlier version appeared as CWI Technical Report SEN-1001, 2010,

which is an extended version of our LICS'09 paper below.

Symbolic synthesis of Mealy machines from arithmetic bitstream functions.

Scientific Annals of Computer Science, Vol. XX, 2010, pp. 97-130.

Full paper (pdf).

Kleene coalgebras.

CWI Technical Report SEN-1001, 2010, pp. 1 - 40.

Full paper (pdf).

Proceedings of the Tenth Workshop on Coalgebraic Methods in

Computer Science (CMCS 2010), Paphos, Cyprus.

ENTCS Volume 264, Issue 2, pp. 1-198

Full paper (pdf).

Short Contributions CMCS 2010.

CWI Technical Report SEN-1004, 2010, pp. 1 - 32.

Full paper (pdf).

Sampling, Splitting and Merging in Coinductive Stream Calculus.

In Proceedings of Mathematics of Program Construction 2010

(Bolduc, Desharnais, Ktari (Eds.)), LNCS Vol. 6120, 2010, pp. 310 - 330.

Full paper (pdf).

A coinductive calculus of binary trees.

Information and Computation, Volume 208, Issue 5, May 2010, pp. 578-593.

Full paper (pdf).

Sampling, Splitting and Merging in Coinductive Stream Calculus.

CWI Technical report SEN-E0904, 2009, pp. 1-26.

Full paper (pdf).

Coinductive predicates as final coalgebras.

Proceedings of FICS, 2009, pp. 79--85.

Full paper (pdf).

Fault-based Test Case Generation for Component Connectors.

In Proceedings of 3rd IEEE International Symposium

on Theoretical Aspects of Software Engineering,

TASE'09, pages 147-154, IEEE Computer Society, 2009.

Full paper (pdf).

Deriving syntax and axioms for quantitative regular behaviours.

In M. Bravetti and G. Zavattaro, editors, CONCUR'09,

LNCS 5710, pp. 146-162. Springer, 2009.

Full paper (pdf).

An algebra for Kripke polynomial coalgebras.

Proceedings LICS'09 pp. 49-58. IEEE, Computer Science Press, 2009.

Full paper (pdf).

A Kleene theorem for polynomial coalgebras.

In L. de Alfaro, editor, proceedings FoSSaCS'09, LNCS 5504, Springer, 2009, pp. 122--136.

Full paper (pdf).

Rational streams coalgebraically.

Logical Methods in Computer Science, Volume 4(3), 22 pp., 2008.

Full paper (pdf).

Observational coalgebras and complete sets of co-operations.

Proceedings of the 9th Workshop on Coalgebraic Methods in Computer Science (CMCS 2008),

Budapest, Hungary, ENTCS 203(5), pp. 153--174, Elsevier, 2008.

Full paper (pdf).

Coalgebraic Logic and Synthesis of Mealy Machines.

Proceedings FoSSaCS 2008, LNCS 4962, Springer, 2008, pp. 231--245.

A preliminary version appeared as CWI technical report R0705 (see below).

Full paper (pdf).

Regular expressions for polynomial coalgebras.

CWI Technical report E0703.

[Abstract] [Full paper (PDF-file)]

Coalgebraic Logic and Synthesis of Mealy Machines.

CWI Technical report R0705.

[Abstract] [Full paper (PDF-file)]

Behavioural differential equations and coinduction for binary trees.

Proceedings Wollic 2007, LNCS 4576, Springer, 2007, pp. 322-336.

Full paper (pdf).

Coalgebraic foundations of linear systems (an exercise in stream calculus).

Proceedings CALCO 2007, LNCS 4624, Springer, 2007, pp. 425-446.

Full paper (pdf) and slides (pdf) of CALCO talk.

Algebra and Coalgebra in Computer Science.

Special issue of Theoretical Computer Science Vol. 366(1-2), 2006, pp. 1-180.

Modeling component connectors in Reo by constraint automata,

Science of Computer Programming Vol. 61(2), 2006, pp. 75-113.

Synthesis of Mealy machines using derivatives.

Proceedings CMCS 2006, ENTCS Vol. 164, Elsevier, 2006, pp. 27-45.

Full paper (pdf).

See the webpage for a corresponding tool (source code, executable, documentation) here.

Algebraic specification and coalgebraic synthesis of Mealy automata.

Proceedings FACS 2005, ENTCS Vol. 160, Elsevier, 2006, pp. 305-319.

Full paper (pdf).

A tutorial on coinductive stream calculus and signal flow graphs.

Theoretical Computer Science Volume 343(3), pp. 443--481, 2005.

An extended abstract of this paper appeared in LNCS 3188, 2004 (see below).

Proceedings of First International Conference on Algebra and Coalgebra in Computer Science (CALCO 2005).

Lecture Notes in Computer Science 3629, Springer, 2005, 457 pages.

Synthesis of Reo Circuits For Implementation Of Component-Connector Automata Specifications.

In: Proceedings of Coordination 2005, LNCS 3454, 2005, pp. 236-251.

Algebraic specification and coalgebraic synthesis of Mealy automata.

Proceedings FACS 2005, ENTCS, see under 2006. A preprint appeared as:

Technical Report SEN-R0514, CWI, Amsterdam, 2005, pp. 1--16.

[Abstract] [Full paper (PDF-file)]

A coinductive calculus of streams.

Mathematical Structures in Computer Science, Vol. 15, pp. 93-147, 2005.

[Full paper (PDF).]

A preprint appeared earlier as Technical Report SEN-R0120, CWI, Amsterdam.

Algebra, bitstreams, and circuits

In: Contributions to General Algebra Vol. 16, Verlag Johannes Heyn, Klagenfurt, 2005, pp. 231--250.

A preprint appeared earlier as: Technical Report SEN-R0502, CWI, Amsterdam, 2005, pp. 1--21.

[Abstract] [Full paper (PDF-file)]

Synthesis of Reo Circuits For Implementation Of Component-Connector Automata Specifications.

Technical Report SEN-R0412, CWI, Amsterdam, 2004, pp. 1--18.

[Abstract] [Full paper (PDF-file)]

Also in: Proceedings of Coordination 2005, see above.

Models and Temporal Logics for Timed Component Connectors.

Technical Report SEN-R0411, CWI, Amsterdam, 2004, pp. 1--24.

[Abstract] [Full paper (PDF-file)]

Also in: Proceedings of the IEEE International Conference on

Software Engineering and Formal Methods (SEFM '04), 2004, pp. 198-207.

An extended version of this paper will appear in:

International Journal on Software and Systems Modelling (2005).

An application of stream calculus to signal flow graphs.

In: Proceedings FMCO 2003 (Formal Methods for Components and Objects).

Editors: F.S. de Boer, M.M. Bonsangue, S. Graf, W.P de Roever.

Lecture Notes in Computer Science 3188, Springer Verlag, 2004, pp. 276-291.

[Abstract] [Full paper (in pdf)]

This paper contains the technical core of Technical Report SEN-E0305 (CWI, Amsterdam, 2003) mentioned below.

Mathematical Techniques for analysing concurrent and probabilistic systems.

CRM Monograph series Volume 23, American Mathematical Society, 2004, 215 pages.

[Full text (in pdf)]

The differential calculus of bitstreams.

Technical Report SEN-E0403, CWI, Amsterdam, 2004, pp. 1--13.

[Abstract] [Full paper (PDF-file)]

A coinductive calculus of component connectors.

In: (M. Wirsing, D. Pattinson and R. Hennicker, Eds.) Recent Trends in Algebraic Development Techniques, Proceedings of 16th International Workshop on Algebraic Development Techniques (WADT 2002), Lecture Notes in Computer Science 2755, Springer, 2003, pp. 35--56.

A preprint of this paper appeared as Technical Report SEN-R0216 (see below).

Behavioural differential equations: a coinductive calculus of streams, automata, and power series.

Theoretical Computer Science Volume 308(1--3), pp. 1--53, 2003.

[Abstract] [Full paper (in pdf)]

A preprint of this paper appeared as Technical Report SEN-R0023 (see below).

An application of coinductive stream calculus to signal flow graphs

Technical Report SEN-E0305, CWI, Amsterdam, 2003, pp. 1--58.

[Full paper (in pdf)]

Modeling component connectors in Reo by constraint automata

Technical Report SEN-R0304, CWI, Amsterdam, 2003, pp. 1--15.

[Abstract] [Full paper (PDF-file)] [ Full paper (compressed PostScript)]

Also in: (A. Brogi, J.M. Jacquet, E. Pimentel, eds.) Proceedings of FOCLASA 2003, ENTCS 97, Elsevier Science B.V., 2003. An extended version will appear in Science of Computer Programming (2005).

Coinductive counting with weighted automata.

In: Journal of Automata, Languages and Combinatorics Vol. 8, No. 2, pp. 319-352.

Special issue with selected papers of the workshop "Weighted Automata: Theory and Applications" (Dresden, Germany, March 4-8, 2002).

Coinductive counting with weighted automata

Technical Report SEN-R0224, CWI, Amsterdam, 2002, pp. 1--30.

[Abstract] [Full Paper (pdf)]

A coinductive calculus of component connectors

Technical Report SEN-R0216, CWI, Amsterdam, 2002, pp. 1--17.

[Abstract] [Full Paper (pdf)]

Also in Proceedings WADT 2002 (see above under 2003).

Coinductive counting: bisimulation in enumerative combinatorics

Proceedings of Coalgebraic Methods in Computer Science (CMCS '02),

Coalgebraic methods in computer science.

Theoretical Computer Science 280(1-2), 2002.

Special issue including selected papers from the Second International Workshop on Coalgebraic Methods in Computer Science (CMCS '99).

Coinductive counting: bisimulation in enumerative combinatorics (extended abstract)

Technical Report SEN-R0129, CWI, Amsterdam, 2001, pp. 1--16.

Elements of stream calculus (an extensive exercise in coinduction).

Technical Report SEN-R0120, CWI, Amsterdam, 2001, pp. 1--54.

Also in: Proceedings MFPS '01,

Coalgebraic methods in computer science.

Theoretical Computer Science 260(1-2), 2001.

Special issue including selected papers from the First International Workshop on Coalgebraic Methods in Computer Science (CMCS '98).

Universal coalgebra: a theory of systems.

Theoretical Computer Science 249(1), 2000, pp. 3-80.

Full paper (pdf).

This is a revised and extended version of Technical Report CS-R9652 mentioned below.

Behavioural differential equations: a coinductive calculus of streams, automata, and power series.

Technical Report SEN-R0023, CWI, Amsterdam, 2000.

This report combines and extends our earlier papers on automata and languages (CONCUR '98) and formal power series (ICALP '99). A revised version appeared in Theoretical Computer Science Volume 308, 2003 (see above).

Coalgebra, concurrency, and control.

In: R. Boel and G. Stremersch (eds.), Discrete Event Systems (analysis and control), Proceedings of WODES 2000 (5th Workshop on Discrete Event Systems), Kluwer, 2000, pp. 31--38.

This is an extended abstract of Technical Report SEN-R9921, mentioned below.

A transition system semantics for the control-driven language MANIFOLD. Theoretical Computer Science 240, 2000, pp. 3--47.

This is an extended and improved version of Technical Report SEN-R9829, mentioned below.

A note on coinduction and weak bisimilarity for while programs. In Theoretical Informatics and Applications (RAIRO) Vol. 33, 1999, pp. 393-400.

Coalgebra, concurrency, and control. Technical Report SEN-R9921, CWI, Amsterdam, 1999.

Full paper (pdf).

This paper describes some first steps in the use of coinductive reasoning for problems of supervisory control of discrete event systems.

Bisimulation for probabilistic transition systems: a coalgebraic approach. Theoretical Computer Science Vol. 221(1-2), 1999, pp. 271--293. (Extended abstract in the proceedings of ICALP '97.)

Proceedings of Second Workshop on Coalgebraic Methods in Computer Science (CMCS '99),

Automata, power series, and coinduction: taking input derivatives seriously (extended abstract). Technical Report SEN-R9901, CWI, Amsterdam, 1999.

Also in: proceedings of ICALP '99 (J. Wiedermann, P. van Emde Boas and M. Nielsen, eds.), LNCS 1644, Springer, 1999, pp. 645-654.

This paper extends the results of Technical Report SEN-R9803 (`Automata and coinduction') to the more general case of formal power series, and presents in that setting coinductive definitions in terms of so-called behavioural differential equations (which include many classical differential equations as a special case).

A transition system semantics for the control-driven language MANIFOLD. Technical Report SEN-R9829, CWI, Amsterdam, 1998.

To appear in TCS.

A note on coinduction and weak bisimilarity for while programs. Technical Report SEN-R9826, CWI, Amsterdam, 1998.

Appeared also in Theoretical Informatics and Applications (RAIRO), see under 1999 above.

Bisimulation for probabilistic transition systems: a coalgebraic approach. Technical Report SEN-R9825, CWI, Amsterdam, 1998.

Also in Theoretical Computer Science Vol. 221(1-2), 1999, pp. 271--293. (Extended abstract in the proceedings of ICALP '97.)

``Jon Barwise and Larry Moss: Vicious Circles--on the mathematics of non-wellfounded phenomena'' (book review), Bulletin of the American Mathematical Society, Vol. 35(1), 1998, pp. 69--75.

Generalized metric spaces: completion, topology, and powerdomains via the Yoneda embedding. Theoretical Computer Science Vol. 193, 1998, pp. 1--51.

This is a revised version of Technical Report CS-R9636, CWI, Amsterdam, 1996.

On the foundations of final coalgebra semantics: non-well-founded sets, partial orders, metric spaces. Mathematical Structures in Computer Science Vol. 8, 1998, pp. 481--540.

Proceedings of First Workshop on Coalgebraic Methods in Computer Science (CMCS '98),

Relators and Metric Bisimulations (Extended Abstract), in Proceedings of CMCS 1998, ENTCS Vol. 11, Elsevier, 1998.

Full paper (pdf).

Automata and coinduction (an exercise in coalgebra).

Proceedings of CONCUR '98, D. Sangiorigi and R. de Simone (eds.),

LNCS 1466, Springer, 1998, pp. 194-218.

Full paper (pdf).

Weighted colimits and formal balls in generalized metric spaces.

Topology and its Applications, Volume 89, 1998, pp. 179-202.

Weighted colimits and formal balls in generalized metric spaces. Technical Report SEN-R9711, CWI, Amsterdam, 1997.

Also in: Topology and its Applications, Volume 89, 1998, pp. 179-202.

Bisimulation for probabilistic transition systems: a coalgebraic approach (extended abstract). Proceedings of ICALP'97 (P. Degano et al, eds.). LNCS Vol. 1256, 1997, pp. 460-470. See also Technical Report SEN-R9825, CWI, Amsterdam, 1998. An extended version appeared in Theoretical Computer Science Vol. 221(1-2) (see 1999 above).

A Tutorial on (Co)Algebras and (Co)Induction. Bulletin of EATCS Vol. 62, 1997, pp. 222--259.

For a recently (2011) updated version click here (pdf).

Generalized metric spaces: completion, topology, and powerdomains via the Yoneda embedding. Technical Report CS-R9636, CWI, Amsterdam, 1996. This reports extends the results of CS-R9560 to the case of generalized metric spaces.

A revised version of this report (in which some errors are corrected) appeared in `Theoretical Computer Science' (see 1998, above).

Universal coalgebra: a theory of systems. Technical Report CS-R9652, CWI, Amsterdam, 1996.

A revised and extended version of this report will appear in Theoretical Computer Science.

M.M. Bonsangue, F. van Breugel, and J.J.M.M. Rutten

Alexandroff and Scott Topologies for Generalized Metric Spaces.
In: Papers on General Topology and Applications:
Eleventh Summer Conference at University of Southern
Maine (S. Andima et al., eds.),
Annals of the New York Academy of Sciences, 1996, pp. 49-68.

A preliminary version appeared as
Technical Report IR-394, Vrije Universiteit, Amsterdam, 1995.

Elements of generalized ultrametric domain theory. Theoretical Computer Science, Vol. 170, 1996, pp. 349--381.

(Revised version of report CS-R9507, CWI, Amsterdam, 1995.)

Full paper (pdf).

A calculus of transition systems (towards universal coalgebra). Technical Report CS-R9503, CWI, Amsterdam, 1995.

Also appeared in: Modal Logic and Process Algebra, a bisimulation perspective (A. Ponse, M. de Rijke, and Y. Venema, eds.), CSLI Lecture Notes No. 53, CSLI Publications, Standford, 1995, pp. 231--256.

The results of this paper have been generalized in Technical Report CS-R9652 (see above).

Elements of generalized ultrametric domain theory. Technical Report CS-R9507, CWI, Amsterdam, 1995.

A revised version of this report has appeared in Theoretical Computer Science, Vol. 170, 1996, pp. 349--381.

Solutions of functorial and non-functorial metric domain equations, in

Selected papers of the workshop on topology and completion in semantics, Chartres. Special issue of Theoretical Computer Science, Vol. 151(1), 1995.

Generalized ultrametric spaces: completion, topology, and powerdomains via the Yoneda embedding. Technical Report CS-R9560, CWI, Amsterdam, 1995.