# 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

Date | Speaker | Room | Topic, Abstract |
---|---|---|---|

02-Jul | Christoph Rauch | 00.131-128 | |

09-Jul | Paul Wild | 00.131-128 | |

16-Jul | Aaron Strahlberger | 00.131-128 | |

16-Jul | Jonas Foster | 00.131-128 | |

23-Jul | Frederik Völkel | 00.131-128 |

## Bisherige Vorträge

Date | Speaker, Topic | Abstract |
---|---|---|

28-May | Michael Sammler, Verified sandboxing of untrusted code in low-level languages slides | 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 [slides] | 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 [slides] | 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 [slides] | 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 [slides] | 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 [slides] | 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. |