×

Sound and complete equational reasoning over comodels. (English) Zbl 1351.68078

Ghica, Dan (ed.), Proceedings of the 31st conference on the mathematical foundations of programming semantics (MFPS XXXI), Nijmegen, The Netherlands, June 22–25, 2015. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 319, 315-331, electronic only (2015).
Summary: Comodels of Lawvere theories, i.e. models in \(\mathsf{Set}^{\mathrm{op}}\), 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.
For the entire collection see [Zbl 1342.68016].

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
03B70 Logic in computer science
18C10 Theories (e.g., algebraic theories), structure, and semantics
68Q55 Semantics in the theory of computing

Software:

CIRC; Cyclist
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abel, A., Mixed inductive/coinductive types and strong normalization, (Asian Symposium on Programming Languages and Systems, APLAS 2007. Asian Symposium on Programming Languages and Systems, APLAS 2007, LNCS, vol. 4807 (2007), Springer), 286-301 · Zbl 1138.68023
[2] Abou-Saleh, F.; Pattinson, D., Comodels and effects in mathematical operational semantics, (Foundations of Software Science and Computations Structures, FoSSaCS 2013. Foundations of Software Science and Computations Structures, FoSSaCS 2013, LNCS, vol. 7794 (2013), Springer), 129-144 · Zbl 1260.68250
[3] Borceux, F., Handbook of Categorical Algebra (1994), Cambridge University Press · Zbl 0911.18001
[4] Brotherston, J.; Gorogiannis, N.; Petersen, R. L., A generic cyclic theorem prover, (Asian Symposium on Programming Languages and Systems, APLAS 2012. Asian Symposium on Programming Languages and Systems, APLAS 2012, LNCS, vol. 7705 (2012), Springer), 350-367
[5] Brotherston, J.; Simpson, A., Complete sequent calculi for induction and infinite descent, (Logic in Computer Science, LICS 2007 (2007), IEEE Computer Society), 51-62
[7] Endrullis, J.; Hansen, H. H.; Hendriks, D.; Polonsky, A.; Silva, A., A coinductive treatment of infinitary rewriting, CoRR (2013)
[8] Kerkhoff, S., A general duality theory for clones, Int. J. Alg. Comput., 23, 3, 457-502 (2013) · Zbl 1286.08003
[9] Kerkhoff, S., Dualizing clones as models of lawvere theories, (Algebraic Complexity Theory, WACT 2013. Algebraic Complexity Theory, WACT 2013, ENTCS, vol. 303 (2014), Elsevier), 79105 · Zbl 1341.08002
[10] Lucanu, D.; Goriac, E.; Caltais, G.; Rosu, G., CIRC: A behavioral verification tool based on circular coinduction, (Algebra and Coalgebra in Computer Science, CALCO 2009. Algebra and Coalgebra in Computer Science, CALCO 2009, LNCS, vol. 5728 (2009), Springer), 433-442 · Zbl 1239.68066
[11] Møgelberg, R.; Staton, S., Linear usage of state, Log. Meth. Comput. Sci., 10 (2014) · Zbl 1326.68070
[12] Plotkin, G.; Power, J., Tensors of comodels and models for operational semantics, (Mathematical Foundations of Programming Semantics, MFPS 2008. Mathematical Foundations of Programming Semantics, MFPS 2008, ENTCS, vol. 218 (2008), Elsevier), 295-311 · Zbl 1286.68303
[13] Plotkin, G., Adequacy for algebraic effects with state, (Algebra and Coalgebra in Computer Science, CALCO 2005. Algebra and Coalgebra in Computer Science, CALCO 2005, LNCS, vol. 3629 (2005), Springer), 51 · Zbl 1151.68466
[14] Power, J.; Shkaravska, O., From comodels to coalgebras: State and arrays, (Coalgebraic Methods in Computer Science, CMCS 2004. Coalgebraic Methods in Computer Science, CMCS 2004, ENTCS, vol. 106 (2004), Elsevier), 297-314 · Zbl 1271.18006
[15] Power, J., Semantics for local computational effects, (Mathematical Foundations of Programming Semantics, MFPS 2006. Mathematical Foundations of Programming Semantics, MFPS 2006, ENTCS, vol. 158 (2006), Elsevier), 355-371 · Zbl 1273.68214
[16] Rosu, G.; Lucanu, D., Circular coinduction: A proof theoretical foundation, (Algebra and Coalgebra in Computer Science, CALCO 2009. Algebra and Coalgebra in Computer Science, CALCO 2009, LNCS, vol. 5728 (2009), Springer), 127-144 · Zbl 1239.68067
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.