Schröder L, Pattinson D (2015)
Publication Type: Conference contribution, Original article
Publication year: 2015
Publisher: Elsevier BV
Edited Volumes: Electronic Notes in Theoretical Computer Science
Series: Electronic Notes in Theoretical Computer Science
Book Volume: 319
Pages Range: 315-331
Conference Proceedings Title: Proc. Mathematical Foundations of Programming Semantics XXXI, MFPS 2015
Event location: Nijmegen
URI: http://www8.cs.fau.de/_media/research:papers:comodels-compl.pdf
DOI: 10.1016/j.entcs.2015.12.019
Comodels of Lawvere theories, i.e. models in Setop, model state spaces with algebraic access operations. Standard equational reasoning is known to be sound but incomplete for comodels. We give two sound and complete calculi for equational reasoning over comodels: an inductive calculus for equality-on-the-nose, and a coinductive/inductive calculus for equality modulo bisimulation which captures bisimulations syntactically through non-wellfounded proofs.
APA:
Schröder, L., & Pattinson, D. (2015). Sound and Complete Equational Reasoning over Comodels. In Proc. Mathematical Foundations of Programming Semantics XXXI, MFPS 2015 (pp. 315-331). Nijmegen: Elsevier BV.
MLA:
Schröder, Lutz, and Dirk Pattinson. "Sound and Complete Equational Reasoning over Comodels." Proceedings of the Mathematical Foundations of Programming Semantics XXXI, Nijmegen Elsevier BV, 2015. 315-331.
BibTeX: Download