A coinductive calculus for asynchronous side-effecting processes - Goncharov, Sergey; Schröder, Lutz (Information and Computation, 2013)
We present an abstract framework for concurrent processes in which atomic steps have generic side effects, handled according to the principle of monadic encapsulation of effects. Processes in this framework are potentially infinite resumptions, modelled using final coalgebras over the monadic base. As a calculus for such processes, we introduce a concurrent extension of Moggi's monadic meta-language of effects. We establish soundness and completeness of a natural equational axiomatization of this calculus. Our main result is a corecursion scheme that is explicitly definable over the base language and provides flexible expressive means for the definition of new operators on processes, such as parallel composition. Moreover, we present initial results on verification methods for generic side-effecting processes. © 2013 Elsevier Inc.
UnivIS-Import:2015-03-09:Pub.2013.tech.IMMD.profes_1.acoind
Keywords: Coinduction; Computational meta-language; Computational monad; Corecursive scheme; Process algebra

A metalanguage for guarded iteration - Goncharov, Sergey; Rauch, Christoph; Schröder, Lutz (Theoretical Computer Science, 2021)
Notions of guardedness serve to delineate admissible recursive definitions in various settings in a compositional manner. In recent work, we have introduced an axiomatic notion of guardedness in symmetric monoidal categories, which serves as a unifying framework for various examples from program semantics, process algebra, and beyond. In the present paper, we propose a generic metalanguage for guarded iteration based on combining this notion with the fine-grain call-by-value paradigm, which we intend as a unifying programming language for guarded and unguarded iteration in the presence of computational effects. We give a generic (categorical) semantics of this language over a suitable class of strong monads supporting guarded iteration, and show it to be in touch with the standard operational behaviour of iteration by giving a concrete big-step operational semantics for a certain specific instance of the metalanguage and establishing soundness and (computational) adequacy for this case.
CRIS-Team Scopus Importer:2021-05-21
Keywords: Computational adequacy; Computational monads; Guarded iteration; Metalanguage

A Metalanguage for Guarded Iteration - Goncharov, Sergey; Rauch, Christoph; Schröder, Lutz (Theoretical Aspects of Computing - ICTAC 2018 (LNCS 11187), 2018)

An Adequate While-Language for Hybrid Computation - Goncharov, Sergey; Neves, Renato (Proceedings of the 21st International Symposium on Principles and Practice of Declarative Programming (PPDP 2019), 2019)
CRIS-Team WoS Importer:2020-04-24

A point-free perspective on lax extensions and predicate liftings - Goncharov, Sergey; Hofmann, Dirk; Nora, Pedro; Schröder, Lutz; Wild, Paul (Mathematical Structures in Computer Science, 2023)
Lax extensions of set functors play a key role in various areas, including topology, concurrent systems, and modal logic, while predicate liftings provide a generic semantics of modal operators. We take a fresh look at the connection between lax extensions and predicate liftings from the point of view of quantale-enriched relations. Using this perspective, we show in particular that various fundamental concepts and results arise naturally and their proofs become very elementary. Ultimately, we prove that every lax extension is induced by a class of predicate liftings; we discuss several implications of this result.
CRIS-Team Scopus Importer:2023-12-15
Keywords: coalgebraic modal logic; Kantorovich extension; Lax extension; Moss lifting

A Relatively Complete Generic Hoare Logic for Order-Enriched Effects - Goncharov, Sergey; Schröder, Lutz (Proc. 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, 2013)
Monads are the basis of a well-established method of encapsulating side-effects in semantics and programming. There have been a number of proposals for monadic program logics in the setting of plain monads, while much of the recent work on monadic semantics is concerned with monads on enriched categories, in particular in domain-theoretic settings, which allow for recursive monadic programs. Here, we lay out a definition of order-enriched monad which imposes cpo structure on the monad itself rather than on base category. Starting from the observation that order-enrichment of a monad induces a weak truth-value object, we develop a generic Hoare calculus for monadic side-effecting programs. For this calculus, we prove relative completeness via a calculus of weakest preconditions, which we also relate to strongest post conditions. © 2013 IEEE.
UnivIS-Import:2015-04-16:Pub.2013.tech.IMMD.profes_1.arelat
Keywords: computational effects; Hoare logic; monads; strongest postconditions; weakest preconditions

A Semantics for Hybrid Iteration - Goncharov, Sergey; Neves, Renato (29th International Conference on Concurrency Theory, CONCUR 2018, 2018)

