Abstract Operational Methods for Call-by-Push-Value - Goncharov, Sergey; Tsampas, Stylianos; Urbat, Henning (Proceedings of the ACM on Programming Languages, 2025)
Levy's call-by-push-value is a comprehensive programming paradigm that combines elements from functional and imperative programming, supports computational effects and subsumes both call-by-value and call-by-name evaluation strategies. In the present work, we develop modular methods to reason about program equivalence in call-by-push-value, and in fine-grain call-by-value, which is a popular lightweight call-by-value sublanguage of the former. Our approach is based on the fundamental observation that presheaf categories of sorted sets are suitable universes to model call-by-(push)-value languages, and that natural, coalgebraic notions of program equivalence such as applicative similarity and logical relations can be developed within. Starting from this observation, we formalize fine-grain call-by-value and call-by-push-value in the higher-order abstract GSOS framework, reduce their key congruence properties to simple syntactic conditions by leveraging existing theory and argue that introducing changes to either language incurs minimal proof overhead.
CRIS-Team Scopus Importer:2025-01-31
Keywords: Call-by-push-value; Categorical semantics; Higher-order Abstract GSOS

A Categorical Approach to Syntactic Monoids - Adámek, Jiří; Milius, Stefan; Urbat, Henning (Logical Methods in Computer Science, 2018)

A characterisation of NL/poly via nondeterministic finite automata - Myers, Robert; Urbat, Henning (15th International Workshop on Descriptional Complexity of Formal Systems, DCFS 2013, 2013)

A fibrational approach to automata theory - Urbat, Henning; Chen, Liang-Ting (6th Conference on Algebra and Coalgebra in Computer Science, CALCO 2015, 2015)
Keywords: Coalgebra; Duality; Eilenberg's variety theorem; Grothendieck fibration

Automata Learning: An Algebraic Approach - Urbat, Henning; Schröder, Lutz (ACM International Conference Proceeding Series, 2020)
We propose a generic categorical framework for learning unknown formal languages of various types (e.g. finite or infinite words, weighted and nominal languages). Our approach is parametric in a monad T that represents the given type of languages and their recognizing algebraic structures. Using the concept of an automata presentation of T-algebras, we demonstrate that the task of learning a T-recognizable language can be reduced to learning an abstract form of algebraic automaton whose transitions are modeled by a functor. For the important case of adjoint automata, we devise a learning algorithm generalizing Angluin's L∗. The algorithm is phrased in terms of categorically described extension steps; we provide for a termination and complexity analysis based on a dedicated notion of finiteness. Our framework applies to structures like ω-regular languages that were not within the scope of existing categorical accounts of automata learning. In addition, it yields new learning algorithms for several types of languages for which no such algorithms were previously known at all, including sorted languages, nominal languages with name binding, and cost functions.
CRIS-Team Scopus Importer:2020-06-16
Keywords: Algebras; Automata Learning; Monads

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

Canonical Nondeterministic Automata - Myers, Robert; Adámek, Jiří; Milius, Stefan; Urbat, Henning; Urbat, Henning (Coalgebraic Methods in Computer Science, 2014)
For each regular language we describe a family of canonical nondeterministic acceptors (nfas). Their construction follows a uniform recipe: build the minimal dfa for in a locally finite variety , and apply an equivalence between the finite -algebras and a category of finite structured sets and relations. By instantiating this to different varieties we recover three well-studied canonical nfas (the átomaton, the jiromaton and the minimal xor automaton) and obtain a new canonical nfa called the distromaton. We prove that each of these nfas is minimal relative to a suitable measure, and give conditions for state-minimality. Our approach is coalgebraic, exhibiting additional structure and universal properties. © 2014 IFIP International Federation for Information Processing.
UnivIS-Import:2015-04-17:Pub.2014.tech.IMMD.profes_1.canoni

Coalgebraic Constructions of Canonical Nondeterministic Automata - Myers, Robert; Adámek, Jiří; Milius, Stefan; Urbat, Henning; Urbat, Henning (Theoretical Computer Science, 2015)
UnivIS-Import:2016-06-01:Pub.2015.tech.IMMD.profes_1.coalge
Keywords: Coalgebras; Join-semilattices; Minimization; Non-deterministic automata

Eilenberg's variety theorem without Boolean operations - Birkmann, Fabian; Milius, Stefan; Urbat, Henning (Information and Computation, 2022)
Eilenberg's variety theorem marked a milestone in the algebraic theory of regular languages by establishing a formal correspondence between properties of regular languages and properties of finite monoids recognizing them. Motivated by classes of languages accepted by quantum finite automata, we introduce basic varieties of regular languages, a weakening of Eilenberg's original concept that does not require closure under any boolean operations, and prove a variety theorem for them. To do so, we investigate the algebraic recognition of languages by lattice bimodules, generalizing Klíma and Polák's lattice algebras, and we utilize the duality between algebraic completely distributive lattices and posets.
CRIS-Team Scopus Importer:2022-05-20
Keywords: Eilenberg's theorem; Pseudovariety; Quantum finite automata; Variety of regular languages

