Oberseminar SoSe 2026

Das Oberseminar des Lehrstuhls für Theoretische Informatik findet dienstags 14:15-15:45 in Raum 00.131-128 (Cauerstraße 11) statt.

Das Oberseminar steht Masterstudierenden und Doktoranden sowie bei Interesse Bachelorstudierenden offen.
Die Themenwahl erfolgt nach Vereinbarung entsprechend den Schwerpunkten des Lehrstuhls. Die Vortragstermine werden am ersten Termin in der Vorlesungszeit festgelegt.

Bei Nachfragen gerne per Mail an den Seminarleiter (Prof. Dr. Stefan Milius), Anmeldung zur Mailingliste: TCS-Seminar Mailinglist

Vorträge

Current Talks

Tuesday, 30.06.2026

Quantalic(?!) Relational Connectors
Florian Guthmann
Abstract
Relational Connectors generalize lax extensions of set functors and enable reasoning about notions of (bi)simulation in a heterogeneous setting. In this talk, we show how to extend this framework from the two-valued domain to a many-valued one. This allows incorporating finer-grained means of comparison than two-valued behavioural equivalences. In search of a suitable value domain, we will explore complete semirings and show where they do and do not suffice. As a conclusion to this search, we show first results for relational connectors that take values in a quantale.

Upcoming Talks

Tuesday, 07.07.2026

TBA
N.N.
Abstract
TBA

Tuesday, 14.07.2026

TBA
Maximilian Rumi
Abstract
TBA

Tuesday, 14.07.2026

TBA
Henning Urbat
Abstract
TBA

Previous Talks

Tuesday, 21.04.2026

Finch: A Browser-Based Proof Assistant for Fitch-Style Natural Deduction
Leon Vatthauer
SlidesAbstract
Finch is a browser-based proof assistant designed to help students construct correct Fitch-style natural deduction proofs by providing helpful error messages and an intuitive interface.
The application was developed for my Master's project and is written purely in Haskell using the Miso library together with GHC's WebAssembly backend. In this talk I will showcase Finch, explain how the proof checker operates, and provide a brief introduction to web development in Haskell.

Tuesday, 28.04.2026

The Substitution Tensor in Presheaves and Nominal Sets
Fabian Lenke
Abstract
Presheaves and nominal sets provide alternative abstract models of sets of syntactic objects with free and bound variables, such as λ-terms. One distinguishing feature of the presheaf-based perspective is its elegant syntax-free characterization of substitution using a closed monoidal structure. In this talk, we introduce a corresponding closed monoidal structure on nominal sets, in the spirit of Fiore et al.'s substitution tensor for presheaves over finite sets. To this end, we present a general method to derive a closed monoidal structure on a category from a given action on that category. We demonstrate that this method not only uniformly recovers known substitution tensors for various kinds of presheaf categories but also yields novel notions of substitution tensor for nominal sets and their relatives, such as renaming sets. In doing so, we shed new light on different incarnations of nominal sets and (pre-)sheaf categories and establish a number of novel correspondences between them.

Tuesday, 05.05.2026

"My Name Is" - The Real S...ingle-Use Maps in Nominal (Renaming) Sets
Simon Prucker
SlidesAbstract
In computer architecture, the volatility of register contents can be both an undesirable property - for example, in memory architectures with destructive readout - and a desirable one, as in cryptographic applications involving one-time keys. In the spirit of ensuring that register contents are not used twice, single-use functions and single-use register automata have been studied in the context of nominal sets, though so far only at a syntactic level.
In this talk, after introducing a notion of multiplicity for names in nominal (renaming) sets, we examine an axiomatic description of single-use maps and establish an insightful characterisation of them. We then give an overview of several promising conjectures concerning the categorical properties of these maps, their relationship to the syntactic notion of single-use functions, and whether they can help define a nominal automata model that is expressively equivalent to nominal monoids and single-use register automata.

Tuesday, 12.05.2026

Combinatorial descriptions of (defect) TQFTs
Prof. Dr. Cathérine Meusburger (Department Mathematik, Lie-Gruppen und Darstellungstheorie)
Abstract
A topological quantum field theory (TQFT) is a symmetric monoidal functor Z: Cob_{n,n-1} -> Vect from a cobordism category Cob_{n,n-1} into the category Vect of vector spaces over some field. It assigns to every closed (n-1)-manifold a vector space and to every compact n-manifold with boundary a linear map between the vector spaces associated to its boundary components, in such a way that this is compatible with gluings of manifolds and with their disjoint union. For n=3, these TQFTs have applications in topological quantum computing, where they describe quantum double and Levin-Wen models. A currently very active topic of research are TQFTs with defects, which arise from stratified cobordism categories and describe defects in quantum double and Levin-Wen models. In the talk I explain how simple examples of TQFTs can be formulated in a more combinatorial way in terms of simplicial complexes and the associated posets and simplicial sets. I then explain how this can be extended to stratified cobordism categories and defect TQFTs.
References: Faria Martins, J. and Meusburger, C., 2026. A geometrical description of untwisted 3d Dijkgraaf-Witten TQFT with defects. Advances in Mathematics, 494 and ongoing work

Tuesday, 19.05.2026

Interpolation in Modal and Fuzzy Modal Logic: A Sequent Calculus-Based Approach
Stefan Gebhart
SlidesAbstract
In this talk, we study Craig and uniform interpolation for modal logics from a proof-theoretic perspective. We first revisit the classical modal logic (\mathbf{K}), presenting one-sided sequent calculi that not only establish interpolation results but also give explicit constructions of interpolants. In particular, we describe how Craig interpolants can be extracted from labelled proofs, and how a modified calculus can be used to compute uniform post-interpolants by eliminating a chosen propositional variable. We then extend this approach to non-expansive fuzzy modal logic. After introducing the corresponding syntax and one-sided sequent calculus, we explain how analogous proof transformations yield Craig and uniform interpolation in the many-valued setting. The focus throughout is on the constructive content of the calculi: proofs are not merely certificates of validity, but provide algorithms for building the required interpolants.

Tuesday, 19.05.2026

A Characterization of the Steady State
Üsame Cengiz
Abstract
Stationary distributions are a fundamental concept in Markov chain analysis; they represent the mean recurrence of states in the long run, depending on the initial state distribution. For finite discrete-time Markov chains, which are represented by a stochastic matrix, these steady states can be generated by a steady state matrix that immediately returns the corresponding steady state when multiplied with an initial state distribution. We start from a little-known characterization of the steady state matrix and use this characterization to prove that any Markov chain can be convexly combined with the identity matrix to yield a non-periodic Markov chain with the identical steady state. We derive a further characterization that is phrased in terms of equations based purely on matrix multiplication (not mentioning rank) and as such can be used for arbitrary monad coalgebras. We illustrate briefly how this last characterization instantiates to further system types beyond probabilistic systems.

Tuesday, 02.06.2026

Terminal Coalgebras in Preasheaf Categories
Jiří Adámek (TU Braunschweig)
Abstract
Every finitary set functor has a terminal coalgebra obtained in countably many steps. This classical result due to Worrell has recently been generalized to endofunctors of DCC categories. These are the locally finitely presentable categories satisfying the Descending Chain Condition for chains of subobjects or strong quotients of every finitely presentable object. Numerous categories are DCC, e.g. sets, posets, vector spaces, and boolean algebras. The category of abelian groups, in contrast, is not DCC.
We characterize DCC categories from among the categories Set^{C^op} of presheaves on small categories C:If C is a group or a groupoid, then presheaves are DCC precisely when C is Noetherian: every ascending(!) chain of subgroups is finite. Important example: the category C of finite sets and bijections.
If C has finite products, then presheaves are DCC precisely when every object of C carries only finitely many sieves. Important example: finite sets and functions.
Presheaves on a poset are DCC precisely when the down-set of every element is finite. (Example: many-sorted sets are DCC.)

Tuesday, 09.06.2026

Extending a Reasoner for Non-Expansive Fuzzy ALC with the generally Operator
Felix Lützow
SlidesAbstract
We give an implementation of an extension to an on-the-fly tableau-based reasoner for satisfiability checking in non-expansive fuzzy ALC, programmed in OCaml. The existing system is extended with configurable support for different logic variants and with the operator generally, whose constraints are reduced to finite successor profiles and checked by linear programming. After discussing the implementation and its optimizations, we present benchmark series that show improvements for many instances and highlight large search-space cases as the main bottleneck.