A Unifying Categorical View of Nondeterministic Iteration and Tests - Goncharov, Sergey; Uustalu, Tarmo (35th International Conference on Concurrency Theory (CONCUR 2024), 2024)
We study Kleene iteration in the categorical context. A celebrated completeness result by Kozen introduced Kleene algebra (with tests) as a ubiquitous tool for lightweight reasoning about program equivalence, and yet, numerous variants of it came along afterwards to answer the demand for more refined flavors of semantics, such as stateful, concurrent, exceptional, hybrid, branching time, etc. We detach Kleene iteration from Kleene algebra and analyze it from the categorical perspective. The notion, we arrive at is that of Kleene-iteration category (with coproducts and tests), which we show to be general and robust in the sense of compatibility with programming language features, such as exceptions, store, concurrent behaviour, etc. We attest the proposed notion w.r.t. various yardsticks, most importantly, by characterizing the free model as a certain category of (nondeterministic) rational trees.
CRIS-Team Scopus Importer:2024-09-20
Keywords: coalgebraic resumptions; Elgot iteration; Kleene algebra; Kleene iteration

Bialgebraic Reasoning on Higher-order Program Equivalence - Goncharov, Sergey; Milius, Stefan; Tsampas, Stylianos; Urbat, Henning (Proceedings - Symposium on Logic in Computer Science, 2024)
Logical relations constitute a key method for reasoning about contextual equivalence of programs in higher-order languages. They are usually developed on a per-case basis, with a new theory required for each variation of the language or of the desired notion of equivalence. In the present paper we introduce a general construction of (step-indexed) logical relations at the level of Higher-Order Mathematical Operational Semantics, a highly parametric categorical framework for modeling the operational semantics of higherorder languages. Our main result states that for languages whose weak operational model forms a lax bialgebra, the logical relation is automatically sound for contextual equivalence. Our abstract theory is shown to instantiate to combinatory logics and λ-calculi with recursive types, and to different flavours of contextual equivalence.
CRIS-Team Scopus Importer:2024-07-26

Coalgebraic Weak Bisimulation from Recursive Equations over Monads - Goncharov, Sergey; Pattinson, Dirk (Proc. 41st International Colloquium on Automata, Languages, and Programming, 2014)
Strong bisimulation for labelled transition systems is one of the most fundamental equivalences in process algebra, and has been generalised to numerous classes of systems that exhibit richer transition behaviour. Nearly all of the ensuing notions are instances of the more general notion of coalgebraic bisimulation. Weak bisimulation, however, has so far been much less amenable to a coalgebraic treatment. Here we attempt to close this gap by giving a coalgebraic treatment of (parametrized) weak equivalences, including weak bisimulation. Our analysis requires that the functor defining the transition type of the system is based on a suitable order-enriched monad, which allows us to capture weak equivalences by least fixpoints of recursive equations. Our notion is in agreement with existing notions of weak bisimulations for labelled transition systems, probabilistic and weighted systems, and simple Segala systems. © 2014 Springer-Verlag.
UnivIS-Import:2015-04-17:Pub.2014.tech.IMMD.profes_1.coalge

Coinductive resumption monads: Guarded iterative and guarded Elgot - Levy, Paul Blain; Goncharov, Sergey (Leibniz International Proceedings in Informatics, LIPIcs, 2019)
We introduce a new notion of “guarded Elgot monad”, that is a monad equipped with a form of iteration. It requires every guarded morphism to have a specified fixpoint, and classical equational laws of iteration to be satisfied. This notion includes Elgot monads, but also further examples of partial non-unique iteration, emerging in the semantics of processes under infinite trace equivalence. We recall the construction of the “coinductive resumption monad” from a monad and endofunctor, that is used for modelling programs up to bisimilarity. We characterize this construction via a universal property: if the given monad is guarded Elgot, then the coinductive resumption monad is the guarded Elgot monad that freely extends it by the given endofunctor.
CRIS-Team Scopus Importer:2021-04-20
Keywords: Coalgebraic resumptions; Guarded iteration; Guarded monads

Complete Elgot Monads and Coalgebraic Resumptions - Goncharov, Sergey; Milius, Stefan; Rauch, Christoph (Electronic Notes in Theoretical Computer Science, 2016)
Monads are used to abstractly model a wide range of computational effects such as nondeterminism, statefulness, and exceptions. Complete Elgot monads are monads that are equipped with a (uniform) iteration operator satisfying a set of natural axioms, which allows to model iterative computations just as abstractly. It has been shown recently that extending complete Elgot monads with free effects (e.g. operations of sending/receiving messages over channels) canonically leads to generalized coalgebraic resumption monads, which were previously used as semantic domains for non-wellfounded guarded processes. In this paper, we continue the study of complete Elgot monads and their relationship with generalized coalgebraic resumption monads. We give a characterization of the Eilenberg-Moore algebras of the latter. In fact, we work more generally with Uustalu's parametrized monads; we introduce complete Elgot algebras for a parametrized monad and we prove that they form an Eilenberg-Moore category. This is further used for establishing a characterization of complete Elgot monads as those monads whose algebras are coherently equipped with the structure of complete Elgot algebras for the parametrized monads obtained from generalized coalgebraic resumption monads.
UnivIS-Import:2018-09-05:Pub.2016.tech.IMMD.profes_1.comple
Keywords: complete Elgot monads; complete Elgot algebras; resumption; coalgebra

