Oberseminar (WiSe 2024/25)

The commercial registry is an important institution for validating information on trading partners in Germany. The obligation to inform the registry on changes to the company results in mostly legally simple and similar applications. Automated application checking could help to reduce the workload on notaries and registry court officials by eliminating oversights. My master project looked into testing logical tools on their applicability in this field. In this talk, I present the challenges faced when formalizing the registration applications using eFLINT, an action based normative specification language for compliance checking, and sCASP, an implementation of answer set programming.

Process algebras are mathematical frameworks for modeling the behaviour of concurrent systems. Bisimilarity serves as an equivalence relation for comparing their behaviour. GSOS is a rule format for defining the operational semantics for such process algebras, but is limited in its ability to encode process algebras with recursion. The key semantic property of bisimilarity being a congruence is also hard to establish in the presence of recursion – the denotational methods employed for that are notoriously involved and fragile. Higher-Order GSOS (HO-GSOS) is a recently proposed framework helping to resolve these limitations. This master’s thesis proposes a treatment of process algebras with recursion via (properly) higher-order abstract GSOS, using Milner’s Calculus of Communicating Systems as a concrete example. This is done by specifying alternative operational semantics rules, showing their equivalence to the standard semantics in the guarded case, and giving the corresponding categorical interpretation to fit into HO-GSOS.

Small-step and big-step are two well-known flavors of operational semantics. The former describes fine-grained steps of reduction, while the latter describes every finite chain of primitive reductions (if it exists) in one atomic step. One can see these two as relations and say that they are equivalent when the big-step semantics is just the transitive closure of the small-step semantics.
Usually, small-step semantics is designed first, and then an equivalent big-step semantics is derived from it. A comprehensive, rigorous method that describes this derivation does not exist in the literature, and it is usually done on a case-by-case basis every time that a language is designed or modified. Abstract HO-GSOS is a categorical framework to reason on small-step higher-order operational semantics. It describes a certain higher-order rule format categorically, allowing further abstract inspections. We have set this framework as our playground and worked through crafting the mentioned comprehensive method to derive a big-step specification. We have introduced some constraints on HO-GSOS, namely “Strongly Separated HO-GSOS,” and described a transformation to equivalent specifications in our new rule format, “Big-step SOS.” The equivalence of the resulting big-step derivation is proved rigorously, and some primitive and frequently needed features of programming languages have been instantiated within the method.

Graded semantics provide a generalized framework for the semantics (and accompanying logics) of coalgebras. In some cases, the framework even supports a notion of infinite behaviour. It’s tempting to assume that this notion would extend finite graded semantics in the same way the established finite semantics that is captured would be. But for example in the case of infinite graded trace semantics there is no such correspondence to infinite trace semantics. In this talk I will make this distinction clear and conclude with a definition of fixpoint logics for infinite graded semantics.

In concurrency theory, a range of different notions of equivalence can be characterized via Spoiler-Duplicator games; for example, most equivalences on the linear-time / branching-time spectrum come with such characterizations. In this talk, we build on work by Ford et al. that extends Spoiler-Duplicator type games to the coalgebraic setting via the framework of graded semantics. We generalize this approach to cover other types of process comparison beyond equivalence, such as behavioural preorders or pseudometrics. At first, we abstract notions of behavoiural conformance in terms of topological categories. We obtain a sound and complete generic game for behavioural conformances in this sense, for which we furthermore derive a syntactic perspective by instantiating to topological categories that can be presented in terms of relational structures.

In this work-in-progress talk, we will take a Curry-Howard correspondence inspired perspective on formal argumentation theory. To this end, a dialectical variant of the (terribly named) calculus (sometimes “Matilda”) is presented and used to study central argumentation-theoretic concepts such as argument, attack (rebuttal and undercut), support, defaults and burden of proof. We will discuss some examples using an extension of the Fellowship prover for the λμμ̃-Calculus and explore possible directions for future work (rewriting, categorical semantics).

Higher-order coalgebras are a convenient abstract setting for modelling higher-order languages and their operational semantics. In this talk, I introduce a fibrational approach to reasoning about congruence properties of higher-order coalgebras. It uniformly applies to various notions of applicative bisimilarity and applicative distances known in the literature, as well as to new settings such as higher-order languages combining nondeterministic and probabilistic effects.

Regular languages – the languages accepted by deterministic finite automata – are known to be precisely the languages recognized by finite monoids. This characterization is the origin of algebraic language theory. In the present paper, we generalize this result to automata with computational effects given by a monad, thereby providing the foundations of an effectful algebraic language theory. Our prime application is a novel algebraic approach to languages computed by T-FA, which are finite automata with effects given by a monad T. We show that these languages coincide with

1. languages recognized by finite monoids via effectful monoid morphisms, and
2. languages recognized by T-bimonoids, and moreover T-monoids if the monad T is commutative.

In this framework, we derive novel characterizations are for languages computed probabilistic finite automata, nondeterministic probabilistic finite automata, and weighted finite automata over arbitrary semirings.

This 45-minutes-talk will cover some probability monads, and generalizations. In the first section, we will encounter some classical probability monads. This will lead us to weakened products and the framework of Markov categories. As a short demonstration of this formalism, we will consider (a categorical version of) de Finetti’s theorem.
The second part then addresses generalizations: imprecise probabilities, such as Dempster-Shafer-belief functions, model situations with insufficient knowledge. Do they fit into the framework of Markov categories? Do they even have probability monads? This is still an open question. Non-commutative probability is another way of generalization; I will shortly show how this is formulated in terms of C*-algebras, and point to recent results on involutive / quantum Markov categories.