Vorträge im SS 2013 - Lehrstuhl für theoretische Informatik 8

Das Oberseminar des Lehrstuhls für Theoretische Informatik findet Dienstags von 14:15-15:45 in Raum 11.150-113 in der Martensstr. 3 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).

Bisherige Vorträge


Date	Speaker, Topic	Abstract
16-Jul	Volker Strehl, Hunting for the second largest eigenvalue … of what? why? how? [pdf-embedder url=”/wp-content/uploads/media/ss13/ober/strehl.pdf” ]	The mixing behavior of markovian random walks on graphs and networks depends on the spectra (eigenvalues) of their transition matrices. The talk reports on earlier and recent investigations (joint work with Christian Riess (Informatik 5) and Rolf Wanka (Informatik 12)) on the spectra of two popular families of networks: cube-connected cycles (CCC) and shuffle-exchange (SE), preferring general ideas and illustrations to involved technicalities. I will try to make the talk fruitful and enjoyable.
9-Jul	Ray-Ming Chen , Introduction to Intuitionistic Set Theories	The history of set theories goes over a century: from Georg Cantor’s naive set theory, to Zermelo-Fraenkel classical set theory, to John-Myhill’s intuitionistic set theory, and to Peter Aczel’s constructive set theory. Each new version of set theory has revolutionized and enriched the landscapes of set theories. Every progress also indicates the advance of human reasoning on the foundation of mathematics, philosophy and computability theory.
2-Jul	Andrei Popescu, Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving (joint work with Dmitriy Traytel and Jasmin Blanchette) [pdf-embedder url=”/wp-content/uploads/media/ss13/ober/popescu.pdf” ]	Interactive theorem provers based on higher-order logic (HOL) traditionally follow the definitional approach, reducing high-level specifications to logical primitives. This also applies to the support for datatype definitions. However, the internal datatype construction used in HOL4, HOL Light, and Isabelle/HOL is fundamentally noncompositional, limiting its efficiency and flexibility, and it does not cater for codatatypes. I shall present a fully modular framework for constructing (co)datatypes in HOL, with support for mixed mutual and nested (co)recursion. Mixed (co)recursion enables type definitions involving both datatypes and codatatypes, such as the type of finitely branching trees of possibly infinite depth. The framework draws heavily from category theory. The key notion is that of a bounded natural functor—an enriched type constructor satisfying specific properties preserved by interesting categorical operations. The framework is implemented as a definitional package in Isabelle, addressing a frequent request from users.
18-Jun	Tadeusz Litak, Sticking the triangle in all the right places: Löb meets Conway	This is a joint work in progress with Stefan Milius. Motivated by the recent interest in models of guarded recursion we study the equational properties of guarded fixpoint operators. We formulate axioms for guarded fixpoint operators generalizing the axioms of iteration theories of Bloom and Ã‰sik. Models of these axioms include both standard (e.g., cpo-based) models of iteration theories and models of guarded recursion such as complete metric spaces or the topos of trees studied by Birkedal et al. We also discuss the connection with other settings such as fixpoint monads of Crole and Pitts, iterative monads or Elgot theories. We show that the standard result on the satisfaction of all Conway axioms by a unique dagger operation generalizes to the guarded setting. We also introduce the notion of guarded trace operator on a category, and we prove that guarded trace and guarded fixpoint operators are in one-to-one correspondence. Our results are intended as first steps leading to the description of classifying theories for guarded recursion and hence completeness results involving our axioms of guarded fixpoint operators in future work.
11-Jun	Daniel Gorín, Coalgebraic Announcement Logics [pdf-embedder url=”/wp-content/uploads/media/ss13/ober/gorin.pdf” ]	In epistemic logic, dynamic operators describe the evolution of the knowledge of participating agents through communication, one of the most basic forms of communication being public announcement. Semantically, dynamic operators correspond to transformations of the underlying model. While metatheoretic results on dynamic epistemic logic so far are largely limited to the setting of Kripke models, there is evident interest in extending its scope to non-relational modalities capturing, e.g., uncertainty or collaboration. We develop a generic framework for non-relational dynamic logic by adding dynamic operators to coalgebraic logic. We discuss a range of examples and establish basic results including bisimulation invariance, complexity, and a small model property.
4-Jun	Daniel Hausmann, Flat coalgebraic fixed point logics II [pdf-embedder url=”/wp-content/uploads/media/ss13/ober/hausmann.pdf” ]	As we have previously seen, various modal logics (including e.g. logics with non-normal or binary modal operators) may be defined in the framework of coalgebraic (modal) logic in a swift and generic manner. Under the assumption that a coalgebraic modal logic is defined exclusively by use of so-called predicate liftings which are monotone w.r.t. subset inclusion, we have seen that the logic at hand latently contains least and greatest fixed points of so-called fixed point schemes. This justifies the extension of the logic by explicit (flat) fixed point operators, resulting in such logics as PLTL, CTL, ATL (depending on the original logic that we started from). Our central desire in this context is the provision of a correct solution to the satisfiability / provability problem of such coalgebraic fixed point logics. We will now delve deeper into the details of the proposed solution – the so-called focussing global caching algorithm, the correctness of which we aim to show. At the heart of the correctness proof lies a non-standard model construction, which employs information gathered by the global caching algorithm for the definition of a so-called pre-tableau in order to ensure that the prospective model coalgebra actually respects fixed points and thus is indeed a model. We will consider several illustrating examples in order to comprehend the involved structures and mechanisms.
28-May	Mihai Codescu, Proof Support for Common Logic (jointly with T. Mossakowski, O. Kutz, C. Lange, M. Grüninger) [pdf-embedder url=”/wp-content/uploads/media/ss13/ober/codescu.pdf” ]	Common Logic is an ISO-standardised language based on first-order logic, created for knowledge representation in the context of the Web. We present the theoretical background for an extension of the Heterogeneous Tool Set HETS that enables proof support for Common Logic. This is achieved via logic translations that relate Common Logic and some of its sublogics to already supported logics and automated theorem proving systems. We thus provide the first theorem proving support for Common Logic covering the full language, including the possibility of verifying meta-theoretical relationships between Common Logic theories.
14-May	Christoph Rauch, Hoare Logic for Exceptional Effects [pdf-embedder url=”/wp-content/uploads/media/ss13/ober/rauch.pdf” ]	I will present my ongoing master’s thesis. Based on work by Lutz Schröder and Sergey Goncharov, I am exploring the extension of a relatively complete Hoare calculus for a monadic metalanguage supporting generic effects and loops via order-enrichment of the underlying monad. Although exceptions are generally supported in this framework, exception handling is not. To remedy this, exception raising and handling are added directly to the language. In addition, the Hoare calculus needs to be adjusted such that it allows verification of programs terminating abnormally. A primary goal for the thesis is to lift the completeness result to the modified calculus.
7-May	Sergey Goncharov, Trace Semantics via Generic Observations [pdf-embedder url=”/wp-content/uploads/media/ss13/ober/goncharov.pdf” ]	Recent progress on defining abstract trace semantics for coalgebras rests upon two observations: (i) coalgebraic bisimulation for deterministic automata coincides with trace equivalence, and (ii) the classical powerset construction for automata determinization instantiates the generic idea of lifting a functor to the Eilenberg-Moore category of an appropriate monad T. We take this approach one step further by rebasing the latter kind of trace semantics on the novel notion of T-observer, which is just a certain natural transformation of the form F â†’ GT , and thus allowing for elimination of assumptions about the structure of the coalgebra functor. As a specific application of this idea we demonstrate how it can be used for capturing trace semantics of push-down automata. Furthermore, we show how specific forms of observers can be used for coalgebra-based treatment of internal automata transitions as well as weak bisimilarity of processes.
29-Apr	Lutz Schröder, Coalgebraic Simulation and Lightweight Description Logics (joint work with Daniel Gorín)	Lightweight description logics of the EL family ensure efficient decidability of the main reasoning problems by restricting to a language fragment where tableaux can be seen as rooted canonical models, in the sense that satisfaction of a formula in a model is equivalent to simulation of its unique tableau. We explore the generalization of this concept to the coalgebraic case, thus covering a broader range of base modalities such as probabilistic modalities or monotone neighbourhood logic. To this end, we introduce a suitable notion of modal simulation and then develop a theory of canonical models.