Vorträge im WS 2016

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 2016

—

Bisherige Vorträge

Date Speaker, Topic Abstract
7-Feb Paul Wild, Correspondence theory for a description logic of change [pdf-embedder url=”/wp-content/uploads/media/ws16/ober/wild-slides.pdf” ] The van Benthem-Rosen theorem states that modal logic is precisely the bisimulation invariant fragment of first-order logic. That is, every modal formula is invariant under bisimulations of Kripke models, and conversely every bisimulation invariant first-order formula is equivalent to a modal one.
The goal of this talk (and my ongoing Master thesis) is to establish an analogous characterisation of the modal description logic S5-ALC as the bisimulation invariant fragment of the modal first-order logic S5-FOL. In S5-ALC, Kripke frames are two-dimensional, with one dimension of possible worlds, connected by an S5 frame and one dimension of individuals, connected by the usual roles. I will show how bisimulation and other concepts from modal logics generalize to this two-dimensional setting and give an overview of the steps involved in proving the characterisation theorem.
31-Jan Ludwig Dietel, Implementierung eines koalgebraischen EL-Reasoners [pdf-embedder url=”/wp-content/uploads/media/ws16/ober/dietel-slides.pdf” ] Im koalgebraischen Reasoner COOL wurde ein koalgebraischer EL-Reasoner implementiert. EL ist die Einschränkung auf konjunktive Fragmente der vollen Logik und erlaubt die Entscheidung des Subsumtionsproblems in polynomieller Zeit. Dazu wird eine generische Implementierung der Tableauregeln für koalgebraische Logiken verwendet. Dazu muss zuvor die TBox in polynomieller Zeit normalisiert werden, um anschließend eine Modellkonstruktion durchzuführen. Die Konstruktion eines WSI-Modells für konjunktive koalgebraische Fixpunktlogiken in polynomieller Zeit geschieht durch eine generische Implementierung der Tableauregeln. Im Anschluss daran müssen die Extensionen der definierten Variablen in der TBox in polynomieller Zeit durch eine generische Implementierung berechnet werden und anschließend ein Model Checking unter der Verwendung der generische Implementierung durchgeführt werden.
31-Jan Johannes Kern, Satisfiability Checking in the Coalgebraic Hybrid mu-Calculus [pdf-embedder url=”/wp-content/uploads/media/ws16/ober/kern-slides.pdf” ] The coalgebraic hybrid mu-Calculus extends the coalgebraic mu-Calculus by so-called nominals, an additional kind of propositional atoms that have to be true in exactly one state of a model, and by global diamonds and boxes. In this talk, a translation of that logic into its nominal-free fragment will be presented, which is based on a similar translation for the ‘classical’ hybrid mu-Calculus with Kripke semantics [1].
[1] Carlos Areces and Balder ten Cate. Hybrid logics. In Patrick Blackburn, J. F. A. K. van Benthem, and Frank Wolter, editors, Handbook of modal logic, pages 851-852. Elsevier, Amsterdam, Boston, 2007.
17-Jan & 24-Jan Daniel Hausmann, New Satisfiability Algorithms for Coalgebraic mu-Calculi [pdf-embedder url=”/wp-content/uploads/media/ws16/ober/hausmann-slides.pdf” ] In previous talks, we have considered global caching algorithms for the flat and alternation-free fragments of the coalgebraic mu-calculus and observed their close relation to satisfiability games. In this talk, I will present two new algorithms: To begin with, we will look at a satisfiability algorithm for the aconjunctive, alternation-free fragment. While this algorithm is formulated as (and enjoys the benefits of) a global caching algorithm, it generalizes the focus games for CTL [Lange, Stirling, 2001] to the aconjunctive, alternation-free case. Afterwards, we will consider a global caching algorithm for the full mu-calculus. This algorithm essentially integrates the construction and Safra/Piterman-style determinization of a parity automaton as well as the solving of the resulting parity game, all on-the-fly. This enables closing tableaux for the full mu-calculus early. The presented algorithms are formulated in coalgebraic generality and are sound, complete and optimal.
20-Dec Thorsten Wißmann, A coalgebraic and categorical Paige Tarjan Algorithm [pdf-embedder url=”/wp-content/uploads/media/ws16/ober/thorsten-slides.pdf” ] The algorithm by Paige and Tarjan computes behaviourally equivalent states in a transition system. In other words, it computes the coarsest quotient of a coalgebra of the Powerset functor. In this talk we will see how to generalize the algorithm to a construction for coalgebras on an arbitrary category, not necessarily Set. Therefore, it is necessary to generalize the set-theoretic constructions to element-free constructions and to rephrase the algorithm’s properties with categorical notions. The generalization results in two categorical constructions: one more general and one faster but less general coalgebraic framework. The ’œfaster’ version instantiates to the classical Paige-Tarjan-algorithm, but also to variations of this algorithm for other functors.
13-Dec Christoph Rauch, Towards a Monadic Metalanguage for (Un)guarded Recursion: A Monad for Infinite Traces [pdf-embedder url=”/wp-content/uploads/media/ws16/ober/christoph-slides.pdf” ] Program language semantics constitute a perfect playground for seeing models of iteration, like completely iterative or Elgot monads, in action. I explore our recent results about iteration and abstract guardedness, introduced to you in Sergey’s talk, by applying them to a type-theoretic coinductive semantics for a While language developed in a series of papers by Nakata and Uustalu, as a starting point towards a metalanguage parametric in an arbitrary monad with support for iteration for guarded morphisms. Concretely, I present a monad capable of giving a trace semantics to possibly non-terminating programs which is abstractly guarded and guarded iterative, but not completely iterative or Elgot, and its implementation in the proof assistant Coq.
13-Dec Sergey Goncharov, Unifying Guarded and Unguarded Iteration [pdf-embedder url=”/wp-content/uploads/media/ws16/ober/sergey-slides.pdf” ] Guarded and unguarded recursion are two well-established principles in semantics, greatly influencing the development of program and specification languages, their usage and the corresponding reasoning techniques. The unguarded recursion is inherent to the comprehensive and elaborated doctrine of domain theory, where programs are viewed through the lens of Scott’s information increase partial order, and therefore recursion arises as a least solution of fixpoint equations. Guarded recursion, to the contrary, stems from process algebra, and is based on unique solutions of guarded recursive specifications, where guardedness can be understood as the requirement for computations to be continuously productive. None of the two approaches cover fixpoints that are neither least nor unique, which e.g. happens to be the case in process algebra once the requirement of guardedness is lifted. In my talk I present recent results of the ongoing effort on unifying notions of recursion based on complete Elgot monads. A new core concept developed as part of this work is that of abstractly guarded monad, which come equipped with a general axiomatic notion of guardedness. The main result linking guarded and unguarded recursion and justifying this approach is that complete Elgot monads are certain iteration-preserving collapses of abstractly guarded monads with iteration.
6-Dec Stefan Milius, One Eilenberg Theorem to Rule Them All [pdf-embedder url=”/wp-content/uploads/media/ws16/ober/stefan-slides.pdf” ] Eilenberg-type correspondences, relating varieties of languages (e.g. of finite words, infinite words, or trees) to pseudovarieties of finite algebras, form the backbone of algebraic language theory. Numerous such correspondences are known in the literature. We demonstrate that they all arise from the same recipe: one models languages and the algebras recognizing them by monads on an algebraic category, and applies a Stone-type duality. Our main contribution is a generic variety theorem that covers more than a dozen Eilenberg-type correspondences in the literature, among them e.g. Wilke’s and Pin’s work on infinity-languages as well as the recent variety theorem for cost functions of Daviaud, Kuperberg, and Pin, and unifies the two previous categorical approaches of Bojanczyk and of Adamek et al. In addition it gives a number of new results, such as an extension of the local variety theorem of Gehrke, Grigorieff, and Pin from finite to infinite words.
29-Nov Fatemeh Seifan, Completeness for Coalgebraic Fixpoint Logic [pdf-embedder url=”/wp-content/uploads/media/ws16/ober/fatemeh-slides.pdf” ] We introduce an axiomatization for the coalgebraic fixed point logic which was introduced by Venema as a generalization, based on Moss’ coalgebraic modality, of the well-known modal mu-calculus. Our axiomatization can be seen as a generalization of Kozen’s proof system for the modal mu-calculus to the coalgebraic level of generality. It consists of a complete axiomatization for Moss’ modality, extended with Kozen’s axiom and rule for the fixpoint operators. Our main result is a completeness theorem stating that, for functors that preserve weak pullbacks and restrict to finite sets, our axiomatization is sound and complete for the standard interpretation of the language in coalgebraic models. The proof we present is based on automata-theoretic ideas: in particular, we introduce the notion of consequence game for modal automata, which plays a crucial role in the proof of our main result. The result generalizes the celebrated Kozen-Walukiewicz completeness theorem for the modal mu-calculus, and our automata-theoretic methods simplify parts of Walukiewicz’ proof.
22-Nov Peter Trommler, From Shared Term Graph to the Spineless Tagless G-Machine in Coq [pdf-embedder url=”/wp-content/uploads/media/ws16/ober/peter-slides.pdf” ] Shared Term Graph (STG) is an intermediate language in the Glasgow Haskell Compiler (GHC). In my talk I present a Coq verified derivation of the STG machine by Pirog and Biernacki and report on first steps towards proof automation following Chlipala’s proof style. On small example I demonstrate the development of a certified program with a fully automated proof.
15-Nov Tadeusz Litak, // Arrows and Boxes// [pdf-embedder url=”/wp-content/uploads/media/ws16/ober/tadeusz-slides.pdf” ] This talk, based on joint work with Albert Visser (Utrecht), is a continuation of the one I gave in December 2014. This time, things are going to be more streamlined, and the material is developed both in width and in depth. Recall that over classical propositional base, standard normal modal logic can be developed either with unary “box” or binary “strict implication” (“Lewis arrow”) as a primitive. Over intuitionistic propositional base, however, these two setups are not just syntactic variants of each other: that of the Lewis’ arrow is richer and more expressive. This has been discovered by authors working on metatheory of Heyting Arithmetic (Visser, Iemhoff, de Jongh, Zhou…). Curiously enough, the same distinction underlies the discussion of “arrows” (Hughes, Lindley, Wadler, Yallop, Atkey, Jacobs, Heunen, Hasuo…) and “idioms” (McBride, Patterson) in functional programming, though I would suggest these arrows are called “strong arrows”, as they form a narrow subclass of Lewis’ arrows.

This is roughly what we learned last time. Now, I am going to present a systematic overview of the present state of knowledge, including results obtained by us. I will present Hilbert-style (and possibly some Gentzen-style) axiomatizations of minimal systems in various signatures and their most interesting extensions. I will discuss completeness results. I will discuss in more detail the matter of arithmetical interpretation and its present and potential connection with the work on guarded (co-)recursion and results on fixpoint definability for corresponding logics. I will explain the connection with, on the one hand, the close connection with “weak logics with strict implication” and “weak Heyting algebras” and, on the other hand, the not-so-close connection with BI: another system combining intuitionistic logic with an additional form of implication. I will show how one can extend the Gödel-(McKinsey-Tarski) translation of logics with Lewis’ arrow into classical modal logics with two unary boxes, obtaining in the process uniform proofs of completeness, fmp, canonicity and correspondence. I would be happy to conclude by discussing how semantic proofs of uniform interpolation work naturally for several systems of strong arrows, but I am afraid time will not allow for that.
8-Nov Ulrich Rabenstein/Miriam Polzer, Double Negation Translation of Intuitionistic Modal Logic in Coq [pdf-embedder url=”/wp-content/uploads/media/ws16/ober/miriam-ulrich-slides.pdf” ] Double-negation translations, which are closely related to continuation-passing style due to the Curry-Howard isomorphism, are used to embed a classical logic into its intuitionistic counterpart. Based on Tadeusz Litak’s ALCOP 2016 presentation, we have formalized several double-negation translations for modal logic with only one modal operator in Coq. Those translations do not work for logics with arbitrary additional axioms, hence we investigate classes of axioms for which they behave as expected. As a proof system we use the normalizing natural deduction system proposed by Bellin, de Paiva and Ritter [1].

