License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CALCO.2017.23
URN: urn:nbn:de:0030-drops-80474
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/8047/
Go to the corresponding LIPIcs Volume Portal

Sprunger, David ; Moss, Lawrence S.

Precongruences and Parametrized Coinduction for Logics for Behavioral Equivalence

pdf-format:
LIPIcs-CALCO-2017-23.pdf (0.5 MB)

Abstract

We present a new proof system for equality of terms which present elements of the final coalgebra of a finitary set functor. This is most important when the functor is finitary, and we improve on logical systems which have already been proposed in several papers. Our contributions here are (1) a new logical rule which makes for proofs which are somewhat easier to find, and (2) a soundness/completeness theorem which works for all finitary functors, in particular removing a weak pullback preservation requirement that had been used previously. Our work is based on properties of precongruence relations and also on a new parametrized coinduction principle.

BibTeX - Entry

@InProceedings{sprunger_et_al:LIPIcs:2017:8047,
  author =	{David Sprunger and Lawrence S. Moss},
  title =	{{Precongruences and Parametrized Coinduction for Logics for Behavioral Equivalence}},
  booktitle =	{7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
  pages =	{23:1--23:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-033-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{72},
  editor =	{Filippo Bonchi and Barbara K{\"o}nig},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/8047},
  URN =		{urn:nbn:de:0030-drops-80474},
  doi =		{10.4230/LIPIcs.CALCO.2017.23},
  annote =	{Keywords: precongruence, kernel bisimulation, finitary functor, coalgebra, behavioural equivalence}
}

Keywords: precongruence, kernel bisimulation, finitary functor, coalgebra, behavioural equivalence
Collection: 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)
Issue Date: 2017
Date of publication: 17.11.2017

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI