Search Results

Documents authored by Goncharov, Sergey

Document
DOI: 10.4230/LIPIcs.CONCUR.2024.25
A Unifying Categorical View of Nondeterministic Iteration and Tests

Authors: Sergey Goncharov and Tarmo Uustalu

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)

Abstract
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.
Cite as

Sergey Goncharov and Tarmo Uustalu. A Unifying Categorical View of Nondeterministic Iteration and Tests. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 25:1-25:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{goncharov_et_al:LIPIcs.CONCUR.2024.25,
  author =	{Goncharov, Sergey and Uustalu, Tarmo},
  title =	{{A Unifying Categorical View of Nondeterministic Iteration and Tests}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{25:1--25:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{311},
  editor =	{Majumdar, Rupak and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.25},
  URN =		{urn:nbn:de:0030-drops-207979},
  doi =		{10.4230/LIPIcs.CONCUR.2024.25},
  annote =	{Keywords: Kleene iteration, Elgot iteration, Kleene algebra, coalgebraic resumptions}
}
Document
Early Ideas
DOI: 10.4230/LIPIcs.CALCO.2023.24
Higher-Order Mathematical Operational Semantics (Early Ideas)

Authors: Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, and Henning Urbat

Published in: LIPIcs, Volume 270, 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)

Abstract
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.
Cite as

Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, and Henning Urbat. Higher-Order Mathematical Operational Semantics (Early Ideas). In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 24:1-24:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{goncharov_et_al:LIPIcs.CALCO.2023.24,
  author =	{Goncharov, Sergey and Milius, Stefan and Schr\"{o}der, Lutz and Tsampas, Stelios and Urbat, Henning},
  title =	{{Higher-Order Mathematical Operational Semantics}},
  booktitle =	{10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
  pages =	{24:1--24:3},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-287-7},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{270},
  editor =	{Baldan, Paolo and de Paiva, Valeria},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.24},
  URN =		{urn:nbn:de:0030-drops-188213},
  doi =		{10.4230/LIPIcs.CALCO.2023.24},
  annote =	{Keywords: Abstract GSOS, lambda-calculus, applicative bisimilarity, bialgebra}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2023.34
Representing Guardedness in Call-By-Value

Authors: Sergey Goncharov

Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)

Abstract
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.
Cite as

Sergey Goncharov. Representing Guardedness in Call-By-Value. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 34:1-34:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{goncharov:LIPIcs.FSCD.2023.34,
  author =	{Goncharov, Sergey},
  title =	{{Representing Guardedness in Call-By-Value}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{34:1--34:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.34},
  URN =		{urn:nbn:de:0030-drops-180181},
  doi =		{10.4230/LIPIcs.FSCD.2023.34},
  annote =	{Keywords: Fine-grain call-by-value, Abstract guardedness, Freyd category, Kleisli category, Elgot iteration}
}
Document
DOI: 10.4230/LIPIcs.CSL.2023.22
Quantitative Hennessy-Milner Theorems via Notions of Density

Authors: Jonas Forster, Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, and Paul Wild

Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)

Abstract
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.
Cite as

Jonas Forster, Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, and Paul Wild. Quantitative Hennessy-Milner Theorems via Notions of Density. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 22:1-22:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{forster_et_al:LIPIcs.CSL.2023.22,
  author =	{Forster, Jonas and Goncharov, Sergey and Hofmann, Dirk and Nora, Pedro and Schr\"{o}der, Lutz and Wild, Paul},
  title =	{{Quantitative Hennessy-Milner Theorems via Notions of Density}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{22:1--22:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.22},
  URN =		{urn:nbn:de:0030-drops-174836},
  doi =		{10.4230/LIPIcs.CSL.2023.22},
  annote =	{Keywords: Behavioural distances, coalgebra, characteristic modal logics, density, Hennessy-Milner theorems, quantale-enriched categories, Stone-Weierstra{\ss} theorems}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2022.30
Stateful Structural Operational Semantics

Authors: Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, and Henning Urbat

Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)

Abstract
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.
Cite as

Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, and Henning Urbat. Stateful Structural Operational Semantics. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 30:1-30:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{goncharov_et_al:LIPIcs.FSCD.2022.30,
  author =	{Goncharov, Sergey and Milius, Stefan and Schr\"{o}der, Lutz and Tsampas, Stelios and Urbat, Henning},
  title =	{{Stateful Structural Operational Semantics}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{30:1--30:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-233-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{228},
  editor =	{Felty, Amy P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.30},
  URN =		{urn:nbn:de:0030-drops-163111},
  doi =		{10.4230/LIPIcs.FSCD.2022.30},
  annote =	{Keywords: Structural Operational Semantics, Rule Formats, Distributive Laws}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2021.131
Uniform Elgot Iteration in Foundations

Authors: Sergey Goncharov

Published in: LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)

Abstract
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 iteration-based 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.
Cite as

Sergey Goncharov. Uniform Elgot Iteration in Foundations. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 131:1-131:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{goncharov:LIPIcs.ICALP.2021.131,
  author =	{Goncharov, Sergey},
  title =	{{Uniform Elgot Iteration in Foundations}},
  booktitle =	{48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
  pages =	{131:1--131:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-195-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{198},
  editor =	{Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.131},
  URN =		{urn:nbn:de:0030-drops-142007},
  doi =		{10.4230/LIPIcs.ICALP.2021.131},
  annote =	{Keywords: Elgot monad, partiality monad, delay monad, restriction category}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2020.24
Towards Constructive Hybrid Semantics

Authors: Tim Lukas Diezel and Sergey Goncharov

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

Abstract
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.
Cite as

Tim Lukas Diezel and Sergey Goncharov. Towards Constructive Hybrid Semantics. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 24:1-24:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{diezel_et_al:LIPIcs.FSCD.2020.24,
  author =	{Diezel, Tim Lukas and Goncharov, Sergey},
  title =	{{Towards Constructive Hybrid Semantics}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{24:1--24:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.24},
  URN =		{urn:nbn:de:0030-drops-123466},
  doi =		{10.4230/LIPIcs.FSCD.2020.24},
  annote =	{Keywords: Hybrid semantics, Elgot iteration, Homotopy type theory, Agda}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2019.13
Coinductive Resumption Monads: Guarded Iterative and Guarded Elgot

Authors: Paul Blain Levy and Sergey Goncharov

Published in: LIPIcs, Volume 139, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)

Abstract
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.
Cite as

Paul Blain Levy and Sergey Goncharov. Coinductive Resumption Monads: Guarded Iterative and Guarded Elgot. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 13:1-13:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{levy_et_al:LIPIcs.CALCO.2019.13,
  author =	{Levy, Paul Blain and Goncharov, Sergey},
  title =	{{Coinductive Resumption Monads: Guarded Iterative and Guarded Elgot}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{13:1--13:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-120-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{139},
  editor =	{Roggenbach, Markus and Sokolova, Ana},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.13},
  URN =		{urn:nbn:de:0030-drops-114414},
  doi =		{10.4230/LIPIcs.CALCO.2019.13},
  annote =	{Keywords: Guarded iteration, guarded monads, coalgebraic resumptions}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2018.22
A Semantics for Hybrid Iteration

Authors: Sergey Goncharov, Julian Jakob, and Renato Neves

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

Abstract
The recently introduced notions of guarded traced (monoidal) category and guarded (pre-)iterative monad aim at unifying different instances of partial iteration whilst keeping in touch with the established theory of total iteration and preserving its merits. In this paper we use these notions and the corresponding stock of results to examine different types of iteration for hybrid computations. As a starting point we use an available notion of hybrid monad restricted to the category of sets, and modify it in order to obtain a suitable notion of guarded iteration with guardedness interpreted as progressiveness in time - we motivate this modification by our intention to capture Zeno behaviour in an arguably general and feasible way. We illustrate our results with a simple programming language for hybrid computations and interpret it over the developed semantic foundations.
Cite as

Sergey Goncharov, Julian Jakob, and Renato Neves. A Semantics for Hybrid Iteration. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 22:1-22:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{goncharov_et_al:LIPIcs.CONCUR.2018.22,
  author =	{Goncharov, Sergey and Jakob, Julian and Neves, Renato},
  title =	{{A Semantics for Hybrid Iteration}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{22:1--22:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.22},
  URN =		{urn:nbn:de:0030-drops-95604},
  doi =		{10.4230/LIPIcs.CONCUR.2018.22},
  annote =	{Keywords: Elgot iteration, guarded iteration, hybrid monad, Zeno behaviour}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact