Vorträge im SoSe 2018

Vorträge im SS 2018

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 2018

—

Bisherige Vorträge

Date Speaker, Topic Abstract
03-Jul Sergey Goncharov, A Semantics for Hybrid Iteration The recently introduced notions of guarded traced (monoidal) category and guarded (pre-)iterative monad aim at unifying different instances of partial iteration whilst keeping in touch with the established theory of total iteration and preserving its merits. In this paper we use these notions and the corresponding stock of results to examine different types of iteration for hybrid computations.
As a starting point we use an available notion of hybrid monad restricted to the category of sets, and modify it in order to obtain a suitable notion of guarded iteration with guardedness interpreted as progressiveness in time – we motivate this modification by our intention to capture Zeno behaviour in an arguably general and feasible way. We illustrate our results with a simple programming language for hybrid computations and interpret it w.r.t. the developed semantic foundations.
03-Jul Ulrich Dorsch, Graded Monads and the Linear Time – Branching Time Spectrum I will present how graded monads can be used in a uniform and purely coalgebraic approach to capture various notions of process equivalences in the linear time – branching time spectrum: completed traces, possible futures, simulation semantics, etc. This is work in progress based on [1] and [2].
[1] Milius, Pattinson, Schröder. Generic Trace Semantics and Graded Monads. 2015
[2] van Glabeek. The Linear Time – Branching Time Spectrum I. 2001
26-Jun Michael Sammler, Formalization of “One Modal Logic to Rule Them All?” In this talk I will discuss the results of my master project, where I formalized the paper “One Modal Logic to Rule Them All?” by Tadeusz Litak and Wesley H. Holliday in Coq. I will show how my formalization helped to improve the paper and give example for some corrections, which were found due to the formalization. The second part of this talk will be on the lessons learned during this project, which resulted in around 4500 lines of Coq code, with a focus on how binding was handled using De-Brujin indices and the Autosubst library.
26-Jun Christian Bay, Ontological Inference of Treatment Plans from Psychiatric Clinical Guidelines In this talk I will present the results of my master thesis.

It is about extending the Clinical Support System, CGM/F20, to generate individual treatment plans for patients. In contrast to existing work in this field, the treatment plan can adapt dynamically depending on the given circumstances. The generation is based on an ontological knowledge base, which consists of a guideline for schizophrenia as well as medical records for patients. Instead of inferring only recommendations for an immediate application, the existing knowledge is used to generate a treatment plan that is as specific as possible. In particular, the ontology has been extended regarding the temporal relationship between events and their recommendation strength. Besides transitioning a large part of the guideline into an ontology, other tools like SPARQL queries and SWRL rules have been used. Besides explaining the basic ideas of my approach, I will present a little case study as well.
25-Jun Ohad Kammar, // A monad for full ground reference cells // I will describe how to build a monad on a functor category to model dynamic allocation of potentially cyclic memory cells. In particular I’ll explain how to tackle the challenge of ‘effect masking’ which means roughly that ‘if you don’t need to know about memory access then you can’t detect it.’, and use this monad to give a denotational account of an ML-like language with reference cells, and validate associated program transformations.

I will explain the main insight behind our construction: identifying the collection of stores as an object in a different functor category equipped with a monad for adding hiding/encapsulation capabilities to the stores. I will then obtain the full ground storage monad by applying a state monad transformer to the encapsulation monad.

The talk is based on work with: Paul B. Levy, Sean K. Moss, and Sam Staton ([http://arxiv.org/abs/1702.04908]).
19-Jun Christoph Rauch, // A Metalanguage for Guarded Iteration // I will present a generic metalanguage for guarded iteration based on combining the notion of abstract guardedness we developed over the past year and a half with the fine-grain call-by-value paradigm, which we intend as a unifying programming language for guarded and unguarded iteration in the presence of computational effects. The language comes with a denotational semantics over a suitable class of strong monads supporting guarded iteration and is in touch with the standard operational behaviour of iteration, which we showed in terms of a concrete big-step operational semantics for a certain specific instance of the metalanguage adequate with respect to the denotational semantics. I will give an overview over the language features and the theoretical foundations needed to construct the denotational model.
12-Jun Henning Urbat, // Data Languages: A Categorical Perspective // Automata theory over the category of nominal sets has received much attention in recent years. In this talk, I will show how to extend the abstract categorical approach to algebraic language theory to the nominal case. The main idea is to consider orbit-finite monoids over nominal sets as language recognizers, and interpret recognition by means of a duality between the category of nominal sets and a suitable category of nominal boolean algebras. In this way, one obtains a nominal version of a (local) Eilenberg-Reiterman correspondence which relates properties of languages to properties of orbit-finite monoids.
05-Jun Fatemeh Seifan, // Completeness for coalgebraic modal mu-calculus: part 2 // In one of my earlier talks (if anybody remembers at all by now) I presented a completeness result for the coalgebraic modal mu-calculus in the case where the functor preserves weak pullbacks. We considered a nabla-based coalgebraic fixpoint logic and proved that Walukiewicz’s well-known completeness result for the standard mu-calculus can be generalized using coalgebras. In this talk I’ll show that we can drop the constrain on preservation of weak pullbacks and prove a more general completeness result (for the coalgebraic mu-calculus based on predicate liftings) that covers the case for the graded mu-calculus and the monotone modal mu-calculus.
29-May Tadeusz Litak, // One Modal Logic to Rule Them All? // This is joint work with Wesley H. Holliday (UC Berkeley). We introduce an extension of the modal language with what we call the global quantificational modality. Unlike the propositional quantifier by itself, it can be straightforwardly interpreted in any Boolean Algebra Expansion (BAE); for example, it does not require any form of lattice-completeness. We present a Hilbert-style calculus GQM, show its completeness, study its relationship with the theory of discriminator BAEs, and show that GQM formulas valid over lattice-complete BAEs cannot be recursively axiomatized. This last statement is proved by generalizing known prenex form results for the full second-order propositional modal logic and appears to be of interest in its own right. Our formalism enables a conceptual shift: what have traditionally been called different “modal logics” now become universal theories over the base logic GQM.
15-May Thorsten Wissmann, // Reachability closure in (weak) coalgebra is a coreflection // We consider coalgebras with an initial state and weak homomorphisms. In case of LTSs this means that the transitions are preserved, but not necessarily reflected by the morphisms. Beside LTSs, this setting covers different kinds of branching, like probabilistic systems, in combination with arbitrary data, e.g. (un)ordered trees instead of ordinary words. In this setting, we prove that the full subcategory of reachable coalgebras is a coreflective subcategory and we give the explicit construction on the level of functors T and F, where T describes the branching and F the data type.
08-May Paul Wild, Fuzzy and Probabilistic van Benthem theorems In my previous talk, we examined variants of modal and first order logic in a fuzzy setting. We then discussed how the notion of behavioural distance can be captured equivalently in terms of 1) a game, 2) the modal formulas, and 3) the so-called Kantorovich lifting. Using this notion of behavioural distance, we then proved a version of the van Benthem characterization theorem for these logics.
In the first part of this talk, we will tie up some loose ends that were left last semester. Then, in the second part, we will demonstrate how the results from the fuzzy setting can be applied in a probabilistic one, where the semantics of diamond is given as an expected value over successor states. Here, in order to give a game-theoretic account of behavioural distance, we will make use of the Kantorovich-Rubinstein duality theorem from transportation theory.
24-Apr Stefan Milius, On Finitary Functors and Finitely Presentable Algebras It is well-known that finitary set functors are, equivalently, the bounded ones. However, the published proof of this fact is incorrect. In this talk we present a correct proof of a more general result. We call a functor finitely bounded if every finitely gerenerated subobject of FX factorizes through a finitely generated subobject of X under F, and we prove that this is equivalent to F being finitary for all functors between “reasonable” locally finitely presentable categories, provided F preserves monomorphisms. We then present a condition on the category under which that last assumption can be dropped.
Furthermore, for finitary regular monads T on locally finitely presentable categories we characterize the finitely generated (and finitely presentable) objects in the category of T-algebras in the style known in general algebra: they are the algebras presentable by finitely many generators (and finitely many relations).