IRIF, the Research Institute on the Foundations of Computer Science, is a research laboratory of CNRS and université Paris-Diderot, also hosting two INRIA project-teams.

The research conducted at IRIF is based on the study and understanding of the foundations of all computer science, in order to provide innovative solutions to the current and future challenges of digital sciences.

IRIF hosts about 200 people. Six of its members have been distinguished by the European Research Council (ERC), three are members of the Institut Universitaire de France IUF), and two are members of the Academia Europæa.

Institut Universitaire de France

10.5.2019
IRIF is proud to announce that Constantin Enea, associate professor of Université de Paris and researcher at IRIF, was appointed junior member of IUF. This appointment will allow him to develop a research project concerning rigorous engineering of distributed databases.

Jeremy Siek

9.1.2019
IRIF has the great pleasure to welcome Jeremy Siek, professor at Indiana University Bloomingtom, who is visiting IRIF for five months. Jeremy is the creator of gradual typing and a world-renowed expert in typed programming languages. Meet him in office 4034a.
gradual typing

Gradual typing is a technique that allows the programmer to control which parts of a program check their type correctness (i.e., that apples are added to apples) before execution and which parts check it during their execution instead. It is often used to gradually add the before-execution check to dynamic languages, like JavaScript, which perform the check only at run-time, since it is generally better to find errors before the execution of a program rather than during its execution.
logo-cirm.jpg

9.5.2019
Claire Mathieu, Amaury Pouly and Yann Régis-Gianas from IRIF gave talks at the conference of French preparatory schools to science and engineering curriculum in May 6-10, contributing to the ongoing important changes in Computer Science education in French high-schools and higher-education systems.

7.5.2019
Claire Mathieu from IRIF explained what algorithms are and what is their history to a national French radio broadcast show about Philosophy.

Uri Zwick

1.2.2019
IRIF has the great pleasure to welcome Uri Zwick, professor at the Blavantik School of Computer Sience (University of Tel-Aviv), who is visiting for four months. His stay is financed by an FSMP chair. Uri is an expert in algorithms, data structures and games. Meet him in office 4048.

EATCS

26.4.2019
Seven papers coauthored by IRIF members will be presented at the prestigious conference ICALP'19 in Patras this summer. Topics include automata, games, graphs, quantum computing, randomized complexity, and semigroups.

CIMPA

23.1.2019
A CIMPA school on Graphs, Algorithms and Randomness is co-organized by Reza Naserasr from IRIF at Tabriz University, 15-22 June 2019. Three colleagues from IRIF, Pierre Fraigniaud, Michel Habib and Frédéric Magniez, are among the five lecturers from France.

(These news are displayed using a randomized-priority ranking.)

Higher categories, polygraphs and homotopy
Friday May 24, 2019, 2PM, Salle 1007 - Séance co-organisée avec le groupe de travail “Théorie des types et réalisabilité”
Hugo Moeneclaey (ENS Paris-Saclay) Monoids up to Coherent Homotopy in Two-Level Type Theory

When defining a monoid structure on an arbitrary type in HoTT, one should require a multiplication that is not only homotopy-associative, but also has an infinite tower of higher homotopies. For example in dimension two one should have a condition similar to Mac Lane’s pentagon for monoidal categories. We call such a monoid a monoid up to coherent homotopy. The goal of my internship in Stockholm was to formalize them in Agda. It is well-known that infinite towers of homotopies are hard to handle in plain HoTT, so we postulate a variant of two-level type theory, with a strict equality and an interval type. Then we adapt the set-theoretical treatment of monoids up to coherent homotopy using operads as presented by Clemens Berger and Ieke Moerdijk [1,2].

Our main results are: (a) Monoids up to coherent homotopy are invariant under homotopy equivalence (b) Loop spaces are monoids up to coherent homotopy.

In this talk I will present the classical theory of monoids up to coherent homotopy, and indicates how two-level type theory can be used to formalize it.

References

1. Axiomatic homotopy theory for operads (arxiv.org/abs/math/0206094)

2. The Boardman-Vogt resolution of operads in monoidal model categories (arxiv.org/abs/math/0502155)

Type theory and realisability
Friday May 24, 2019, 2PM, Salle 1007
Hugo Moeneclaey Monoids up to Coherent Homotopy in Two-Level Type Theory

When defining a monoid structure on an arbitrary type in HoTT, one should require a multiplication that is not only homotopy-associative, but also has an infinite tower of higher homotopies. For example in dimension two one should have a condition similar to Mac Lane’s pentagon for monoidal categories. We call such a monoid a monoid up to coherent homotopy. The goal of my internship in Stockholm was to formalize them in Agda. It is well-known that infinite towers of homotopies are hard to handle in plain HoTT, so we postulate a variant of two-level type theory, with a strict equality and an interval type. Then we adapt the set-theoretical treatment of monoids up to coherent homotopy using operads as presented by Clemens Berger and Ieke Moerdijk [1,2].

Our main results are: (a) Monoids up to coherent homotopy are invariant under homotopy equivalence (b) Loop spaces are monoids up to coherent homotopy.

In this talk I will present the classical theory of monoids up to coherent homotopy, and indicates how two-level type theory can be used to formalize it.

References

1. Axiomatic homotopy theory for operads (arxiv.org/abs/math/0206094)

2. The Boardman-Vogt resolution of operads in monoidal model categories (arxiv.org/abs/math/0502155)

Algorithms and complexity
Tuesday May 28, 2019, 11AM, Salle 1007
Simon Apers (INRIA) Quantum Fast-Forwarding: Markov Chains and Graph Property Testing

I will introduce a new tool for quantum algorithms called quantum fast-forwarding (QFF). The tool uses quantum walks as a means to quadratically fast-forward a reversible Markov chain. In a number of quantum walk steps that scales as the square root of the classical runtime, and inversely proportional to the 2-norm of the classical distribution, it retrieves a quantum superposition that encodes the classical distribution. This shows that quantum walks can accelerate the transient dynamics of Markov chains, thereby complementing the line of results that proves the acceleration of their limit behavior.

This tool leads to speedups on random walk algorithms in a very natural way. Specifically I will consider random walk algorithms for testing the graph expansion and clusterability, and show that QFF allows to quadratically improve the dependency of the classical property testers on the random walk runtime. Moreover, this new quantum algorithm exponentially improves the space complexity of the classical tester to logarithmic. As a subroutine of independent interest, I use QFF to determine whether a given pair of nodes lies in the same cluster or in separate clusters. This solves a robust version of s-t connectivity, relevant in a learning context for classifying objects among a set of examples. The different algorithms crucially rely on the quantum speedup of the transient behavior of random walks.

Graphs
Tuesday May 28, 2019, 3PM, Salle 1007
Jean-Florent Raymond (TU Berlin) Enumerating minimal dominating sets in $K_t$-free graphs

In algorithmic enumeration, one is typically asked to output the set of all objects of a certain type related to an input (e.g. all the cycles of a graph, all its maximal cliques, etc.), rather than finding just one. The problem of enumerating all the minimal dominating sets of a graph received an important attention, partly because of its strong links with a fundamental hypergraph problem. A long standing open question is whether the above problem can be solved in (output-) polynomial time. In this talk, I will introduce the problem and present an output-polynomial algorithm for Kt-free graphs. This is joint work with Marthe Bonamy, Oscar Defrain, and Michał Pilipczuk.

Link to the article: https://arxiv.org/abs/1810.00789