Equational Axiomatization of Algebras with Structure - Milius, Stefan; Urbat, Henning (22nd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2019), 2019)
This paper proposes a new category theoretic account of equationally axiomatizable classes of algebras. Our approach is well-suited for the treatment of algebras equipped with additional computationally relevant structure, such as ordered algebras, continuous algebras, quantitative algebras, nominal algebras, or profinite algebras. Our main contributions are a generic HSP theorem and a sound and complete equational logic, which are shown to encompass numerous flavors of equational axiomizations studied in the literature.
CRIS-Team Scopus Importer:2019-05-09

Finite behaviours and finitary corecursion - Urbat, Henning (7th Conference on Algebra and Coalgebra in Computer Science, CALCO 2017, 2017)
Keywords: Completely iterative algebra; Fg-iterative algebra; Iterative algebra; Iterative monad; Rational fixpoint; Terminal coalgebra

Generalized Eilenberg Theorem I: Local Varieties of Languages - Adámek, Jiří; Milius, Stefan; Myers, Robert; Urbat, Henning; Urbat, Henning (Foundations of Software Science and Computation Structures, 2014)
We investigate the duality between algebraic and coalgebraic recognition of languages to derive a generalization of the local version of Eilenberg's theorem. This theorem states that the lattice of all boolean algebras of regular languages over an alphabet Σ closed under derivatives is isomorphic to the lattice of all pseudovarieties of Σ-generated monoids. By applying our method to different categories, we obtain three related results: one, due to Gehrke, Grigorieff and Pin, weakens boolean algebras to distributive lattices, one due to Polák weakens them to join-semilattices, and the last one considers vector spaces over ℤ2. © 2014 Springer-Verlag.
UnivIS-Import:2015-04-17:Pub.2014.tech.IMMD.profes_1.genera

Generalized Eilenberg Theorem: Varieties of Languages in a Category - Adámek, Jiří; Milius, Stefan; Myers, Robert; Urbat, Henning (ACM Transactions on Computational Logic, 2019)

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

Monoidal Extended Stone Duality - Birkmann, Fabian; Urbat, Henning; Milius, Stefan (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2024)
Extensions of Stone-type dualities have a long history in algebraic logic and have also been instrumental for proving results in algebraic language theory. We show how to extend abstract categorical dualities via monoidal adjunctions, subsuming various incarnations of classical extended Stone and Priestley duality as a special case. Guided by these categorical foundations, we investigate residuation algebras, which are algebraic models of language derivatives, and show the subcategory of derivation algebras to be dually equivalent to the category of profinite ordered monoids, restricting to a duality between boolean residuation algebras and profinite monoids. We further extend this duality to capture relational morphisms of profinite ordered monoids, which dualize to natural morphisms of residuation algebras.
CRIS-Team Scopus Importer:2024-06-21
Keywords: Profinite Monoids; Regular Languages; Stone Duality

Nominal Büchi Automata with Name Allocation - Urbat, Henning; Hausmann, Daniel; Milius, Stefan; Schröder, Lutz (Leibniz International Proceedings in Informatics, LIPIcs, 2021)
Infinite words over infinite alphabets serve as models of the temporal development of the allocation and (re-)use of resources over linear time. We approach ω-languages over infinite alphabets in the setting of nominal sets, and study languages of infinite bar strings, i.e. infinite sequences of names that feature binding of fresh names; binding corresponds roughly to reading letters from input words in automata models with registers. We introduce regular nominal nondeterministic Büchi automata (Büchi RNNAs), an automata model for languages of infinite bar strings, repurposing the previously introduced RNNAs over finite bar strings. Our machines feature explicit binding (i.e. resource-allocating) transitions and process their input via a Büchi-type acceptance condition. They emerge from the abstract perspective on name binding given by the theory of nominal sets. As our main result we prove that, in contrast to most other nondeterministic automata models over infinite alphabets, language inclusion of Büchi RNNAs is decidable and in fact elementary. This makes Büchi RNNAs a suitable tool for applications in model checking.
CRIS-Team Scopus Importer:2021-10-01
Keywords: Data languages; Inclusion checking; Infinite words; Nominal sets

