Conference contribution
(Original article)


Sound and Complete Equational Reasoning over Comodels


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
Event: Mathematical Foundations of Programming Semantics XXXI
Event location: Nijmegen

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.



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). 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
Share link
Last updated on 2017-08-19 at 03:13
PDF downloaded successfully