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, 19.05.2026 |
Interpolation in Modal and Fuzzy Modal Logic: A Sequent Calculus-Based Approach
AbstractIn 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
AbstractStationary 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. |
| Upcoming Talks | |
| Tuesday, 26.05.2026 |
Sitzung fällt wegen Bergdienstag aus
|
| Tuesday, 02.06.2026 |
TBA
AbstractTBA |
| Tuesday, 09.06.2026 |
TBA
AbstractTBA |
| Tuesday, 09.06.2026 |
TBA
AbstractTBA |
| Tuesday, 16.06.2026 |
TBA
AbstractTBA |
| Tuesday, 23.06.2026 |
TBA
AbstractTBA |
| Tuesday, 30.06.2026 |
TBA
AbstractTBA |
| Tuesday, 07.07.2026 |
TBA
AbstractTBA |
| Tuesday, 14.07.2026 |
TBA
AbstractTBA |
| Tuesday, 14.07.2026 |
TBA
AbstractTBA |
| Previous Talks | |
| Tuesday, 21.04.2026 |
Finch: A Browser-Based Proof Assistant for Fitch-Style Natural Deduction
Slides
AbstractFinch 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
AbstractPresheaves 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
Slides
AbstractIn 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
AbstractA 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 |