Complete Elgot Monads and Coalgebraic Resumptions - Goncharov, Sergey; Milius, Stefan; Rauch, Christoph (MFPS XXXII, 2016)
<em style="border: 0px; font-size: 16px; margin: 0px; padding: 0px; vertical-align: baseline; font-family: Arial, Helvetica, "Lucida Sans Unicode", "Microsoft Sans Serif", "Segoe UI Symbol", STIXGeneral, "Cambria Math", "Arial Unicode MS", sans-serif; color: rgb(46, 46, 46); word-spacing: -1.24453px;">Monads<span style="color: rgb(46, 46, 46); font-family: Arial, Helvetica, "Lucida Sans Unicode", "Microsoft Sans Serif", "Segoe UI Symbol", STIXGeneral, "Cambria Math", "Arial Unicode MS", sans-serif; font-size: 16px; word-spacing: -1.24453px;"> are used to abstractly model a wide range of computational effects such as nondeterminism, statefulness, and exceptions. <em style="border: 0px; font-size: 16px; margin: 0px; padding: 0px; vertical-align: baseline; font-family: Arial, Helvetica, "Lucida Sans Unicode", "Microsoft Sans Serif", "Segoe UI Symbol", STIXGeneral, "Cambria Math", "Arial Unicode MS", sans-serif; color: rgb(46, 46, 46); word-spacing: -1.24453px;">Complete Elgot monads<span style="color: rgb(46, 46, 46); font-family: Arial, Helvetica, "Lucida Sans Unicode", "Microsoft Sans Serif", "Segoe UI Symbol", STIXGeneral, "Cambria Math", "Arial Unicode MS", sans-serif; font-size: 16px; word-spacing: -1.24453px;"> are monads that are equipped with a (<em style="border: 0px; font-size: 16px; margin: 0px; padding: 0px; vertical-align: baseline; font-family: Arial, Helvetica, "Lucida Sans Unicode", "Microsoft Sans Serif", "Segoe UI Symbol", STIXGeneral, "Cambria Math", "Arial Unicode MS", sans-serif; color: rgb(46, 46, 46); word-spacing: -1.24453px;">uniform<span style="color: rgb(46, 46, 46); font-family: Arial, Helvetica, "Lucida Sans Unicode", "Microsoft Sans Serif", "Segoe UI Symbol", STIXGeneral, "Cambria Math", "Arial Unicode MS", sans-serif; font-size: 16px; word-spacing: -1.24453px;">) <em style="border: 0px; font-size: 16px; margin: 0px; padding: 0px; vertical-align: baseline; font-family: Arial, Helvetica, "Lucida Sans Unicode", "Microsoft Sans Serif", "Segoe UI Symbol", STIXGeneral, "Cambria Math", "Arial Unicode MS", sans-serif; color: rgb(46, 46, 46); word-spacing: -1.24453px;">iteration operator<span style="color: rgb(46, 46, 46); font-family: Arial, Helvetica, "Lucida Sans Unicode", "Microsoft Sans Serif", "Segoe UI Symbol", STIXGeneral, "Cambria Math", "Arial Unicode MS", sans-serif; font-size: 16px; word-spacing: -1.24453px;"> satisfying a set of natural axioms, which allows to model <em style="border: 0px; font-size: 16px; margin: 0px; padding: 0px; vertical-align: baseline; font-family: Arial, Helvetica, "Lucida Sans Unicode", "Microsoft Sans Serif", "Segoe UI Symbol", STIXGeneral, "Cambria Math", "Arial Unicode MS", sans-serif; color: rgb(46, 46, 46); word-spacing: -1.24453px;">iterative computations<span style="color: rgb(46, 46, 46); font-family: Arial, Helvetica, "Lucida Sans Unicode", "Microsoft Sans Serif", "Segoe UI Symbol", STIXGeneral, "Cambria Math", "Arial Unicode MS", sans-serif; font-size: 16px; word-spacing: -1.24453px;"> just as abstractly. It has been shown recently that extending complete Elgot monads with free effects (e.g. operations of sending/receiving messages over channels) canonically leads to <em style="border: 0px; font-size: 16px; margin: 0px; padding: 0px; vertical-align: baseline; font-family: Arial, Helvetica, "Lucida Sans Unicode", "Microsoft Sans Serif", "Segoe UI Symbol", STIXGeneral, "Cambria Math", "Arial Unicode MS", sans-serif; color: rgb(46, 46, 46); word-spacing: -1.24453px;">generalized coalgebraic resumption monads<span style="color: rgb(46, 46, 46); font-family: Arial, Helvetica, "Lucida Sans Unicode", "Microsoft Sans Serif", "Segoe UI Symbol", STIXGeneral, "Cambria Math", "Arial Unicode MS", sans-serif; font-size: 16px; word-spacing: -1.24453px;">, which were previously used as semantic domains for non-wellfounded guarded processes. In this paper, we continue the study of complete Elgot monads and their relationship with generalized coalgebraic resumption monads. We give a characterization of the Eilenberg-Moore algebras of the latter. In fact, we work more generally with Uustalu's <em style="border: 0px; font-size: 16px; margin: 0px; padding: 0px; vertical-align: baseline; font-family: Arial, Helvetica, "Lucida Sans Unicode", "Microsoft Sans Serif", "Segoe UI Symbol", STIXGeneral, "Cambria Math", "Arial Unicode MS", sans-serif; color: rgb(46, 46, 46); word-spacing: -1.24453px;">parametrized monads<span style="color: rgb(46, 46, 46); font-family: Arial, Helvetica, "Lucida Sans Unicode", "Microsoft Sans Serif", "Segoe UI Symbol", STIXGeneral, "Cambria Math", "Arial Unicode MS", sans-serif; font-size: 16px; word-spacing: -1.24453px;">; we introduce complete Elgot algebras for a parametrized monad and we prove that they form an Eilenberg-Moore category. This is further used for establishing a characterization of complete Elgot monads as those monads whose algebras are coherently equipped with the structure of complete Elgot algebras for the parametrized monads obtained from generalized coalgebraic resumption monads.
Keywords: Complete Elgot monad; complete Elgot algebra; resumption monad; uniform iteration

Exploring the Boundaries of Monad Tensorability on Set - Bowler, Nathan; Goncharov, Sergey; Levy, Paul; Schröder, Lutz (Logical Methods in Computer Science, 2013)
We study a composition operation on monads, equivalently presented as large equational theories. Specifically, we discuss the existence of tensors, which are combinations of theories that impose mutual commutation of the operations from the component theories. As such, they extend the sum of two theories, which is just their unrestrained combination. Tensors of theories arise in several contexts; in particular, in the semantics of programming languages, the monad transformer for global state is given by a tensor. We present two main results: we show that the tensor of two monads need not in general exist by presenting two counterexamples, one of them involving finite powerset (i.e. the theory of join semilattices); this solves a somewhat long-standing open problem, and contrasts with recent results that had ruled out previously expected counterexamples. On the other hand, we show that tensors with bounded powerset monads do exist from countable powerset upwards. © N. Bowler, S. Goncharov, P. B. Levy, and L. Schröder.
UnivIS-Import:2015-03-09:Pub.2013.tech.IMMD.profes_1.explor
Keywords: Monads; Non-determinism; Side effects; Tensor products

Generic Hoare Logic for Order-Enriched Effects with Exceptions - Rauch, Christoph; Goncharov, Sergey; Schröder, Lutz (Recent Trends in Algebraic Development Techniques: 23rd IFIP WG 1.3 International Workshop, WADT 2016, Revised Selected Papers, 2017)

Guarded and Unguarded Iteration for Generalized Processes - Goncharov, Sergey; Schröder, Lutz; Rauch, Christoph; Pirog, Maciej (Logical Methods in Computer Science, 2019)
Models of iterated computation, such as (completely) iterative monads, often depend on a notion of guardedness, which guarantees unique solvability of recursive equations and requires roughly that recursive calls happen only under certain guarding operations. On the other hand, many models of iteration do admit unguarded iteration. Solutions are then no longer unique, and in general not even determined as least or greatest fixpoints, being instead governed by quasi-equational axioms. Monads that support unguarded iteration in this sense are called (complete) Elgot monads. Here, we propose to equip (Kleisli categories of) monads with an abstract notion of guardedness and then require solvability of abstractly guarded recursive equations; examples of such abstractly guarded pre-iterative monads include both iterative monads and Elgot monads, the latter by deeming any recursive definition to be abstractly guarded. Our main result is then that Elgot monads are precisely the iteration-congruent retracts of abstractly guarded iterative monads, the latter being defined as admitting unique solutions of abstractly guarded recursive equations; in other words, models of unguarded iteration come about by quotienting models of guarded iteration.
CRIS-Team WoS Importer:2019-08-13

Guarded Traced Categories - Goncharov, Sergey; Schröder, Lutz (21st International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2018 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, 2018)

