chateau_d_if.jpeg

CSL 2016 main conference: invited speakers

  • Libor Barto (Charles University in Prague)

    The computational and descriptive complexity of finite domain fixed template constraint satisfaction problem (CSP) is a well developed topic that combines several areas in mathematics and computer science. Allowing the domain to be infinite provides a way larger playground which covers many more computational problems and requires further mathematical tools. I will talk about some of the research challenges and recent progress on them.

    • Aug. 29, 2016, 9 a.m.
  • Agata Ciabattoni (Technische Universität Wien)

    The possession of a suitable proof-calculus is the starting point for many investigations into a logic, including decidability and complexity, computational interpretations and automated theorem proving. By suitable proof-calculus we mean a calculus whose proofs exhibit some notion of subformula property (`analyticity'). In this talk we describe a method for the algorithmic introduction of analytic sequent-style calculi for a wide range of non-classical logics starting from Hilbert systems. To demonstrate the widespread applicability of this method, we discuss how to use the introduced calculi for proving various results ranging from Curry-Howard isomorphism to new interpretative tools for Indology.

    • Aug. 31, 2016, 9 a.m.
  • Nicolai Kraus (University of Nottingham)
    • Aug. 31, 2016, 2 p.m. — Ackermann Award
  • Anca Muscholl (Université Bordeaux & Institut Universitaire de France)

    Synthesis is a particularly challenging for concurrent programs. At the same time it is a very promising approach, since concurrent programs are difficult to get right, or to analyze with traditional verification techniques. The talk provides an introduction to distributed synthesis in the setting of Mazurkiewicz traces, and its applications to decentralized runtime monitoring.

    • Aug. 30, 2016, 9 a.m.
  • Alexandra Silva (University College London)

    The area of automata learning was pioneered by Angluin in the 80's. Her original algorithm, which applied to regular languages and deterministic automata, has been extended to various types of automata and used in software and hardware verification. In this talk, we will take an abstract perspective at automata learning. We show how the correctness of the original algorithm and many extensions can be captured in one proof using coalgebraic techniques. We also show that a novel algorithm for nominal automata can be derived from the abstract framework.

    • Sept. 1, 2016, 9 a.m.