## Invited speakers

There will be four invited talks at FCT 2017. The invited speakers are:

- Thomas Colcombet (CNRS, University of Paris-Diderot, France)
- Martin Dietzfelbinger (Technische Universität Ilmenau, Germany)
- Juraj Hromkovič (ETH Zürich, Switzerland)
- Anca Muscholl (University of Bordeaux, France)

- Jean-Éric Pin (CNRS, University of Paris-Diderot, France)

**Thomas Colcombet**is currently a full time senior researcher at the CNRS, working in the Institut de Recherche en Informatique Fondamentale, Paris. After studying at the Ecole Normale Supérieure de Lyon, he received a PhD degree from the university of Rennes. His research is in automata theory in a broad sense, and in particular its connections to algebra, category theory, topology, model theory and algorithmic logic as well as game theory.

**Automata and Program Analysis**

*Based on joint work with Laure Daviaud and Florian Zuleger.*

**Martin Dietzfelbinger**is a full professor of Computer Science (for complexity theory and efficient algorithms) at Technische Universität Ilmenau. He received a Diplom (Master’s degree) Mathematics from the Ludwig Maximilians Universität Munich in 1983, was awarded a PhD degree in Computer Science from the University of Illinois at Chicago in 1987, and completed his hablitation at the University of Paderborn in 1992. Before moving to Ilmenau in 1998, he was a professor in the Computer Science Department of the University of Dortmund for several years. Nowadays, his main research interests lie in understanding the power of randomization in data structures and algorithms. A substantial part of his work deals with different aspects of foundations and applications of hashing in data structures and algorithmics.

**Optimal Dual-Pivot Quicksort: Exact Comparison Count**

*Based on joint work with Martin Aumüller, Daniel Krenn, Clemens Heuberger, and Helmut Prodinger.*

**What one has to know when attacking P vs. NP**

*Based on joint work with Peter Rossmanith.*

Mathematics was developed as a strong research instrument with fully verifiable argumentations. We call any consistent and sufficiently powerful formal theory that enables to algorithmically verify for any given text whether it is a proof or not algorithmically verifiable mathematics (AV-mathematics for short). We say that a decision problem $L \subseteq \Sigma^\ast$ is almost everywhere solvable if for all but finitely many inputs $x \in \Sigma^\ast$ one can prove either “$x \in L$” or “$x \not\in L$” in AV-mathematics.

First, we formalize Rice's theorem on unprovability, claiming that each nontrivial semantic problem about programs is not almost everywhere solvable in AV-mathematics. Using this, we show that there are infinitely many algorithms (programs that are provably algorithms) for which there do not exist proofs that they work in polynomial time or that they do not work in polynomial time. We can prove the same also for linear time or any time-constructible function.

Note that, if $\textsf{P}\ne \textsf{NP}$ is provable in AV-mathematics, then for each algorithm $A$ it is provable that “$A$ does not solve SATISFIABILITY or $A$ does not work in polynomial time”. Interestingly, there exist algorithms for which it is neither provable that they do not work in polynomial time, nor that they do not solve SATISFIABILITY. Moreover, there is an algorithm solving SATISFIABILITY for which one cannot prove in AV-mathematics that it does not work in polynomial time.

Furthermore, we show that $\textsf{P}=\textsf{NP}$ implies the existence of algorithms $X$ for which the true claim “$X$ solves SATISFIABILITY in polynomial time” is not provable in AV-mathematics. Analogously, if the multiplication of two decimal numbers is solvable in linear time, one cannot decide in AV-mathematics for infinitely many algorithms $X$ whether “$X$ solves multiplication in linear time”.

**Anca Muscholl**is Professor of Computer Science at the University of Bordeaux, France, since 2007. Before moving to Bordeaux she was a professor at the University of Paris VII. She received her PhD in 1994 from the University of Stuttgart, and the habilitation in 1999. Her research interests lie in the area of automata, logic, verification and control of concurrent systems. She spent the academic year 2015/16 as a Hans-Fischer Senior Fellow of the Institute of Advanced Study at the Technical University of Munich.

**A tour of recent results on word transducers**

*Based on joint work with Félix Baschenis, Olivier Gauwin and Gabriele Puppis.*

In this talk we survey recent results on regular word transducers. We discuss how some of the classical connections between automata, logic and algebra extend to transducers, as well as some genuine definability questions.

**Jean-Éric Pin**is currently director of research appointed by the CNRS (Centre National de la Recherche Scientifique) and working at IRIF (Institut de Recherche en Informatique Fondamentale), a Joint Research Unit supported by CNRS and University Paris Diderot. He is a leading scientist in the algebraic theory of automata and languages in connection with logic, topology, and combinatorics, but his research has also been influential in other areas. He wrote a number of articles in semigroup theory, most of them motivated by problems issued from automata theory. He is the author of two reference books in automata theory: Varieties of Formal Languages and the monograph Infinite Words, co-authored with D. Perrin. He is also a fellow of the EATCS.

**Some results of Zoltán Ésik on regular languages**

*Talk in memory of Zoltán Ésik.*