Nominal Topology for Data Languages - Birkmann, Fabian; Milius, Stefan; Urbat, Henning (Leibniz International Proceedings in Informatics, LIPIcs, 2023)
We propose a novel topological perspective on data languages recognizable by orbit-finite nominal monoids. For this purpose, we introduce pro-orbit-finite nominal topological spaces. Assuming globally bounded support sizes, they coincide with nominal Stone spaces and are shown to be dually equivalent to a subcategory of nominal boolean algebras. Recognizable data languages are characterized as topologically clopen sets of pro-orbit-finite words. In addition, we explore the expressive power of pro-orbit-finite equations by establishing a nominal version of Reiterman’s pseudovariety theorem.
CRIS-Team Scopus Importer:2023-08-18
Keywords: Data languages; Nominal sets; Profinite space; Stone duality

Nondeterministic syntactic complexity - Myers, Robert S.R.; Milius, Stefan; Urbat, Henning (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2021)
We introduce a new measure on regular languages: their nondeterministic syntactic complexity. It is the least degree of any extension of the ‘canonical boolean representation’ of the syntactic monoid. Equivalently, it is the least number of states of any subatomic nondeterministic acceptor. It turns out that essentially all previous structural work on nondeterministic state-minimality computes this measure. Our approach rests on an algebraic interpretation of nondeterministic finite automata as deterministic finite automata endowed with semilattice structure. Crucially, the latter form a self-dual category.
CRIS-Team Scopus Importer:2021-07-09

