IRIF is a research laboratory of CNRS and Université Paris Cité, also hosting one Inria project-team.

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), six are members of the Institut Universitaire de France IUF), two are members of the Academia Europæa, and one is member of Académie des sciences.

25.1.2023
Claire Mathieu, membre de l’IRIF et spécialiste des algorithmes, est intervenue à l’émission Arrêt sur Images autour du ChatGPT. Comment cette IA construit-elle ses textes ? Pourquoi parvient-elle à couvrir à peu près n’importe quel sujet ?

27.1.2023
A full-time research associates position is available to work on the ​VeSyAm research project. The position will start in July 2023. Deadline to apply: 12 noon on 15 Feb 2023. Further information in the job description.

16.1.2023
Claire Mathieu and 8 other authors co-authored the article "Découpage électoral des circonscriptions législatives en France : Déséquilibres démographiques et contraintes territoriales" about a new perspective for understanding electoral maps, using computational social science to study the criteria which shape how electoral districts are drawn up in France.

13.1.2023
Internship proposal for Masters student in computer science at LS2N and IRIF in Real-time analysis and verification of ROS2 robotic applications. To apply, please refer to the internship description.

11.1.2023
LAFI'23, a workshop affiliated to POPL’23 about Languages for Inference, will be held on January 15, 2023, as a bi-located event in Boston and at Université Paris Cité. The Paris antenna will take place in salle Leduc, at the first floor of Saints-Pères building, 45 rue des Saints-Pères, 75006 Paris, from 3pm to 9:30pm Paris time. The The talks of V. Blanchi, G. Caylak, M. Pagani (IRIF), F. Zaiser will happen physically in Paris. Registration is mandatory.

14.12.2022
Ahmed Bouajjani (IRIF) figures among the nine new honorary doctors appointed at Faculty of Science and Technology of Uppsala University. His research focuses on veriﬁcation, speciﬁcation and semantics for parallel and distributed programs and computer systems.

12.12.2022
Jonas Landman, former PhD student at IRIF, is the 2022 winner of a thesis Prize from Chancellerie des Universités de Paris. His thesis “Quantum Algorithms for Unsupervised Machine Learning and Neural Networks” was awarded in the All Specialties Science Prize Category.

30.11.2022
Sophie Laplante (IRIF) and Anupa Sunny (IRIF) will present at ITCS 2023 their paper Certificate Games in which players are given inputs x, y such that f(x)\≠f(y). Their goal is to find a position where the bits of their inputs differ. This simple new game can be used to give bounds on query complexity, block sensitivity and several other complexity measures.

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

Algorithms and complexity
Monday January 30, 2023, 11AM, Salle 3052
Samson Wang (Imperial College London) Qubit-Efficient Randomized Quantum Algorithms for Linear Algebra

We propose a class of randomized quantum algorithms for the task of sampling from matrix functions, without the use of quantum block encodings or any other coherent oracle access to the matrix elements. As such, our use of qubits is purely algorithmic, and no additional qubits are required for quantum data structures. For NxN matrices, the space cost is log(N)+2 qubits and depending on the structure of the matrices, the gate complexity can be comparable to state-of-the-art methods that use quantum data structures of up to size O(N^2), when considering equivalent end-to-end problems. Within our framework, we present a quantum linear system solver that allows one to sample properties of the solution vector, as well as an algorithm for sampling properties of ground states of Hamiltonians. As a concrete application, we combine these two sub-routines to present a scheme for calculating Green's functions of quantum many-body systems.

Verification
Monday January 30, 2023, 11AM, 1007 and Zoom link
Sylvain Perifel (IRIF) Deterministic pushdown automata can compress some normal sequences

Joint work with O. Carton

Normality has been introduced by É. Borel more than one hundred years ago. A real number is normal to an integer base if, in its infinite expansion expressed in that base, all blocks of digits of the same length have the same limiting frequency. Normality can also be characterized by non-compressibility by finite state machines. In this talk, we will present a new result showing that pushdown machines, even deterministic, can compress some normal sequences. This solves positively a question left open by V. Becher, P. A. Heiber and O. Carton.

One world numeration seminar
Tuesday January 31, 2023, 2PM, Online
Slade Sanderson (Universiteit Utrecht) Matching for parameterised symmetric golden maps

In 2020, Dajani and Kalle investigated invariant measures and frequencies of digits of signed binary expansions arising from a parameterised family of piecewise linear interval maps of constant slope 2. Central to their study was a property called ‘matching,’ where the orbits of the left and right limits of discontinuity points agree after some finite number of steps. We obtain analogous results for a parameterised family of ‘symmetric golden maps’ of constant slope $\beta$, with $\beta$ the golden mean. Matching is again central to our methods, though the dynamics of the symmetric golden maps are more delicate than the binary case. We characterize the matching phenomenon in our setting, present explicit invariant measures and frequencies of digits of signed $\beta$-expansions, and—time permitting—show further implications for a family of piecewise linear maps which arise as jump transformations of the symmetric golden maps.

Joint with Karma Dajani.

Algorithms and complexity
Wednesday February 1, 2023, 2PM, Salle 3052

Correlation clustering is a classic model for clustering with several applications in data mining and unsupervised machine learning. In this problem, we are given a complete graph where each edge is labeled + or -; and the goal is to find a partition of the vertex set so as to minimize the number of + edges across the parts of the partition plus the number of – edges within the parts of the partition.

We will first present a new result showing that a constant number of rounds of the Sherali-Adams hierarchy yields a strict improvement over the natural LP: we present the first better-than-two approximation for the problem, improving upon the previous approximation of 2.06 of Chawla, Makarychev, Schramm, Yaroslavtsev based on rounding the natural LP (which is known to have an integrality gap of 2). We will then review several recent ideas which have led to practical constant factor approximations to Correlation Clustering in various setups: distributed and parallel environments, differentially-private algorithms, dynamic algorithms, or sublinear time algorithms.

This is a combination of joint works with Euiwoong Lee, Alantha Newman, Silvio Lattanzi, Slobodan Mitrovic, Ashkan Norouzi-Fard, Nikos Parotsidis, Jakub Tarnawski, Chenglin Fan and Andreas Maggiori.

Enumerative and analytic combinatorics
Thursday February 2, 2023, 11AM, IHP
Seminaire Flajolet (Vincent Juge, Jang Soo Kim, Olya Mandelshtam) IHP

PhD students seminar
Thursday February 2, 2023, 4PM, 3052 and Zoom link
Aymeric Walch The categorical semantic iceberg finally explained

Denotational semantic is a field which consists in studying computation without computing. That is, a program P of type int → int can be seen on a high level as a function from the integers to the integers.

After a quick review of the idea behind denotational semantic, we will show that the word “denotational” can in fact be replaced by the word “categorical”. A program will not be interpreted as a mere function, but rather as a morphism in some category. This enlargement of perspective allows us to consider a lot more interesting interpretations for programs: relations, games, probability kernels…

We will then cover the basic categorical ingredients that makes a category a good candidate for interpreting computation. That is, a category must handle tupling and curryfication. If the time allows for it, we will then quickly introduce how those categorical ideas lead to the development of linear logic.

This talk *will not* assume any prior knowledge in category theory nor in denotational semantic.

Analysis and conception of systems
Thursday February 2, 2023, 2PM, salle séminaires au plateau SCAI +(Esclangon, 1er étage, campus Jussieu)
Marine Minier (Université de Lorraine) Comment les outils automatiques peuvent nous aider, nous cryptographes

Higher categories, polygraphs and homotopy
Friday February 3, 2023, 2PM, Salle 1007
Pierre-Louis Curien & Guillaume Laplante-Anfossi (IRIF & Melbourne University) Une preuve simple et connexe du théorème de cohérence de MacLane

Bien que le théorème de cohérence de MacLane pour les catégories monoïdales ait été prouvé initialement par une méthode proche de la réécriture, il présente un caractère topologique. C’est ce qui a poussé Kapranov à suggérer en 1993 une « preuve instantanée » de ce théorème basée sur l’existence d'une famille de polytopes qu’il nomme permutoassociaèdres. Dans la première partie, on formalisera cette idée, montrant que la cohérence de MacLane est une conséquence directe de la simple connexité des permutoassociaèdres. Cela suggère un lien combinatoire plus général entre cohérence n-catégorique et n-connexité de certains espaces, avatar « strict » de travaux infini-catégoriques récents de Shaul Barkan.

Dans la deuxième partie, on s'intéressera à l'instanciation du théorème général à la classe des “hypergraph polytopes” (aussi connus sous le nom de nestoèdres), dont les faces (et en particulier les sommets et les arêtes) sont décrits par des objets combinatoires appelés “constructs”. Les arêtes sont naturellement orientées à l'aide d'un ordre appelé ordre de Tamari généralisé, et lorsqu'on instancie encore davantage, à la classe des opéraèdres, on obtient un système de réécriture de termes convergent (sous-jacent au problème de cohérence des opérades catégorifiées de Dosen et Petric), ce qui permet dans ce cas d'obtenir la cohérence par des méthodes de réécriture (complétion de Squier). Les diagrammes obtenus sont légèrement différents de ceux de Dosen et Petric.

Automata
Friday February 3, 2023, 2PM, Salle 3052
Florent Koechlin Two criteria to prove the inherent ambiguity of bounded context-free languages

A context-free language is inherently ambiguous if any grammar recognizing it is ambiguous, i.e. there is a word that is generated in two different ways. Deciding the inherent ambiguity of a context-free language is a difficult problem, undecidable in general. The first examples of inherently ambiguous languages were discovered in the 1960s, using iteration techniques on derivation trees. They belonged to a particular subfamily of context-free languages, called bounded context-free languages.
    Although they made it possible to prove the inherent ambiguity of several languages, as for example the language L = a^n b^m c^p with n=m or m=p, iteration techniques are still very laborious to implement, are very specific to the studied language, and seem even sometimes unadapted. For instance, the relative simplicity of the proof of inherent ambiguity of L completely collapses by replacing the constraint "n=m or m=p" by "n≠m or m≠p".
In this talk, I will present two useful criteria based on generating series to prove easily the inherent ambiguity of some bounded context-free languages. These languages, which have a rational generating series, resisted both the classical iteration techniques developed in the 1960’s and the analytic methods introduced by Philippe Flajolet in 1987.

Verification
Monday February 6, 2023, 11AM, 1007 and Zoom link
Claudio Gomes (University of Aarhus) Application of formal methods to verification of self-adaptation loops in digital twins

The performance and reliability of Cyber-Physical Systems are increasingly aided through the use of digital twins, which mirror the static and dynamic behaviour of a Cyber-Physical System (CPS) in software. Digital twins enable the development of self-adaptive CPSs which reconfigure their behaviour in response to novel environments. It is crucial that these self-adaptations are formally verified at runtime, to avoid expensive re-certification of the reconfigured CPS. In this talk, I discuss formally verified self-adaptation in a digital twinning system, by constructing a non-deterministic model which captures the uncertainties in the system behaviour after a self-adaptation. We use Signal Temporal Logic to specify the safety requirements the system must satisfy after reconfiguration and employ formal methods based on verified monitoring over Flow* flowpipes to check these properties at runtime. This gives us a framework to predictively detect and mitigate unsafe self-adaptations before they can lead to unsafe states in the physical system.