Vorträge im WS 2017
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 WS 2017
—
Bisherige Vorträge
| Date | Speaker, Topic | Abstract |
| 20-Feb | Merlin Göttlinger, Formalising Algorithmic Correspondence for Modal Languages [pdf-embedder url=”/wp-content/uploads/media/ws17/ober/goettlinger-slides.pdf” ] | It is well-known that modal formulas if interpreted as conditions on frames correspond to monadic second-order formulas. However, some of those formulas have corresponding first-order formulas. There have been several algorithms developed to compute such correspondents algorithmically if they exist, trying to approximate the class of elementary formulas. We will recap hybrid polyadic modal logic, correspondence and have an in depth look into the algorithm SQEMA and issues arising when formalizing it in Coq. |
| 13-Feb | Malin Altenmüller, SpaceMonads! Indexing the Interior by its Perimeter [pdf-embedder url=”/wp-content/uploads/media/ws17/ober/altenmueller-slides.pdf” ] | The index of a dependent type assigns some kind of information to the type. One possibility is information about outer boundaries of a spatial structure. The types which depend on such an index represent structures that exactly fit their perimeter. I use a representation of finite indexed containers to define how space can be subdivided. Creating interiors for this description gives us the “SpaceMonadâ€. My bachelor’s thesis (and also this talk) is about the implementation of the definition, some computations and various examples of SpaceMonads (including matrices, electrical circuits and binary search trees) in the dependently typed programming language Agda. |
| 30-Jan | Julian Jakob, Exploring Zeno-like Iteration for Hybrid Components [pdf-embedder url=”/wp-content/uploads/media/ws17/ober/jakob-slides.pdf” ] | The continuous evolution monad introduced by Neves et al. encodes continuous behaviour as a computational effect, modeling a wide range of physical systems with both a continuous and a discrete component. The main goal of this master thesis is constructing a sound theory of iteration for this monad. As the standard example we take a ball dropped from some height and record its position; in idealized conditions the number of bounces is infinite, but the time until the ball stops moving is finite, which we call Zeno behaviour. Neves et al. only provide a definition for simple feedback, which we generalized. However, finding a parametrized iteration (or recursion) operator with an adequate guardedness condition has proved troublesome at various points. Therefore, we also explore changes to the monad to solve our difficulties. |
| 30-Jan | Ulrich Dorsch, Predicate Liftings and Functor Presentations in Coalgebraic Expression Languages [pdf-embedder url=”/wp-content/uploads/media/ws17/ober/udorsch.pdf” ] | Expression languages describing behaviours of Set-coalgebras can be embedded into coalgebraic logic. We define a generic expression language parametric in the coalgebraic type functor with semantics given by particular predicate liftings for the type functor (as used in coalgebraic logic) making the language a fragment of the coalgebraic μ-calculus. We establish a Kleene-type correspondence between expressions and finite systems. The properties we require of our predicate liftings are satisfied by the Moss-liftings defined via functor presentations by Marti and Venema in their work on lax extensions. Our approach covers many coalgebraic type functors, including the finitary distribution and monotone neighbourhood functor. |
| 23-Jan | Miriam Polzer, Internal Generic Hoare Logics in a Topos [pdf-embedder url=”/wp-content/uploads/media/ws17/ober/polzer-slides.pdf” ] | While the goal of my (ongoing) master’s thesis is to explore the connection between internal and external logical operations extracted from monads over a topos, this talk will mostly cover preliminaries: Using Lawvere’s hyperdoctrines, one can soundly interpret logic inside a category, a special case of this being the internal language of an elementary topos. Apart from this, we also want to establish a connection between the internal and the external view on a category. I will show how this can be done with a Yoneda Lemma construction in general, and with the so called “Kripke-Joyal semantics” in the case of topos logic. |
| 16-Jan | Tobias Heindl, Tree automata from the free 2-categories monad | Trees and forests, seen as string diagrams, form 2-cells in 2-categories. Thus it is only natural to ask whether there is a good notion of recognizability for sets of 2-cells in a 2-category that is compatible with the established notion of recognizable tree language. The talk gives a pictorial account of an instantiation of BojaÅ„czyk’s monadic recognizability for the free 2-categories monad on 2-polygraphs to shed light on the presenter’s proposal to use 2-functors to finite 2-categories as recognizers of 2-cell languages in a 2-category. The take home message is that BojaÅ„czyk’s recognizability is formidable to justify the proposal and leads us to an interesting perspective of the definition of (a sub-class—?!—of) tree automata. The talk will conclude with speculations on how the proposed notion of recognizable 2-cell language relates to the open problem of decidability of first-order recognizability of tree languages. |
| 09-Jan | Peter Trommler, //Cmm Semantics in Coq // [pdf-embedder url=”/wp-content/uploads/media/ws17/ober/trommler-talk.pdf” ] | Cmm is the intermediate language in the Glasgow Haskell Compiler (GHC) that is the basis for GHC’s backends. I will present Greg Morrisett’s Coq formalization of Separation Logic and a denotational style of axiomatic semantics for a small imperative language with functional abstraction based on Separation Logic. The semantics uses a combination of a State and a Maybe monad to model heap and failed computations. With this I will show the development of a semantics for expressions in Cmm. First ideas to model conditional instructions and jumps will conclude the talk. |
| 19-Dec | Christoph Rauch, Guards! Guards! [pdf-embedder url=”/wp-content/uploads/media/ws17/ober/rauch-guards.pdf” ] | In the recent months, our study of monads with iteration has turned more and more into research focused around guardedness (in our specific sense); from /guarded morphisms/ with respect to some iteration operator, we have gone through /guarded monads/ to obtain a definition of /guarded category/, culminating in Sergey and Lutz coining the term /guarded monoidal category/. In parallel, however, we want to make sense of these developments with examples and applications in programming semantics. In my talk, I will report the status of our efforts to implement the idea of a guarded metalanguage with support for guarded iteration and, eventually, recursion. |
| 12-Dec | Paul Wild, A Fuzzy van Benthem/Rosen theorem [pdf-embedder url=”/wp-content/uploads/media/ws17/ober/wild-fuzzy.pdf” ] | Fuzzy logics extend classical logics by allowing every truth value to be any real number in the interval [0,1] (instead of just 0 and 1). In this talk, the main focus will be on a simple fuzzy modal logic and a version of the van Benthem/Rosen theorem for that logic. Recall that the van Benthem/Rosen theorem for the basic modal logic K states that every bisimulation invariant first order p can be equivalently expressed as a formula of K. Thus, the first prerequisites for a fuzzy version of this theorem are suitable (i.e. fuzzy) notions of bisimulation and bisimulation invariance. It turns out that the concept of bisimulation can be generalised to that of behavioural distance, a (pseudo-)metric measuring how similar two states in a model behave. Bisimulation invariance can then be framed in terms of nonexpansivity with respect to behavioural distance. |
| 05-Dec | Tadeusz Litak, Infinite Populations, Choice and Determinacy [pdf-embedder url=”/wp-content/uploads/media/ws17/ober/freiburg_presentation.pdf” ] | This talk criticizes non-constructive uses of set theory in formal economics. The main focus is on results on preference aggregation and Arrow’s theorem for infinite electorates, but the present analysis would apply as well, e.g., to analogous results in intergenerational social choice. To separate justified and unjustified uses of infinite populations in social choice, I suggest a principle which may be called the “Hildenbrand criterion” and argue that results based on unrestricted Axiom of Choice (AC) do not meet this criterion. The technically novel part is a proposal to use a set-theoretic principle known as the Axiom of Determinacy (AD), not as a replacement for Choice, but simply to eliminate applications of set theory violating the Hildenbrand criterion. A particularly appealing aspect of AD from the point of view of the research area in question is its game-theoretic flavor. |
| 28-Nov | Sergey Goncharov, Unifying Guardedness: From Process Algebra to Hilbert Spaces [pdf-embedder url=”/wp-content/uploads/media/ws17/ober/goncharov-slides.pdf” ] | In models of computation, various notions of guardedness serve to control cyclic behavior by allowing only guarded cycles, with the aim to ensure properties such as solvability of recursive equations or productivity. Typical examples are guarded process algebra definitions, finite delay in online Turing machines, productive definitions in intensional type theory, and even contractive maps in (ultra)metric spaces. We propose an abstract notion of guardedness in the setting of symmetric monoidal categories by postulating certain families of guarded morphisms satisfying few simple axioms. On top of this data, we introduce guarded traces, generalizing the standard setting of symmetric trace monoidal categories. Our approach is instrumental in distinguishing a particularly common type of guardedness via families of morphisms called guarded ideals, whose elements serve as primitive guards. This furthermore allows us to incorporate as a worked example the category of Hilbert spaces and bounded linear maps for which partial traces were previously introduced via the notion of nuclear ideal by Abramsky, Blute, and Panangaden. Surprisingly, we obtain this example as a rather trivial instance: it is an ideally guarded category over the empty class of guards. |
| 21-Nov | Henning Urbat, Free Algebras With Effectful Iteration [pdf-embedder url=”/wp-content/uploads/media/ws17/ober/oberseminar2017_urbat.pdf” ] | For every endofunctor H on an algebraic category C=Alg(T), we introduce a coalgebra \phi H that we propose to serve a semantic domain for finite recursive specifications with a side effect. Such specification are modelled as equation morphisms of the form e: X -> T(HX+A) for a finite set X of variables. The coalgebra \phi H always forms a fixed point of the functor H. In contrast to related concepts such as the rational fixed point, \phi H does not admit a universal property as a coalgebra. However, we can show that \phi H is the initial “ffg-Elgot algebra”, the latter being a generalisation of the notion of an Elgot algebra in the literature. This talk is based on joint work with Jiri Adamek and Stefan Milius. |
| 07-Nov | Thorsten Wißmann, Conditional Transition Systems With Upgrades [pdf-embedder url=”/wp-content/uploads/media/ws17/ober/cts-wissmann.pdf” ] | Conditional Transition Systems arise when modelling software product lines, where a piece of software is available in multiple versions (e.g. a “basic” and a “professional” version). Fixing a particular version, the CTS acts like an ordinary (labelled) transition system, where the set of available transitions depend in on the current version. At any time, the system can upgrade to a higher version in order to activate further transitions. Similarly, the corresponding notion of bisimulation (“conditional bisimulation”) is for each version a traditional bisimulation with additional properties modelling the upgrades.
In the present work, CTSs are modelled as coalgebras in a Kleisli Category of the reader monad on posets. Here, the functor needs to be chosen carefully to obtain precisely the “conditional bisimulation” naturally from the coalgebraic framework. While the plain powerset functor fails to do that, a slightly modified functor does the job. In order to show the similarities between those functors, a generic framework for coalgebras with upgrades is developed. On our way to this main result, we will also use some general ‘fun facts’ about the reader monad. |
| 24-Oct | Cristian Bay, A library for Elgot Monads [pdf-embedder url=”/wp-content/uploads/media/ws17/ober/talk-bay.pdf” ] | I present the results of my master project, supervised by Sergey Goncharov. I developed a Haskell library for complete Elgot monads based on a modification of the free monad transformer introduced by Uustalu et al. to represent the behaviour of CCS-style process algebra. Complete Elgot monads do fit well in the task of implementing such processes, in particular because they allow one to handle unguarded process definitions. A silent feature of the chosen implementation is the possibility to rebase the entire framework on a different kind of effects than mere nondeterminism, specifically, I demonstrate how probabilistic process algebra comes out naturally by replacing nondeterministic choice by probabilistic one. Furthermore, I illustrate the implementation of probabilistic processes by the fair coin tossing simulation protocol by von Neumann [0]. In the remained of the talk I discuss the least fixed-point semantics for preventing possible endless computation loops in iterations.// //[0] https://en.wikipedia.org/wiki/Fair_coin |
Misc
—