On Algebras with Effectful Iteration - Milius, Stefan; Adámek, Jiří; Urbat, Henning (Proc. Coalgebraic Methods in Computer Science (CMCS'18), 2018)

On Continuous Nondeterminism and State Minimality - Adámek, Jiří; Milius, Stefan; Myers, Robert; Urbat, Henning; Urbat, Henning (Electronic Notes in Theoretical Computer Science, 2014)
This paper is devoted to the study of nondeterministic closure automata, that is, nondeterministic finite automata (nfas) equipped with a strict closure operator on the set of states and continuous transition structure. We prove that for each regular language L there is a unique minimal nondeterministic closure automaton whose underlying nfa accepts L. Here minimality means no proper sub or quotient automata exist, just as it does in the case of minimal dfas. Moreover, in the important case where the closure operator of this machine is topological, its underlying nfa is shown to be state-minimal. The basis of these results is an equivalence between the categories of finite semilattices and finite strict closure spaces.
UnivIS-Import:2015-03-09:Pub.2014.tech.IMMD.profes_1.oncont
Keywords: Canonical Nondeterministic Automata; Closure Spaces; Semilattices; State Minimality

On Finitary Functors and Their Presentation - Adámek, Jiří; Milius, Stefan; Moss, Lawrence; Urbat, Henning; Urbat, Henning (Journal of Computer and System Sciences, 2015)
UnivIS-Import:2015-03-09:Pub.2014.tech.IMMD.profes_1.onfini

On Language Varieties Without Boolean Operations - Birkmann, Fabian; Milius, Stefan; Urbat, Henning (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2021)
Eilenberg’s variety theorem marked a milestone in the algebraic theory of regular languages by establishing a formal correspondence between properties of regular languages and properties of finite monoids recognizing them. Motivated by classes of languages accepted by quantum finite automata, we introduce basic varieties of regular languages, a weakening of Eilenberg’s original concept that does not require closure under any boolean operations, and prove a variety theorem for them. To do so, we investigate the algebraic recognition of languages by lattice bimodules, generalizing Klíma and Polák’s lattice algebras, and we utilize the duality between algebraic completely distributive lattices and posets.
CRIS-Team Scopus Importer:2021-04-30

On the behaviour of coalgebras with side effects and algebras with effectful iteration - Adamek, Jiri; Milius, Stefan; Urbat, Henning (Journal of Logic and Computation, 2021)
For every finitary monad T on sets and every endofunctor F on the category of T-algebras, we introduce the concept of an ffg-Elgot algebra for F, i.e. an algebra admitting coherent solutions for finite systems of recursive equations with effects represented by the monad T. The goal is to study the existence and construction of free ffg-Elgot algebras. To this end, we investigate the locally ffg fixed point phi(F), i.e. the colimit of all F-coalgebras with free finitely generated carrier, which is shown to be the initial ffg-Elgot algebra. This is the technical foundation for our main result: the category of ffg-Elgot algebras is monadic over the category of T-algebras.
CRIS-Team WoS Importer:2021-10-15

Positive Data Languages - Frank, Florian; Milius, Stefan; Urbat, Henning (LIPIcs : Leibniz International Proceedings in Informatics, 2023)
Positive data languages are languages over an infinite alphabet closed under possibly non-injective renamings of data values. Informally, they model properties of data words expressible by assertions about equality, but not inequality, of data values occurring in the word. We investigate the class of positive data languages recognizable by nondeterministic orbit-finite nominal automata, an abstract form of register automata introduced by Bojańczyk, Klin, and Lasota. As our main contribution we provide a number of equivalent characterizations of that class in terms of positive register automata, monadic second-order logic with positive equality tests, and finitely presentable nondeterministic automata in the categories of nominal renaming sets and of presheaves over finite sets.
Keywords: Data Languages; Register Automata; MSO; Nominal Sets; Presheaves

Profinite Monads, Profinite Equations and Reitermann's Theorem - Chen, Liang-Ting; Adámek, Jiří; Milius, Stefan; Urbat, Henning; Urbat, Henning (Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS 2016, 2016)
UnivIS-Import:2017-03-24:Pub.2016.tech.IMMD.profes_1.profin
Keywords: monads; algebra; pseudo-varieties; profinite equations

Reiterman's Theorem on Finite Algebras for a Monad - Adamek, Jiri; Chen, Liang-Ting; Milius, Stefan; Urbat, Henning (ACM Transactions on Computational Logic, 2021)
Profinite equations are an indispensable tool for the algebraic classification of formal languages. Reiterman's theorem states that they precisely specify pseudovarieties, i.e., classes of finite algebras closed under finite products, subalgebras and quotients. In this article, Reiterman's theorem is generalized to finite EilenbergMoore algebras for a monad T on a category D: we prove that a class of finite T-algebras is a pseudovariety iff it is presentable by profinite equations. As a key technical tool, we introduce the concept of a profinite monad (T) over cap associated to the monad T, which gives a categorical view of the construction of the space of profinite terms.
CRIS-Team WoS Importer:2022-02-11

Schützenberger products in a category - Chen, Liang-Ting; Urbat, Henning (20th International Conference on Developments in Language Theory, DLT 2016, 2016)

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

Syntactic Minimization of Nondeterministic Finite Automata - Myers, Robert S.R.; Urbat, Henning (Leibniz International Proceedings in Informatics, LIPIcs, 2021)
Nondeterministic automata may be viewed as succinct programs implementing deterministic automata, i.e. complete specifications. Converting a given deterministic automaton into a small nondeterministic one is known to be computationally very hard; in fact, the ensuing decision problem is PSPACE-complete. This paper stands in stark contrast to the status quo. We restrict attention to subatomic nondeterministic automata, whose individual states accept unions of syntactic congruence classes. They are general enough to cover almost all structural results concerning nondeterministic state-minimality. We prove that converting a monoid recognizing a regular language into a small subatomic acceptor corresponds to an NP-complete problem. The NP certificates are solutions of simple equations involving relations over the syntactic monoid. We also consider the subclass of atomic nondeterministic automata introduced by Brzozowski and Tamm. Given a deterministic automaton and another one for the reversed language, computing small atomic acceptors is shown to be NP-complete with analogous certificates. Our complexity results emerge from an algebraic characterization of (sub)atomic acceptors in terms of deterministic automata with semilattice structure, combined with an equivalence of categories leading to succinct representations.
CRIS-Team Scopus Importer:2021-10-01
Keywords: Algebraic language theory; Nondeterministic automata; Np-completeness

Syntactic Monoids in a Category - Adámek, Jiří; Milius, Stefan; Urbat, Henning; Urbat, Henning (Coalgebraic and Algebraic Methods in Computer Science (CALCO'15), 2015)
UnivIS-Import:2016-06-01:Pub.2015.tech.IMMD.profes_1.syntac
Keywords: Algebra; Algebraic automata theory; Coalgebra; Commutative variety; Duality; Symmetric monoidal closed category; Syntactic monoid; Transition monoid

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

Varieties of data languages - Urbat, Henning; Milius, Stefan (Leibniz International Proceedings in Informatics, LIPIcs, 2019)
We establish an Eilenberg-type correspondence for data languages, i.e. languages over an infinite alphabet. More precisely, we prove that there is a bijective correspondence between varieties of languages recognized by orbit-finite nominal monoids and pseudovarieties of such monoids. This is the first result of this kind for data languages. Our approach makes use of nominal Stone duality and a recent category theoretic generalization of Birkhoff-type theorems that we instantiate here for the category of nominal sets. In addition, we prove an axiomatic characterization of weak pseudovarieties as those classes of orbit-finite monoids that can be specified by sequences of nominal equations, which provides a nominal version of a classical theorem of Eilenberg and Schützenberger.
CRIS-Team Scopus Importer:2019-07-26
Keywords: Algebraic language theory; Data languages; Nominal sets; Stone duality

Varieties of Languages in a Category - Adámek, Jiří; Milius, Stefan; Myers, Robert; Urbat, Henning; Urbat, Henning (30th Annual Symposium on Logic in Computer Science (LICS'15), 2015)
UnivIS-Import:2016-06-01:Pub.2015.tech.IMMD.profes_1.variet
Keywords: Algebra; Automata; Coalgebra; Duality; Eilenberg's theorem; Monoids; Varieties of languages

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