Document Open Access Logo

Coinduction: Automata, Formal Proof, Companions (Invited Paper)

Author Damien Pous

PDF

File

Thumbnail PDF
PDF
LIPIcs.CALCO.2019.4.pdf
  • Filesize: 309 kB
  • 4 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
Keywords
  • Coinduction
  • Automata
  • Coalgebra
  • Formal proofs

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

Coinduction is a mathematical tool that is used pervasively in computer science: to program and reason about infinite data-structures, to give semantics to concurrent systems, to obtain automata algorithms. We present some of these applications in automata theory and in formalised mathematics. Then we discuss recent developments on the abstract theory of coinduction and its enhancements.

Cite As Get BibTex

Damien Pous. Coinduction: Automata, Formal Proof, Companions (Invited Paper). In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 4:1-4:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.CALCO.2019.4

Author Details

Damien Pous
  • Univ Lyon, CNRS, ENS de Lyon, UCB Lyon 1, LIP, Lyon, France

Funding

This work has been funded by the European Research Council (ERC) under the European Union’s Horizon 2020 programme (CoVeCe, grant agreement No 678157).

References

  1. F. Bartels. On generalised coinduction and probabilistic specification formats. PhD thesis, CWI, Amsterdam, April 2004. Google Scholar
  2. Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, and Dmitriy Traytel. Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants. In ESOP, volume 10201 of LNCS, pages 111-140. Springer, 2017. URL: https://doi.org/10.1007/978-3-662-54434-1_5.
  3. S. L. Bloom, Z. Ésik, and G. Stefanescu. Notes on equational theories of relations. Algebra Universalis, 33(1):98-126, 1995. URL: https://doi.org/10.1007/BF01190768.
  4. Maurice Boffa. Une remarque sur les systèmes complets d'identités rationnelles. Informatique Théorique et Applications, 24:419-428, 1990. URL: http://archive.numdam.org/article/ITA_1990__24_4_419_0.pdf.
  5. Filippo Bonchi and Damien Pous. Checking NFA equivalence with bisimulations up to congruence. In POPL, pages 457-468. ACM, 2013. URL: https://doi.org/10.1145/2429069.2429124.
  6. Thomas Braibant and Damien Pous. Deciding Kleene Algebras in Coq. LMCS, 8(1):1-16, 2012. URL: https://doi.org/10.2168/LMCS-8(1:16)2012.
  7. Paul Brunet and Damien Pous. Petri automata for Kleene allegories. In LICS, pages 68-79. ACM, 2015. URL: https://doi.org/10.1109/LICS.2015.17.
  8. Paul Brunet, Damien Pous, and Georg Struth. On decidability of Concurrent Kleene Algebra. In CONCUR, volume 85 of LIPIcs, pages 24:1-24:16. Schloss Dagstuhl, 2017. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2017.28.
  9. Amina Doumane and Damien Pous. Completeness for identity-free Kleene Lattices. In CONCUR, volume 118 of LIPIcs, pages 18:1-18:17. Schloss Dagstuhl, 2018. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2018.18.
  10. Z. Ésik and L. Bernátsky. Equational properties of Kleene algebras of relations with conversion. Theoretical Computer Science, 137(2):237-251, 1995. URL: https://doi.org/10.1016/0304-3975(94)00041-G.
  11. Chung-Kil Hur, Georg Neis, Derek Dreyer, and Viktor Vafeiadis. The power of parameterization in coinductive proof. In POPL, pages 193-206. ACM, 2013. URL: https://doi.org/10.1145/2429069.2429093.
  12. B. Knaster. Un théorème sur les fonctions d'ensembles. Annales de la Société Polonaise de Mathématiques, 6:133-134, 1928. Google Scholar
  13. D. Kozen. A Completeness Theorem for KLeene Algebras and the Algebra of Regular Events. Information and Computation, 110(2):366-390, 1994. URL: https://doi.org/10.1006/inco.1994.1037.
  14. D. Kozen. Kleene algebra with tests. Transactions on Programming Languages and Systems, 19(3):427-443, May 1997. URL: https://doi.org/10.1145/256167.256195.
  15. Daniel Krob. A Complete System of B-Rational Identities. In ICALP, volume 443 of LNCS, pages 60-73. Springer, 1990. URL: https://doi.org/10.1007/BFb0032022.
  16. Marina Lenisa, John Power, and Hiroshi Watanabe. Distributivity for endofunctors, pointed and co-pointed endofunctors, monads and comonads. Electronical Notes in Computer Science, 33:230-260, 2000. URL: https://doi.org/10.1016/S1571-0661(05)80350-0.
  17. Yoshiki Nakamura. Partial derivatives on graphs for Kleene allegories. In LiCS, pages 1-12. IEEE, 2017. URL: https://doi.org/10.1109/LICS.2017.8005132.
  18. Damien Pous. Kleene Algebra with Tests and Coq tools for while programs. In ITP, volume 7998 of LNCS, pages 180-196. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39634-2_15.
  19. Damien Pous. Coinduction all the way up. In LICS, pages 307-316. ACM, 2016. URL: https://doi.org/10.1145/2933575.2934564.
  20. Damien Pous. On the positive calculus of relations with transitive closure. In STACS, volume 96 of LIPIcs, pages 3:1-3:16. Schloss Dagstuhl, 2018. URL: https://doi.org/10.4230/LIPIcs.STACS.2018.3.
  21. Damien Pous and Jurriaan Rot. Companions, Codensity, and Causality. In FoSSaCS, volume 10203 of LNCS. Springer, 2017. Extended version at https://arxiv.org/abs/1712.08526. URL: https://doi.org/10.1007/978-3-662-54458-7_7.
  22. Jan J. M. M. Rutten. A coinductive calculus of streams. Math. Struct. in Comp. Sci., 15(1):93-147, 2005. URL: https://doi.org/10.1017/S0960129504004517.
  23. D. Sangiorgi. On the Bisimulation Proof Method. Math. Struct. in Comp. Sci., 8:447-479, 1998. URL: https://doi.org/10.1017/S0960129598002527.
  24. Davide Sangiorgi and David Walker. The π-calculus: a Theory of Mobile Processes. Cambridge University Press, 2001. Google Scholar
  25. A. Tarski. A Lattice-Theoretical Fixpoint Theorem and its Applications. Pacific Journal of Mathematics, 5(2):285-309, June 1955. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact