Healthiness from duality. (English) Zbl 1401.68042
Proceedings of the 2016 31st annual ACM/IEEE symposium on logic in computer science, LICS 2016, New York City, NY, USA, July 5–8, 2016. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-4391-6). 682-691 (2016).
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 03B70 | Logic in computer science |
| 18A40 | Adjoint functors (universal constructions, reflective subcategories, Kan extensions, etc.) |
| 18C10 | Theories (e.g., algebraic theories), structure, and semantics |
References:
| [1] | J. Adámek and J. Rosick��. Locally Presentable and Accessible Categories. Cambridge Univ. Press, 1994. · Zbl 0795.18007 |
| [2] | M. Barr and C. Wells. Toposes, Triples and Theories. Springer, Berlin, 1985. Available online. · Zbl 0567.18001 |
| [3] | M. M. Bonsangue, editor. Coalgebraic Methods in Computer Science, volume 8446 of Lecture Notes in Computer Science, 2014. Springer. |
| [4] | K. Cho. Total and partial computation in categorical quantum foundations. In C. Heunen, P. Selinger, and J. Vicary, editors, Proc. QPL 2015, volume 195 of EPTCS, pages 116-135, 2015. · Zbl 1477.81028 |
| [5] | K. Cho, B. Jacobs, B. Westerbaan, and A. Westerbaan. An introduction to effectus theory. CoRR, abs/1512.05813, 2015. · Zbl 1352.81011 |
| [6] | D. M. Clark and B. Davey. Natural Dualities for the Working Algebraist. Cambridge Univ. Press, 1998. · Zbl 0910.08001 |
| [7] | E. W. Dijkstra. A Discipline of Programming. Prentice Hall, 1976. · Zbl 0368.68005 |
| [8] | S. Goncharov and L. Schröder. A relatively complete generic Hoare logic for order-enriched effects. In Proc. LICS 2013, pages 273-282. IEEE, 2013. 10.1109/LICS.2013.33 · Zbl 1366.68023 |
| [9] | P. R. Halmos. Algebraic Logic. American Mathematical Society, 2006. · Zbl 0101.01101 |
| [10] | D. Harel, J. Tiuryn, and D. Kozen. Dynamic Logic. MIT Press, Cambridge, MA, USA, 2000. ISBN 0262082896. · Zbl 0976.68108 |
| [11] | I. Hasuo. Generic weakest precondition semantics from monads enriched with order. In Bonsangue {3}, pages 10-32. · Zbl 1331.68051 |
| [12] | I. Hasuo. Generic weakest precondition semantics from monads enriched with order. Theor. Comput. Sci., 604:2-29, 2015. 10.1016/j.tcs.2015.03.047 · Zbl 1330.68046 |
| [13] | W. Hino, H. Kobayashi, I. Hasuo, and B. Jacobs. Healthiness from duality. arXiv preprint, 2016. |
| [14] | C. A. R. Hoare. An axiomatic basis for computer programming. Commun. ACM, 12:576-580, 583, 1969. 10.1145/363235.363259 · Zbl 0179.23105 |
| [15] | D. Hofmann and P. Nora. Dualities for modal algebras from the point of view of triples. Algebra Universalis, 73(3):297-320, 2015. · Zbl 1431.18004 |
| [16] | M. Hyland and J. Power. The category theoretic understanding of universal algebra: Lawvere theories and monads. Electronic Notes in Theoretical Computer Science, 172:437-458, 2007. 10.1016/j.entcs.2007.02.019 · Zbl 1277.08003 |
| [17] | B. Jacobs. Dijkstra monads in monadic computation. In Bonsangue {3}, pages 135-150. · Zbl 1331.68052 |
| [18] | B. Jacobs. A recipe for state-and-effect triangles. In L. S. Moss and P. Sobocinski, editors, CALCO 2015, volume 35 of LIPIcs, pages 116-129, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. · Zbl 1366.68025 |
| [19] | B. Jacobs. New directions in categorical logic, for classical, probabilistic and quantum logic. Logical Methods in Comp. Sci., 11(3), 2015. · Zbl 1338.03117 |
| [20] | B. Jacobs. Dijkstra and Hoare monads in monadic computation. Theoretical Computer Science, 604:30-45, 2015. 10.1016/j.tcs.2015.03.020 · Zbl 1330.68047 |
| [21] | C. Jones. Probabilistic Non-Determinism. PhD thesis, Univ. Edinburgh, 1990. |
| [22] | B. Jónsson and A. Tarski. Boolean algebras with operators I. Amer. Journ. Math., 73:891-939, 1951. · Zbl 0045.31505 |
| [23] | K. Keimel. Healthiness conditions for predicate transformers. Electr. Notes Theor. Comput. Sci., 319:255-270, 2015. 10.1016/j.entcs.2015.12.016 · Zbl 1351.68076 |
| [24] | G. M. Kelly. A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on. Bulletin of the Australian Mathematical Society, 20:1-83, 1980. · Zbl 0437.18004 |
| [25] | G. M. Kelly. Basic Concepts of Enriched Category Theory. Number 64 in LMS. Cambridge Univ. Press, 1982. Available online. |
| [26] | G. M. Kelly and A. J. Power. Adjunctions whose counits are coequalizers, and presentations of finitary enriched monads. Journal of Pure and Applied Algebra, 89(1-2):163-179, 1993. · Zbl 0779.18003 |
| [27] | D. Kozen. Semantics of probabilistic programs. J. Comput. Syst. Sci., 22(3):328-350, 1981. · Zbl 0476.68019 |
| [28] | S. Lack and J. Power. Gabriel-Ulmer duality and Lawvere theories enriched over a general base. J. Funct. Program., 19:265-286, 2009. 10.1017/S0956796809007254 · Zbl 1191.68163 |
| [29] | S. Mac Lane. Categories for the Working Mathematician. Springer, Berlin, 2nd edition, 1998. · Zbl 0906.18001 |
| [30] | M. Makkai and R. Paré. Accessible categories: the foundations of categorical model theory. Contemp. Math., 104, 1989. · Zbl 0703.03042 |
| [31] | C. Morgan, A. McIver, and K. Seidel. Probabilistic predicate transformers. ACM Trans. Program. Lang. Syst., 18(3):325-353, 1996. 10.1145/229542.229547 |
| [32] | A. Sokolova. Coalgebraic Analysis of Probabilistic Systems. PhD thesis, Techn. Univ. Eindhoven, 2005. |
| [33] | T. Wilke. Alternating tree automata, parity games, and modal μ-calculus. Bull. Belg. Math. Soc. Simon Stevin, 8(2):359-391, 2001. · Zbl 0994.68079 |
| [34] | G. Winskel. The Formal Semantics of Programming Languages. MIT Press, 1993. · Zbl 0919.68082 |
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.