Tuesday, 09.06.2026

Worrels Fixpunkt Konstruktion für lokal endlich generierte Kategorien
Jakob Roßkopf
Abstract
Adámek, Milius und Moss haben Worrels Fixpunkt Konstruktion für lokal endlich präsentierbare Kategorien verallgemeinert. Dabei wird ein finitärer Funktor iterativ auf ein terminales Objekt angewendet. In diesem Vortrag wird diese Konstruktion auf lokal endlich generierte Kategorien weiter verallgemeintert. Dazu werden statt Monomorphismen und starken Epimorphismen beliebige Faktorisierungssysteme betrachtet. Damit diese Konstruktion funktioniert, muss der Funktor verträglich mit diesen Faktorisierungssystemen sein. Ein wichtiges Beispiel dieser Verallgemeinerung sind metrische Räume.

Tuesday, 16.06.2026

Graded Algebraic Reasoning over Relational Structures
Jonas Forster
Abstract
We introduce a framework of graded universal algebra over categories of single-sorted relational structures axiomatised by infinitary Horn theories, such as partial orders or metric spaces.
Our concept of graded algebra supports grades drawn from a preordered monoid and operations (1) given by ordinary functions (i.e. they are not required to be morphisms in the underlying base category) and (2) involve unrestricted objects as arities. We extract a syntax of graded algebraic theories from the relational signature at hand, and we provide a sound and complete deduction system for graded algebraic reasoning over such theories. Moreover, we show that every graded algebraic theory can be associated with a free-algebra graded monad. We illustrate the breadth of our framework by providing axiomatic treatments of existing graded monads from numerical analysis and quantum information theory: the neighborhood monad on pseudometric spaces and the quantum monad on relational structures, respectively.

Tuesday, 23.06.2026

Choose your (Equivariant?) Strategy: NAPAs and Nominal Parity Games
Ole Elliger
SlidesAbstract
We develop nominal alternating parity automata (NAPAs) that accept infinite bar strings, i.e., infinite words over an infinite alphabet with explicit binders. These automata come with a parity game semantics: An infinite bar string is accepted if there is a winning strategy in the parity game induced by the automaton. While parity games enjoy memoryless determinacy, it is unclear whether this property carries over to a nominal variant of parity games. In this talk, we present examples illustrating why the current lack of equivariant strategies may pose a challenge for the development of NAPAs. Additionally, we partially examine the proof of memoryless determinacy for classical parity games to identify where a nominal analogue of this result might fail.