Higher-Order Mathematical Operational Semantics - Goncharov, Sergey; Milius, Stefan; Schröder, Lutz; Tsampas, Stylianos; Urbat, Henning (Leibniz International Proceedings in Informatics, LIPIcs, 2023)
We present a higher-order extension of Turi and Plotkin's abstract GSOS framework that retains the key feature of the latter: for every language whose operational rules are represented by a higher-order GSOS law, strong bisimilarity on the canonical operational model is a congruence with respect to the operations of the language. We further extend this result to weak (bi-)similarity, for which a categorical account of Howe's method is developed. It encompasses, for instance, Abramsky's classical compositionality theorem for applicative similarity in the untyped λ-calculus. In addition, we give first steps of a theory of logical relations at the level of higher-order abstract GSOS.
CRIS-Team Scopus Importer:2023-10-06
Keywords: Abstract GSOS; applicative bisimilarity; bialgebra; lambda-calculus

Implementing Hybrid Semantics: From Functional to Imperative - Goncharov, Sergey; Neves, Renato; Proença, José (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2020)
Hybrid programs combine digital control with differential equations, and naturally appear in a wide range of application domains, from biology and control theory to real-time software engineering. The entanglement of discrete and continuous behaviour inherent to such programs goes beyond the established computer science foundations, producing challenges related to e.g. infinite iteration and combination of hybrid behaviour with other effects. A systematic treatment of hybridness as a dedicated computational effect has emerged recently. In particular, a generic idealized functional language HybCore with a sound and adequate operational semantics has been proposed. The latter semantics however did not provide hints to implementing HybCore as a runnable language, suitable for hybrid system simulation (e.g. the semantics features rules with uncountably many premises). We introduce an imperative counterpart of HybCore, whose semantics is simpler and runnable, and yet intimately related with the semantics of HybCore at the level of hybrid monads. We then establish a corresponding soundness and adequacy theorem. To attest that the resulting semantics can serve as a firm basis for the implementation of typical tools of programming oriented to the hybrid domain, we present a web-based prototype implementation to evaluate and inspect hybrid programs, in the spirit of GHCi for Haskell and UTop for OCaml. The major asset of our implementation is that it formally follows the operational semantic rules.
CRIS-Team Scopus Importer:2020-12-25

Kantorovich Functors and Characteristic Logics for Behavioural Distances - Goncharov, Sergey; Hofmann, Dirk; Nora, Pedro; Schröder, Lutz; Wild, Paul (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2023)
Behavioural distances measure the deviation between states in quantitative systems, such as probabilistic or weighted systems. There is growing interest in generic approaches to behavioural distances. In particular, coalgebraic methods capture variations in the system type (nondeterministic, probabilistic, game-based etc.), and the notion of quantale abstracts over the actual values distances take, thus covering, e.g., two-valued equivalences, (pseudo)metrics, and probabilistic (pseudo)metrics. Coalgebraic behavioural distances have been based either on liftings of Set -functors to categories of metric spaces, or on lax extensions of Set -functors to categories of quantitative relations. Every lax extension induces a functor lifting but not every lifting comes from a lax extension. It was shown recently that every lax extension is Kantorovich, i.e. induced by a suitable choice of monotone predicate liftings, implying via a quantitative coalgebraic Hennessy-Milner theorem that behavioural distances induced by lax extensions can be characterized by quantitative modal logics. Here, we essentially show the same in the more general setting of behavioural distances induced by functor liftings. In particular, we show that every functor lifting, and indeed every functor on (quantale-valued) metric spaces, that preserves isometries is Kantorovich, so that the induced behavioural distance (on systems of suitably restricted branching degree) can be characterized by a quantitative modal logic.
CRIS-Team Scopus Importer:2023-08-04

Local Local Reasoning: A BI-Hyperdoctrine for Full Ground Store - Polzer, Miriam; Goncharov, Sergey (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2020)
Modelling and reasoning about dynamic memory allocation is one of the well-established strands of theoretical computer science, which is particularly well-known as a source of notorious challenges in semantics, reasoning, and proof theory. We capitalize on recent progress on categorical semantics of full ground store, in terms of a full ground store monad, to build a corresponding semantics of a higher order logic over the corresponding programs. Our main result is a construction of an (intuitionistic) BI-hyperdoctrine, which is arguably the semantic core of higher order logic over local store. Although we have made an extensive use of the existing generic tools, certain principled changes had to be made to enable the desired construction: while the original monad works over total heaps (to disable dangling pointers), our version involves partial heaps (heaplets) to enable compositional reasoning using separating conjunction. Another remarkable feature of our construction is that, in contrast to the existing generic approaches, our BI-algebra does not directly stem from an internal categorical partial commutative monoid.
CRIS-Team Scopus Importer:2020-05-08

Monodic Fragments of Probabilistic First-order Logic - Jung, Jean Christoph; Lutz, Carsten; Goncharov, Sergey; Schröder, Lutz (Proc. 41st International Colloquium on Automata, Languages, and Programming, 2014)
By classical results of Abadi and Halpern, validity for probabilistic first-order logic of type 2 (ProbFO) is Π1 2-complete and thus not recursively enumerable, and even small fragments of ProbFO are undecidable. In temporal first-order logic, which has similar computational properties, these problems have been addressed by imposing monodicity, that is, by allowing temporal operators to be applied only to formulas with at most one free variable. In this paper, we identify a monodic fragment of ProbFO and show that it enjoys favorable computational properties. Specifically, the valid sentences of monodic ProbFO are recursively enumerable and a slight variation of Halpern's axiom system for type-2 ProbFO on bounded domains is sound and complete for monodic ProbFO. Moreover, decidability can be obtained by restricting the FO part of monodic ProbFO to any decidable FO fragment. In some cases, which notably include the guarded fragment, our general constructions result in tight complexity bounds. © 2014 Springer-Verlag.
UnivIS-Import:2015-04-17:Pub.2014.tech.IMMD.profes_1.monodi

Quantitative Hennessy-Milner Theorems via Notions of Density - Forster, Jonas; Goncharov, Sergey; Hofmann, Dirk; Nora, Pedro; Schröder, Lutz; Wild, Paul (Leibniz International Proceedings in Informatics, LIPIcs, 2023)
The classical Hennessy-Milner theorem is an important tool in the analysis of concurrent processes; it guarantees that any two non-bisimilar states in finitely branching labelled transition systems can be distinguished by a modal formula. Numerous variants of this theorem have since been established for a wide range of logics and system types, including quantitative versions where lower bounds on behavioural distance (e.g. in weighted, metric, or probabilistic transition systems) are witnessed by quantitative modal formulas. Both the qualitative and the quantitative versions have been accommodated within the framework of coalgebraic logic, with distances taking values in quantales, subject to certain restrictions, such as being so-called value quantales. While previous quantitative coalgebraic Hennessy-Milner theorems apply only to liftings of set functors to (pseudo)metric spaces, in the present work we provide a quantitative coalgebraic Hennessy-Milner theorem that applies more widely to functors native to metric spaces; notably, we thus cover, for the first time, the well-known Hennessy-Milner theorem for continuous probabilistic transition systems, where transitions are given by Borel measures on metric spaces, as an instance of such a general result. In the process, we also relax the restrictions imposed on the quantale, and additionally parametrize the technical account over notions of closure and, hence, density, providing associated variants of the Stone-Weierstraß theorem; this allows us to cover, for instance, behavioural ultrametrics.
CRIS-Team Scopus Importer:2023-03-03
Keywords: Behavioural distances; characteristic modal logics; coalgebra; density; Hennessy-Milner theorems; quantale-enriched categories; Stone-Weierstraß theorems

Representing Guardedness in Call-By-Value - Goncharov, Sergey (Leibniz International Proceedings in Informatics, LIPIcs, 2023)
Like the notion of computation via (strong) monads serves to classify various flavours of impurity, including exceptions, non-determinism, probability, local and global store, the notion of guardedness classifies well-behavedness of cycles in various settings. In its most general form, the guardedness discipline applies to general symmetric monoidal categories and further specializes to Cartesian and co-Cartesian categories, where it governs guarded recursion and guarded iteration respectively. Here, even more specifically, we deal with the semantics of call-by-value guarded iteration. It was shown by Levy, Power and Thielecke that call-by-value languages can be generally interpreted in Freyd categories, but in order to represent effectful function spaces, such a category must canonically arise from a strong monad. We generalize this fact by showing that representing guarded effectful function spaces calls for certain parametrized monads (in the sense of Uustalu). This provides a description of guardedness as an intrinsic categorical property of programs, complementing the existing description of guardedness as a predicate on a category.
CRIS-Team Scopus Importer:2023-08-11
Keywords: Abstract guardedness; Elgot iteration; Fine-grain call-by-value; Freyd category; Kleisli category

Shades of Iteration: From Elgot to Kleene - Goncharov, Sergey (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2023)
Notions of iteration range from the arguably most general Elgot iteration to a very specific Kleene iteration. The fundamental nature of Elgot iteration has been extensively explored by Bloom and Esik in the form of iteration theories, while Kleene iteration became extremely popular as an integral part of (untyped) formalisms, such as automata theory, regular expressions and Kleene algebra. Here, we establish a formal connection between Elgot iteration and Kleene iteration in the form of Elgot monads and Kleene monads, respectively. We also introduce a novel class of while-monads, which like Kleene monads admit a relatively simple description in algebraic terms. Like Elgot monads, while-monads cover a large variety of models that meaningfully support while-loops, but may fail the Kleene algebra laws, or even fail to support a Kleen iteration operator altogether.
CRIS-Team Scopus Importer:2023-11-17

Stateful Structural Operational Semantics - Goncharov, Sergey; Milius, Stefan; Schröder, Lutz; Tsampas, Stelios; Urbat, Henning (Leibniz International Proceedings in Informatics, LIPIcs, 2022)
Compositionality of denotational semantics is an important concern in programming semantics. Mathematical operational semantics in the sense of Turi and Plotkin guarantees compositionality, but seen from the point of view of stateful computation it applies only to very fine-grained equivalences that essentially assume unrestricted interference by the environment between any two statements. We introduce the more restrictive stateful SOS rule format for stateful languages. We show that compositionality of two more coarse-grained semantics, respectively given by assuming read-only interference or no interference between steps, remains an undecidable property even for stateful SOS. However, further restricting the rule format in a manner inspired by the cool GSOS formats of Bloom and van Glabbeek, we obtain the streamlined and cool stateful SOS formats, which respectively guarantee compositionality of the two more abstract equivalences.
CRIS-Team Scopus Importer:2022-07-22
Keywords: Distributive Laws; Rule Formats; Structural Operational Semantics

Toward a Uniform Theory of Effectful State Machines - Goncharov, Sergey; Milius, Stefan; Silva, Alexandra (ACM Transactions on Computational Logic, 2020)
Using recent developments in coalgebraic and monad-based semantics, we present a uniform study of various notions of machines, e.g., finite state machines, multi-stack machines, Turing machines, valence automata, and weighted automata. They are instances of Jacobs's notion of a T-automaton, where T is a monad. We show that the generic language semantics for T-automata correctly instantiates the usual language semantics for a number of known classes of machines/languages, including regular, context-free, recursively-enumerable, and various subclasses of context free languages (e.g., deterministic and real-time ones). Moreover, our approach provides new generic techniques for studying the expressivity power of various machine-based models.
CRIS-Team Scopus Importer:2020-06-05
Keywords: bialgebraic semantics; coalgebras; Kleene theorem; Monads; side-effects

Towards a Coalgebraic Chomsky Hierarchy - Goncharov, Sergey; Milius, Stefan; Silva, Alexandra (Proc. 8th IFIP TC 1/WG 2.2 International Conference on Theoretical Computer Science, 2014)
UnivIS-Import:2015-04-17:Pub.2014.tech.IMMD.profes_1.toward

Towards a Higher-Order Mathematical Operational Semantics - Goncharov, Sergey; Milius, Stefan; Schröder, Lutz; Tsampas, Stelios; Urbat, Henning (Proceedings of the ACM on Programming Languages, 2023)
Compositionality proofs in higher-order languages are notoriously involved, and general semantic frameworks guaranteeing compositionality are hard to come by. In particular, Turi and Plotkin's bialgebraic abstract GSOS framework, which has been successfully applied to obtain off-The-shelf compositionality results for first-order languages, so far does not apply to higher-order languages. In the present work, we develop a theory of abstract GSOS specifications for higher-order languages, in effect transferring the core principles of Turi and Plotkin's framework to a higher-order setting. In our theory, the operational semantics of higher-order languages is represented by certain dinatural transformations that we term pointed higher-order GSOS laws. We give a general compositionality result that applies to all systems specified in this way and discuss how compositionality of the SKI calculus and the λ-calculus w.r.t. a strong variant of Abramsky's applicative bisimilarity are obtained as instances.
CRIS-Team Scopus Importer:2023-02-03
Keywords: Abstract GSOS; Categorical semantics; Higher-order reasoning

Towards constructive hybrid semantics - Diezel, Tim Lukas; Goncharov, Sergey (Leibniz International Proceedings in Informatics, LIPIcs, 2020)
With hybrid systems becoming ever more pervasive, the underlying semantic challenges emerge in their entirety. The need for principled semantic foundations has been recognized previously in the case of discrete computation and discrete data, with subsequent implementations in programming languages and proof assistants. Hybrid systems, contrastingly, do not directly fit into the classical semantic paradigms due to the presence of quite specific “non-programmable” features, such as Zeno behaviour and the inherent indispensable reliance on a notion of continuous time. Here, we analyze the phenomenon of hybrid semantics from a constructive viewpoint. In doing so, we propose a monad-based semantics, generic over a given ordered monoid representing the time domain, hence abstracting from the monoid of constructive reals. We implement our construction as a higher inductive-inductive type in the recent cubical extension of the Agda proof assistant, significantly using state-of-the-art advances of homotopy type theory. We show that classically, i.e. under the axiom of choice, our construction admits a charaterization in terms of directed sequence completion.
CRIS-Team Scopus Importer:2021-04-19
Keywords: Agda; Elgot iteration; Homotopy type theory; Hybrid semantics

