Sound and Complete Equational Reasoning over Comodels

Conference contribution
(Original article)


Publication Details

Author(s): Schröder L, Pattinson D
Title edited volumes: Electronic Notes in Theoretical Computer Science
Publisher: Elsevier BV
Publication year: 2015
Title of series: Electronic Notes in Theoretical Computer Science
Volume: 319
Conference Proceedings Title: Proc. Mathematical Foundations of Programming Semantics XXXI, MFPS 2015
Pages range: 315-331
ISSN: 1571-0661


Abstract


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.



FAU Authors / FAU Editors

Schröder, Lutz Prof. Dr.
Lehrstuhl für Informatik 8 (Theoretische Informatik)


How to cite

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: 

Last updated on 2018-19-04 at 03:16