[1] Gianluigi Bellin, Valeria De Paiva, and Eike Ritter. “Extended Curry-Howard correspondence for a basic constructive modal logic.” In Proceedings of Methods for Modalities. 2001.
8-Nov Dominik Paulus, A classroom-oriented formalization of separation logic [pdf-embedder url=”/wp-content/uploads/media/ws16/ober/dominik-slides.pdf” ] Separation logic is an extension to Hoare logic which permits reasoning about imperative programs that involve dynamic memory allocation and shared mutable data structures. Based on the existing material from Software Foundations by Benjamin Pierce et al., I have implemented a formalization of separation logic in Coq. I will give a brief introduction to separation logic, show my implementation and highlight some design decisions along with possible alternatives to them.
25-Oct Baltasar Trancón y Widemann, The Virtue of Vicious Circles [pdf-embedder url=”/wp-content/uploads/media/ws16/ober/baltasar-slides.pdf” ] It is common for programming languages to implement structured data as directed graphs in memory, with cells/objects for nodes and pointers/references for edges. Cycles can arise by mutually recursive definition or destructive assignment, which makes processing such data cumbersome: Naive recursive traversals of the graph diverge, whereas graph algorithms work at too low levels of abstraction. Lazy functional programming can deal productively with a certain restricted class of algorithms on infinite graphs, with cyclical ones as a special case. In this talk, an alternative view is presented. It relies on coalgebraic semantics of data graphs, and coinductive denotational semantics for (co)recursive functions on finite cyclical graphs. Operational semantics are discussed in terms of a function calling convention with several effective and transparent cycle detection and handling strategies. The algorithmic expressive power of the approach is illustrated with examples both straightforward and surprising, most of which cannot be emulated by laziness. Interestingly, the biggest unsolved problem is syntactic; namely to find an adequate front-end notation that leverages the technique in a corecursive functional programming language.