Trace Semantics via Generic Observations - Goncharov, Sergey (Proc. 5th Conference on Algebra and Coalgebra in Computer Science, CALCO 2013, 2013)
Recent progress on defining abstract trace semantics for coalgebras rests upon two observations: (i) coalgebraic bisimulation for deterministic automata coincides with trace equivalence, and (ii) the classical powerset construction for automata determinization instantiates the generic idea of lifting a functor to the Eilenberg-Moore category of an appropriate monad. We take this approach one step further by rebasing the latter kind of trace semantics on the novel notion of T-observer, which is just a certain natural transformation of the form F → GT, and thus allowing for elimination of assumptions about the structure of the coalgebra functor. As a specific application of this idea we demonstrate how it can be used for capturing trace semantics of push-down automata. Furthermore, we show how specific forms of observers can be used for coalgebra-based treatment of internal automata transitions as well as weak bisimilarity of processes.
UnivIS-Import:2015-04-16:Pub.2013.tech.IMMD.profes_1.traces

Unguarded Recursion on Coinductive Resumptions - Goncharov, Sergey; Rauch, Christoph; Schröder, Lutz (Mathematical Foundations of Programming Semantics XXXI, MFPS 2015, 2015)
We study a model of side-effecting processes obtained by adjoining free operations to a monad modelling base effects by means of a cofree coalgebra construction; one thus arrives at what one may think of as types of non-wellfounded side-effecting trees, generalizing the infinite resumption monad. Types of this kind have received some attention in the recent literature; in particular, it has been shown that they admit guarded iteration. Here, we show that they also admit unguarded iteration, i.e. form complete Elgot monads, provided that the underlying base effect supports unguarded iteration.
Keywords: recursion; coalgebra; coinduction; complete Elgot monad; resumptions

Unguarded Recursion on Coinductive Resumptions - Goncharov, Sergey; Schröder, Lutz; Rauch, Christoph; Jakob, Julian (Logical Methods in Computer Science, 2018)
We study a model of side-effecting processes obtained by starting from a monad modelling base effects and adjoining free operations using a cofree coalgebra construction; one thus arrives at what one may think of as types of non-wellfounded side-effecting trees, generalizing the infinite resumption monad. Correspondingly, the arising monad transformer has been termed the coinductive generalized resumption transformer. Monads of this kind have received some attention in the recent literature; in particular, it has been shown that they admit guarded iteration. Here, we show that they also admit unguarded iteration, i.e. form complete Elgot monads, provided that the underlying base effect supports unguarded iteration. Moreover, we provide a universal characterization of the coinductive resumption monad transformer in terms of coproducts of complete Elgot monad
Keywords: recursion; coalgebra; coinduction; complete Elgot monad; resumptions

Uniform elgot iteration in foundations - Goncharov, Sergey (Leibniz International Proceedings in Informatics, LIPIcs, 2021)
Category theory is famous for its innovative way of thinking of concepts by their descriptions, in particular by establishing universal properties. Concepts that can be characterized in a universal way receive a certain quality seal, which makes them easily transferable across application domains. The notion of partiality is however notoriously difficult to characterize in this way, although the importance of it is certain, especially for computer science where entire research areas, such as synthetic and axiomatic domain theory revolve around it. More recently, this issue resurfaced in the context of (constructive) intensional type theory. Here, we provide a generic categorical iterationbased notion of partiality, which is arguably the most basic one. We show that the emerging free structures, which we dub uniform-iteration algebras enjoy various desirable properties, in particular, yield an equational lifting monad. We then study the impact of classicality assumptions and choice principles on this monad, in particular, we establish a suitable categorial formulation of the axiom of countable choice entailing that the monad is an Elgot monad.
CRIS-Team Scopus Importer:2021-10-01
Keywords: Delay monad; Elgot monad; Partiality monad; Restriction category

Unifying Guarded and Unguarded Iteration - Goncharov, Sergey; Schröder, Lutz; Rauch, Christoph; Piróg, Maciej (Proceedings of the 20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2017), 2017)
Keywords: Recursion theory; equational theories; guarded recursion

Weak Similarity in Higher-Order Mathematical Operational Semantics - Urbat, Henning; Tsampas, Stelios; Goncharov, Sergey; Milius, Stefan; Schröder, Lutz (Proceedings - Symposium on Logic in Computer Science, 2023)
Higher-order abstract GSOS is a recent extension of Turi and Plotkin's framework of Mathematical Operational Semantics to higher-order languages. The fundamental well-behavedness property of all specifications within the framework is that coalgebraic strong (bi)similarity on their operational model is a congruence. In the present work, we establish a corresponding congruence theorem for weak similarity, which is shown to instantiate to well-known concepts such as Abramsky's applicative similarity for the λ-calculus. On the way, we develop several techniques of independent interest at the level of abstract categories, including relation liftings of mixed-variance bifunctors and higher-order GSOS laws, as well as Howe's method.
CRIS-Team Scopus Importer:2023-08-11
Keywords: Computer science; Semantics; Mathematical models