Vorträge im SS 2019

Das Oberseminar des Lehrstuhls für Theoretische Informatik findet dienstags 14:15-15:45 in Raum Raum 00.131, Cauerstraße 11 statt. Es steht Masterstudierenden und Doktoranden sowie bei Interesse Bachelorstudierenden offen. Die Themenwahl erfolgt nach Vereinbarung entsprechend den Schwerpunkten des Lehrstuhls. Nachfragen gerne per Mail an den Leiter des Lehrstuhls (mailto:lutz.schroeder@informatik.uni-erlangen.de).

Voraussichtlicher Plan für SS 2019

—

Bisherige Vorträge

Date Speaker, Topic Abstract
16-July Aaron Strahlberger, Implementation of a Coalgebraic Model Checker [pdf-embedder url=”/wp-content/uploads/media/ss19/ober/strahlberger-slides.pdf” ] For my bachelor thesis I am implementing a model checker based on the insights described in the recent paper “Game Based Local Model Checking for the coalgebraic µ-Calculus” by Daniel Hausmann and Lutz Schröder. In this talk I describe the theoretical background and my implementation.
16-July Jonas Foster, Non-Iterative Modal Logics are Coalgebraic [pdf-embedder url=”/wp-content/uploads/media/ss19/ober/forster-slides.pdf” ] Coalgebraic modal logic is a semantic framework that naturally lends its self to the study of modal logics axiomatised in rank 1. We generalise one of the results concerning rank-1 logics, a canonical model construction, to non-iterative logics, i.e. modal logics axiomatised in such a way that all propositional variables in axioms are nested at most one modality deep. We restrict the class of coalgebras on a functor by introducing the notions of weak copoints and proper coalgebras on weakly pointed functors, construct a canonical structure, show soundness and attempt to show completeness.
9-July Paul Wild, Towards Pseudometric Graded Semantics [pdf-embedder url=”/wp-content/uploads/media/ss19/ober/wild-slides.pdf” ] We make some first steps towards transferring the graded monad approach to trace semantics to a quantitative setting. To this end, we employ a graded version of the quantitative algebraic theories recently put forward by Mardare et al. to obtain graded monads which are then lifted to the category of pseudometric spaces and nonexpansive maps.
02-July Christoph Rauch, A Trace (of) Sandwich [pdf-embedder url=”/wp-content/uploads/media/ss19/ober/rauch-slides.pdf” ] In my last talk, I presented a metalanguage for guarded iteration, which is supposed to capture the widespread phenomenon of having to guard certain operations in order to guarantee sensible behaviour (e.g. termination or progress) of iteration constructs. I also pointed out the connection to trace-based operational semantics for programming languages. This talk will provide a slightly different perspective: I will give a little recap of monads (specifically monads for iteration) and adjunctions, with recipes for combining them in order to trace programs, and I will present sandwich theorems which allow us to use these monads in the guarded metalanguage.
18-June Miriam Polzer, Local Store: All Hail the Magic Garbage Collector [pdf-embedder url=”/wp-content/uploads/media/ss19/ober/polzer-slides.pdf” ] I will present a simple programming language for local storage (of values and pointers) and some program equalities and behaviours of interest. While there are various denotational semantics for these, there are no Hoare or Separation Logics and weakest precondition operators (at least to my knowledge). I will present three different ideas.
28-May Michael Sammler, Verified sandboxing of untrusted code in low-level languages [pdf-embedder url=”/wp-content/uploads/media/ss19/ober/MSMSc_presentation.pdf” ] Sandboxing is a common technique for isolating untrusted components in applications, but the high-level guarantees of such a compartmentalization have not been formally explored. In this talk I will present an idealization and formalization of low-level sandboxing of an untrusted and untyped component in a typed application and show that the sandbox is secure when interacting with the untrusted component using the any type that is inhabited by all values. Furthermore I will present a mechanism to automatically insert checks and transformations at the boundary that – although not necessary for security – greatly simplify the integration of the untrusted code into the typed application by converting between the any type and richer types. I will also give an overview of the higher-order concurrent separation logic framework Iris as it is the basis of the formalization.
21-May Ulrich Dorsch, Graded Monads and Graded Logics [pdf-embedder url=”/wp-content/uploads/media/ss19/ober/udorsch_talk19.pdf” ] I will present how graded monads can be used in a uniform and purely coalgebraic approach to capture various notions of (trace) equivalences in the linear time – branching time spectrum as well as trace equivalence for generative probabilistic systems. In particular I will present graded monads that can be defined via graded theories. I will further present how graded logics invariant under the given semantics can be extracted via graded algebras together with a generic expressiveness criterion for these logics.
14-May Thorsten Wißmann, Internalizing Multisortedness [pdf-embedder url=”/wp-content/uploads/media/ss19/ober/wissmann-internal-multisort-slides.pdf” ] When instantiating coalgebraic frameworks (like in coalgebraic logics or in coalgebraic minimization procedures) multisorted systems arise. E.g. in Segala systems, one sort of states has non-deterministic behaviour, and the other sort has probabilistic behaviour. If the underlying category is Set, or in general an extensive category, we will translate coalgebras for such a multisorted functor into coalgebras for a canonically singlesorted functor on the base category. This translation preserves behavioural equivalence. This translation is implemented the coalgebraic partition refiner CoPaR and makes CoPaR applicable to composite and multisorted Set-functors.
14-May Thorsten Wißmann, Fibrational View on Breadth-First Search [pdf-embedder url=”/wp-content/uploads/media/ss19/ober/wissmann-fib-graph-slides.pdf” ] This work in progress tries to put different constructions on graphs in a common coalgebraic framework. The motivation is the common statement that “shortest path algorithms like Dijkstra or Bellman Ford are basically breadth-first search with weights”. After a short introduction on fibrations, we will define the ‘initial lifting’ of a coalgebra (with a root vertex) and will see how to construct it. The initial lifting of a coalgebra instantiates to the following: (1) Rechability: The initial lifting tells which states are reachable from the root node, and the related construction resembles breadth-first search. (2) Shortest paths: The initial liftings provides a distance function that equips each vertex with a distance from the root (in a possibly infinite coalgebra). If the coalgebra is finite, this is the length of the shortest path, and the construction resembles the algorithms by Djikstra and Bellman&Ford.
07-May Hans-Peter Deifel, Overview of Automata Learning [pdf-embedder url=”/wp-content/uploads/media/ss19/ober/hpdeifel-slides.pdf” ] I will give an introduction to the field of automata/model learning. Starting from Angluin’s original L* algorithm, I will present extensions of the algorithm to different types of automata and discuss available optimizations and their applicability in practice. Finally, I will hint at two different category theoretical abstractions of the algorithm that have been proposed by Jacobs and Silva, as well as Barlocco, Kupke, and Rot.
30-Apr Merlin Göttinger, More Power to Coalition Logic [pdf-embedder url=”/wp-content/uploads/media/ss19/ober/goettlinger-slides.pdf” ] We will have a look at coalition logic and the coalgebraic view on it. Further we will present possible extensions of coalition logic better suited to represent statements made by humans in day to day reasoning about coalition power. We will see how these extensions in syntax affect the coalgebraic representation and give one-step rule axiomatizations to show that SAT is still in PSPACE.