activity
20242026
most citedBialgebraic Reasoning on Higher-Order Program Equivalence

4 citations · 8 across the 9 of their papers we have counts for

collaborators

11 papers

cs.LO2026

Compositionality in Coalgebraic Trace Semantics

Robin Jourde, Henning Urbat, Sergey Goncharov +2

A key requirement on any well-behaved process language is its compositionality: behavioural equivalence of processes should be respected by the constructors of the language. Turi a…

cs.LO2026

The Only Distributive Law Over the Powerset Monad Is the One You Know

Sergey Goncharov, Dirk Hofmann, Pedro Nora +2

Distributive laws of set functors over the powerset monad (also known as Kleisli laws for the powerset monad) are well-known to be in one-to-one correspondence with extensions of s…

cs.LO2025

Big Steps in Higher-Order Mathematical Operational Semantics

Sergey Goncharov, Pouya Partow, Stelios Tsampas

Small-step and big-step operational semantics are two fundamental styles of structural operational semantics (SOS), extensively used in practice. The former one is more fine-graine…

cs.PL2025

Bialgebraic Reasoning on Stateful Languages

Sergey Goncharov, Stefan Milius, Lutz Schröder +2

Reasoning about program equivalence in imperative languages is notoriously challenging, as the presence of states (in the form of variable stores) fundamentally increases the obser…

cs.LO2025

Relators and Notions of Simulation Revisited

Sergey Goncharov, Dirk Hofmann, Pedro Nora +2

Simulations and bisimulations are ubiquitous in the study of concurrent systems and modal logics of various types. Besides classical relational transition systems, relevant system…

cs.PL2024★ 3 cited

Abstract Operational Methods for Call-by-Push-Value

Sergey Goncharov, Stelios Tsampas, Henning Urbat

Levy's call-by-push-value is a comprehensive programming paradigm that combines elements from functional and imperative programming, supports computational effects and subsumes bot…

cs.LO2024

Identity-Preserving Lax Extensions and Where to Find Them

Sergey Goncharov, Dirk Hofmaan, Pedro Nora +2

Generic notions of bisimulation for various types of systems (nondeterministic, probabilistic, weighted etc.) rely on identity-preserving (normal) lax extensions of the functor enc…

cs.LO2024

A Unifying Categorical View of Nondeterministic Iteration and Tests

Sergey Goncharov, Tarmo Uustalu

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 reasonin…

cs.LO2024★ 1 cited

Higher-order bialgebraic semantics

Sergey Goncharov, Stefan Milius, Lutz Schröder +2

Compositionality proofs in higher-order languages are notoriously involved, and general semantic frameworks guaranteeing compositionality are hard to come by. In particular, Turi a…

cs.LO2024★ 4 cited

Bialgebraic Reasoning on Higher-Order Program Equivalence

Sergey Goncharov, Stefan Milius, Stelios Tsampas +1

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 n…

cs.LO2024

Logical Predicates in Higher-Order Mathematical Operational Semantics

Sergey Goncharov, Alessio Santamaria, Lutz Schröder +2

We present a systematic approach to logical predicates based on universal coalgebra and higher-order abstract GSOS, thus making a first step towards a unifying theory of logical re…