Current Talks
Tuesday, 30.06.2026	Quantalic(?!) Relational Connectors Florian Guthmann Abstract Relational Connectors generalize lax extensions of set functors and enable reasoning about notions of (bi)simulation in a heterogeneous setting. In this talk, we show how to extend this framework from the two-valued domain to a many-valued one. This allows incorporating finer-grained means of comparison than two-valued behavioural equivalences. In search of a suitable value domain, we will explore complete semirings and show where they do and do not suffice. As a conclusion to this search, we show first results for relational connectors that take values in a quantale.
Upcoming Talks
Tuesday, 07.07.2026	TBA N.N. Abstract TBA
Tuesday, 14.07.2026	TBA Maximilian Rumi Abstract TBA
Tuesday, 14.07.2026	TBA Henning Urbat Abstract TBA
Previous Talks
Tuesday, 21.04.2026	Finch: A Browser-Based Proof Assistant for Fitch-Style Natural Deduction Leon Vatthauer Slides Abstract Finch is a browser-based proof assistant designed to help students construct correct Fitch-style natural deduction proofs by providing helpful error messages and an intuitive interface. The application was developed for my Master's project and is written purely in Haskell using the Miso library together with GHC's WebAssembly backend. In this talk I will showcase Finch, explain how the proof checker operates, and provide a brief introduction to web development in Haskell.
Tuesday, 28.04.2026	The Substitution Tensor in Presheaves and Nominal Sets Fabian Lenke Abstract Presheaves and nominal sets provide alternative abstract models of sets of syntactic objects with free and bound variables, such as λ-terms. One distinguishing feature of the presheaf-based perspective is its elegant syntax-free characterization of substitution using a closed monoidal structure. In this talk, we introduce a corresponding closed monoidal structure on nominal sets, in the spirit of Fiore et al.'s substitution tensor for presheaves over finite sets. To this end, we present a general method to derive a closed monoidal structure on a category from a given action on that category. We demonstrate that this method not only uniformly recovers known substitution tensors for various kinds of presheaf categories but also yields novel notions of substitution tensor for nominal sets and their relatives, such as renaming sets. In doing so, we shed new light on different incarnations of nominal sets and (pre-)sheaf categories and establish a number of novel correspondences between them.
Tuesday, 05.05.2026	"My Name Is" - The Real S...ingle-Use Maps in Nominal (Renaming) Sets Simon Prucker Slides Abstract In computer architecture, the volatility of register contents can be both an undesirable property - for example, in memory architectures with destructive readout - and a desirable one, as in cryptographic applications involving one-time keys. In the spirit of ensuring that register contents are not used twice, single-use functions and single-use register automata have been studied in the context of nominal sets, though so far only at a syntactic level. In this talk, after introducing a notion of multiplicity for names in nominal (renaming) sets, we examine an axiomatic description of single-use maps and establish an insightful characterisation of them. We then give an overview of several promising conjectures concerning the categorical properties of these maps, their relationship to the syntactic notion of single-use functions, and whether they can help define a nominal automata model that is expressively equivalent to nominal monoids and single-use register automata.
Tuesday, 12.05.2026	Combinatorial descriptions of (defect) TQFTs Prof. Dr. Cathérine Meusburger (Department Mathematik, Lie-Gruppen und Darstellungstheorie) Abstract A topological quantum field theory (TQFT) is a symmetric monoidal functor Z: Cob_{n,n-1} -> Vect from a cobordism category Cob_{n,n-1} into the category Vect of vector spaces over some field. It assigns to every closed (n-1)-manifold a vector space and to every compact n-manifold with boundary a linear map between the vector spaces associated to its boundary components, in such a way that this is compatible with gluings of manifolds and with their disjoint union. For n=3, these TQFTs have applications in topological quantum computing, where they describe quantum double and Levin-Wen models. A currently very active topic of research are TQFTs with defects, which arise from stratified cobordism categories and describe defects in quantum double and Levin-Wen models. In the talk I explain how simple examples of TQFTs can be formulated in a more combinatorial way in terms of simplicial complexes and the associated posets and simplicial sets. I then explain how this can be extended to stratified cobordism categories and defect TQFTs. References: Faria Martins, J. and Meusburger, C., 2026. A geometrical description of untwisted 3d Dijkgraaf-Witten TQFT with defects. Advances in Mathematics, 494 and ongoing work
Tuesday, 19.05.2026	Interpolation in Modal and Fuzzy Modal Logic: A Sequent Calculus-Based Approach Stefan Gebhart Slides Abstract In this talk, we study Craig and uniform interpolation for modal logics from a proof-theoretic perspective. We first revisit the classical modal logic (\mathbf{K}), presenting one-sided sequent calculi that not only establish interpolation results but also give explicit constructions of interpolants. In particular, we describe how Craig interpolants can be extracted from labelled proofs, and how a modified calculus can be used to compute uniform post-interpolants by eliminating a chosen propositional variable. We then extend this approach to non-expansive fuzzy modal logic. After introducing the corresponding syntax and one-sided sequent calculus, we explain how analogous proof transformations yield Craig and uniform interpolation in the many-valued setting. The focus throughout is on the constructive content of the calculi: proofs are not merely certificates of validity, but provide algorithms for building the required interpolants.
Tuesday, 19.05.2026	A Characterization of the Steady State Üsame Cengiz Abstract Stationary distributions are a fundamental concept in Markov chain analysis; they represent the mean recurrence of states in the long run, depending on the initial state distribution. For finite discrete-time Markov chains, which are represented by a stochastic matrix, these steady states can be generated by a steady state matrix that immediately returns the corresponding steady state when multiplied with an initial state distribution. We start from a little-known characterization of the steady state matrix and use this characterization to prove that any Markov chain can be convexly combined with the identity matrix to yield a non-periodic Markov chain with the identical steady state. We derive a further characterization that is phrased in terms of equations based purely on matrix multiplication (not mentioning rank) and as such can be used for arbitrary monad coalgebras. We illustrate briefly how this last characterization instantiates to further system types beyond probabilistic systems.
Tuesday, 02.06.2026	Terminal Coalgebras in Preasheaf Categories Jiří Adámek (TU Braunschweig) Abstract Every finitary set functor has a terminal coalgebra obtained in countably many steps. This classical result due to Worrell has recently been generalized to endofunctors of DCC categories. These are the locally finitely presentable categories satisfying the Descending Chain Condition for chains of subobjects or strong quotients of every finitely presentable object. Numerous categories are DCC, e.g. sets, posets, vector spaces, and boolean algebras. The category of abelian groups, in contrast, is not DCC. We characterize DCC categories from among the categories Set^{C^op} of presheaves on small categories C: If C is a group or a groupoid, then presheaves are DCC precisely when C is Noetherian: every ascending(!) chain of subgroups is finite. Important example: the category C of finite sets and bijections. If C has finite products, then presheaves are DCC precisely when every object of C carries only finitely many sieves. Important example: finite sets and functions. Presheaves on a poset are DCC precisely when the down-set of every element is finite. (Example: many-sorted sets are DCC.)
Tuesday, 09.06.2026	Extending a Reasoner for Non-Expansive Fuzzy ALC with the generally Operator Felix Lützow Slides Abstract We give an implementation of an extension to an on-the-fly tableau-based reasoner for satisfiability checking in non-expansive fuzzy ALC, programmed in OCaml. The existing system is extended with configurable support for different logic variants and with the operator generally, whose constraints are reduced to finite successor profiles and checked by linear programming. After discussing the implementation and its optimizations, we present benchmark series that show improvements for many instances and highlight large search-space cases as the main bottleneck.
Tuesday, 09.06.2026	Worrels Fixpunkt Konstruktion für lokal endlich generierte Kategorien Jakob Roßkopf Abstract Adámek, Milius und Moss haben Worrels Fixpunkt Konstruktion für lokal endlich präsentierbare Kategorien verallgemeinert. Dabei wird ein finitärer Funktor iterativ auf ein terminales Objekt angewendet. In diesem Vortrag wird diese Konstruktion auf lokal endlich generierte Kategorien weiter verallgemeintert. Dazu werden statt Monomorphismen und starken Epimorphismen beliebige Faktorisierungssysteme betrachtet. Damit diese Konstruktion funktioniert, muss der Funktor verträglich mit diesen Faktorisierungssystemen sein. Ein wichtiges Beispiel dieser Verallgemeinerung sind metrische Räume.
Tuesday, 16.06.2026	Graded Algebraic Reasoning over Relational Structures Jonas Forster Abstract We introduce a framework of graded universal algebra over categories of single-sorted relational structures axiomatised by infinitary Horn theories, such as partial orders or metric spaces. Our concept of graded algebra supports grades drawn from a preordered monoid and operations (1) given by ordinary functions (i.e. they are not required to be morphisms in the underlying base category) and (2) involve unrestricted objects as arities. We extract a syntax of graded algebraic theories from the relational signature at hand, and we provide a sound and complete deduction system for graded algebraic reasoning over such theories. Moreover, we show that every graded algebraic theory can be associated with a free-algebra graded monad. We illustrate the breadth of our framework by providing axiomatic treatments of existing graded monads from numerical analysis and quantum information theory: the neighborhood monad on pseudometric spaces and the quantum monad on relational structures, respectively.
Tuesday, 23.06.2026	Choose your (Equivariant?) Strategy: NAPAs and Nominal Parity Games Ole Elliger Slides Abstract We develop nominal alternating parity automata (NAPAs) that accept infinite bar strings, i.e., infinite words over an infinite alphabet with explicit binders. These automata come with a parity game semantics: An infinite bar string is accepted if there is a winning strategy in the parity game induced by the automaton. While parity games enjoy memoryless determinacy, it is unclear whether this property carries over to a nominal variant of parity games. In this talk, we present examples illustrating why the current lack of equivariant strategies may pose a challenge for the development of NAPAs. Additionally, we partially examine the proof of memoryless determinacy for classical parity games to identify where a nominal analogue of this result might fail.

Vorträge

Kalender