Sergey Goncharov´s Publications

2024
[37] , , , and : A point-free perspective on lax extensions and predicate liftings, In Mathematical Structures in Computer Science, 34(2), pp. 98–127, . [bibtex] [doi]
2023
[36] , , , and : Towards a Higher-Order Mathematical Operational Semantics, In In 50th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2023), . [bibtex]
[35] , , , and : Kantorovich Functors and Characteristic Logics for Behavioural Distances, In Pawel Sobocinski, Orna Kupferman, eds.: Foundations of Software Science and Computation Structures (FoSSaCS 2023), Springer International Publishing, . [bibtex]
[34] , , , , and : Quantitative Hennessy-Milner Theorems via Notions of Density, In Bartek Klin, Elaine Pimentel, eds.: 31st EACSL Annual Conference on Computer Science Logic, CSL 2023, February 13-16, 2023, Warsaw, Poland, LIPIcs, vol. 252, pp. 22:1–22:20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, . [bibtex] [doi]
2022
[33] , , , and : Stateful Structural Operational Semantics, In Amy Felty, ed.: Proc. 7th International Conference on Formal Structures for Computation and Deduction (FSCD), LIPIcs, Schloss Dagstuhl – Leibniz-Zentrum für Informatik, . To appear; available online at https://arxiv.org/pdf/2202.10866 [bibtex]
2021
[32] , and : A metalanguage for guarded iteration, In Theoretical Computer Science, 880, pp. 111–137, . [bibtex]
[31] : Uniform Elgot Iteration in Foundations, In Nikhil Bansal, Emanuela Merelli, James Worrell, eds.: 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021), LIPIcs, vol. 198, pp. 131:1–131:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik, . [bibtex]
2020
[30] , and : Towards a Uniform Theory of Effectful State Machines, In ACM Trans. Comput. Logic, 21(3), . [preprint] [bibtex] [url]
[29] and : Local Local Reasoning: A BI-Hyperdoctrine for Full Ground Store, In Jean Goubault-Larrecq, Barbara König, eds.: 23rd International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2020), Lecture Notes in Computer Science, vol. 12077, pp. 542–561, Springer, . [bibtex] [url] [doi]
[28] : Implementing Hybrid Semantics: From Functional to Imperative, In Adenilso da Silva Simão Volker Stolz Violet Ka I Pun, ed.: 17th International Colloquium on Theoretical Aspects of Computing (ICTAC 2020), . [preprint] [bibtex]
[27] and : Towards Constructive Hybrid Semantics, In Zena M. Ariola, ed.: 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), Leibniz International Proceedings in Informatics (LIPIcs), vol. 167, pp. 24:1–24:19, Schloss Dagstuhl–Leibniz-Zentrum für Informatik, . [bibtex] [url] [doi]
2019
[26] and : Coinductive Resumption Monads: Guarded Iterative and Guarded Elgot, In Markus Roggenbach, Ana Sokolova, eds.: Proc. 8rd international conference on Algebra and coalgebra in computer science (CALCO 2019), LIPIcs, vol. 139, pp. 13:1–13:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, . [bibtex] [url] [doi]
[25] , , and : Guarded and Unguarded Iteration for Generalized Processes, In Logical Methods in Computer Science, 15(3), . [bibtex] [url] [doi]
[24] and : An Adequate While-Language for Hybrid Computation, In Ekaterina Komendantskaya, ed.: Proceedings of the 21th International Symposium on Principles and Practice of Declarative Programming, (PPDP 2019), ACM, . [preprint] [bibtex]
2018
[23] and : Guarded Traced Categories, In Christel Baier, Ugo Dal Lago, eds.: Proc. 21st International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2018, LNCS, vol. 10803, pp. 313–330, Springer, . [bibtex] [url] [doi]
[22] , and : A Metalanguage for Guarded Iteration, In Bernd Fischer, Tarmo Uustalu, eds.: Theoretical Aspects of Computing – ICTAC 2018, pp. 191–210, Springer International Publishing, . [ArXiv preprint] [bibtex]
[21] , and : A Semantics for Hybrid Iteration, In Sven Schewe, Lijun Zhang, eds.: 29th International Conference on Concurrency Theory (CONCUR 2018), LNCS, Springer, . [preprint] [bibtex]
[20] , , and : Unguarded Recursion on Coinductive Resumptions, In Log. Methods Comput. Sci., 14(3), . [bibtex] [url] [doi]
2017
[19] , and : Generic Hoare Logic for Order-Enriched Effects with Exceptions, In Phillip James, Markus Roggenbach, eds.: Recent Trends in Algebraic Development Techniques: 23rd IFIP WG 1.3 International Workshop, WADT 2016, Revised Selected Papers, pp. 208–222, Springer, . The final publication is available at Springer via https://doi.org/10.1007/978-3-319-72044-9_14. [bibtex] [pdf]
[18] , , and : Unifying Guarded and Unguarded Iteration, In Javier Esparza, Andrzej Murawski, eds.: Proc. 20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2017), Lect. Notes Comput. Sci. (ArCOSS), vol. 10203, pp. 517–533, Springer, . The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-662-54458-7_30. [bibtex] [pdf]
2016
[17] , and : Complete Elgot Monads and Coalgebraic Resumptions, In Electr. Notes Theor. Comput. Sci., 325, pp. 147–168, . [bibtex] [url]
2015
[16] , and : Unguarded Recursion on Coinductive Resumptions, In Proc. 31st Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXI), Electronic Notes in Theoretical Computer Science, vol. 319(), pp. 183 – 198, . [preprint] [bibtex] [url]
2014
[15] , , and : Monodic Fragments of Probabilistic First-order Logic, In Javier Esparza, Pierre Fraigniaud, Thore Husfeldt, Elias Koutsoupias, eds.: Proc. 41st International Colloquium on Automata, Languages, and Programming, ICALP 2014, Lecture Notes in Computer Science, vol. 8573, pp. 256–267, Springer, . The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-662-43951-7_22. [bibtex] [doi]
[14] and : Coalgebraic Weak Bisimulation from Recursive Equations over Monads, In Javier Esparza, Pierre Fraigniaud, Thore Husfeldt, Elias Koutsoupias, eds.: Automata, Languages, and Programming - 41st International Colloquium, ICALP 2014, Copenhagen, Denmark, July 8-11, 2014, Proceedings, Part II, Lecture Notes in Computer Science, vol. 8573, pp. 196–207, . The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-662-43951-7_17. [bibtex] [doi]
[13] , and : Towards a Coalgebraic Chomsky Hierarchy (Extended Abstract), In Josep Diaz, Ivan Lanese, Davide Sangiorgi, eds.: Proc. 8th IFIP TC 1/WG 2.2 International Conference on Theoretical Computer Science (TCS'14), Lecture Notes Comput. Sci., vol. 8705, pp. 265–280, Springer, . The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-662-44602-7_21. [bibtex] [doi]
2013
[12] and : A Relatively Complete Generic Hoare Logic for Order-Enriched Effects, In Proc. 28th Annual Symposium on Logic in Computer Science (LICS 2013), pp. 273–282, IEEE, . [bibtex] [pdf] [doi]
[11] and : A coinductive calculus for asynchronous side-effecting processes, In Information and Computation, 231(0), pp. 204 – 232, . [bibtex] [pdf] [doi]
[10] : Trace Semantics via Generic Observations, In Reiko Heckel, Stefan Milius, eds.: Algebra and Coalgebra in Computer Science (CALCO 2013), Lecture Notes in Computer Science, Springer, . The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-642-40206-7_13. [bibtex] [doi]
[9] , , and : Exploring the Boundaries of Monad Tensorability on Set, In Logical Methods in Computer Science, 9(3), . [bibtex] [url] [doi]
2011
[8] and : A Counterexample to Tensorability of Effects, In Andrea Corradini, Bartek Klin, eds.: Algebra and Coalgebra in Computer Science (CALCO 2011), Lecture Notes in Computer Science, Springer, . [bibtex]
[7] and : A coinductive calculus for asynchronous side-effecting processes, In Olaf Owe, Martin Steffen, Jan Arne Telle, eds.: Fundamentals of Computation Theory (FCT 2011), Lecture Notes in Computer Science, vol. 6914, Springer, . [bibtex] [url]
[6] and : Powermonads and Tensors of Unranked Effects, In Martin Grohe, ed.: Logic in Computer Science (LICS 2011), IEEE Computer Society, . [bibtex] [url]
2010
[5] , and : A Generic Complete Dynamic Logic for Reasoning about Purity and Effects, In Formal Aspects of Computing, 22(3-4), pp. 363–384, . [bibtex] [url]
[4] : Kleene monads, PhD thesis, Universität Bremen, . [pdf] [bibtex]
2009
[3] , and : Kleene Monads: Handling Iteration in a Framework of Generic Effects, In Alexander Kurz, Andrzej Tarlecki, eds.: Algebra and Coalgebra in Computer Science (CALCO 2009), Lecture Notes in Computer Science, vol. 5728, pp. 18–33, Springer, . [bibtex] [url]
2008
[2] , and : A generic complete dynamic logic for reasoning about purity and effects, In J. Fiadeiro, P. Inverardi, eds.: Fundamental Approaches to Software Engineering (FASE 2008), Lecture Notes in Computer Science, vol. 4961, pp. 199–214, Springer, . [bibtex] [url]
2006
[1] , and : Completeness of Global Evaluation Logic, In Rastislav Královič, Paweł Urzyczyn, eds.: Mathematical Foundations of Computer Science, Lecture Notes in Computer Science, vol. 4162, pp. 447–458, Springer, . [bibtex] [url]