Welcome 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. Seven 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. Notion of the day Social Networks Follow us on Twitter/X, LinkedIn and Mastodon for our latest news: News 5.11.2024 This year, three IRIF researchers are part of two projects that have won a 2025 Synergy Grant from the European Research Council (ERC). Many congratulations to Valérie Berthé, Hugo Herbelin and Paul-André Melliès ! IRIF wishes them successful results. 12.11.2024 The LVP (Languages and Program Verification) working group of the GPL GdR of the CNRS will be holding its one-day conference on Thursday 14 November 2024 at IRIF, from 9am to 5.40pm. Emilio Jesús Gallego Aria, Inria researcher at IRIF, University of Paris, will be giving a talk on : ‘Flèche: Incremental Validation for Hybrid Formal Documents’. This event is free but registration is required. 24.10.2024 The Innovation Prize has been awarded to Sergio Rajsbaum, associate member of IRIF, in recognition of his significant contribution to Distributed Computing. The prize will be presented to him at the SIROCCO'25 conference in Delphi, Greece. 24.10.2024 Does Computer Science Have a Future? That is the question to be debated during the third conference, “We Turn Off, We Reflect, We Discuss,” organized at Université Paris Cité by François Laroussinie. José Halloy (LIED) and Anne-Laure Ligozat (LISN) are the invited speakers. It will take place on December 10, 2024, from 4:15 PM to 6:30 PM. This event is free of charge. 31.10.2024 IRIF is excited to host Dexter Kozen from Cornell University as a speaker in our Distinguished Talks series. The talk will take place on December 03, 2024, starting at 11a.m. More details to come! 30.9.2024 Jean-Louis Krivine, Professor Emeritus at IRIF, has published a book entitled ‘Les décompilateurs - L'Univers en tête’. In it you will find, among other things, a reflection on the origin of mathematics and the link between logic and theoretical computing, as well as some paradoxes in quantum mechanics. 25.9.2024 CNRS Computer Science is organizing the conference “Optimization: at the Heart of Challenges in Computer Science” which will take place on October 3, 2024, at the CNRS Headquarters. This event, aimed at industry professionals, decision-makers, and journalists, brings together the scientific community to exchange and share knowledge on this cross-disciplinary topic. Claire Mathieu, Simon Apers and David Saulpic will give talks. 18.9.2024 Neha Rino (MPRI intern at IRIF in 2023), Eugène Asarin and Mohammed Foughali won the Best Paper Award at FORMATS. This work formulate and solve by an efficient algorithm the problem of quantitative monitoring: compute a real number characterizing to which extent the given trace of a real-time system satisfies its specification. edit all the past news (These news are displayed using a randomized-priority ranking.) Agenda Automata Friday November 15, 2024, 2PM, Salle 3052 Luc Dartois (LACL) Reversible Transducers over Infinite Words Deterministic two-way transducers capture the class of regular functions. The efficiency of composing two-way transducers has a direct implication in algorithmic problems related to synthesis, where transformation specifications are converted into equivalent transducers. These specifications are presented in a modular way, and composing the resultant machines simulates the full specification. In this talk, I will present how we can achieve efficient composition of two-way transducers, mainly through the use of Reversible Transducers. Reversible machines are machine that are both deterministic and codeterministic. I will show how any two-way transducers can be made reversible, while being easily composable. I will also show how these results can be extended to the setting of infinite words, which is the dedicated setting for model-checking for example. PhD defences Friday November 15, 2024, 10AM, Salle 279F, Halle aux farines Colin González (IRIF) From spreadsheets to functional programs: compilation and efficient execution of structured spreadsheets The development of applications with spreadsheets by non-professional programmers is a widespread practice both in industrial settings and in certain research fields. Owing to their simplicity and interactivity, spreadsheets count as a significant part of software development today. However, they can also be seen as poorly structured programs prone to committing programming errors. This thesis proposes a new perspective on spreadsheet development by adopting the principles of structured programming. Through the development of Lisa, a domain specific language, we propose the structured programming approach for spreadsheets. The main feature of this approach is to organise the sheets by columns rather than by cells. In this way, we can model the columns as potentially infinite streams of data. The unique aspect of this language is the introduction of indexed streams. In this context, the indexed nature of the streams capture the notion of the current row number of a given column’s cell. A relative access (relative to the current index) operation allows preserving a programming style akin to that of formulae found in traditional spreadsheets. The remainder of the thesis addresses the design and implementation of Lisa, a functional language focused on programming with indexed streams. In particular, we cover the compilation of Lisa into executables for various execution targets, ranging from traditional hardware platforms to the blockchain. Moreover, the programs issued by the compilation process depend on a runtime environment providing the relative access operator and indexed streams. The implementation of this operation is particularly slow for classical implementations of streams. To address these performance issues, we propose a new way of programming streams that is well suited to accelerating this key operation. Lisa is a fundamental component for the design of a specialised spreadsheet software tailored for the development of structured spreadsheets. In such a spreadsheet software, Lisa is used both to implement the formulae of a sheet and to develop extensions in the form of macro definitions. Finally, the compiled approach allows generating, from a structured sheet, an executable compatible with various software interfaces, thus enabling the modular composition of spreadsheet application developments, carried by end users, with highly technical software components developed by specialists. Verification Monday November 18, 2024, 11AM, Salle 3052 Romain Delpy (LaBRI, Univ. Bordeaux) An Automata-based Approach for Synchronizable Mailbox Communication We revisit finite-state communicating systems with round-based communication under mailbox semantics. Mailboxes correspond to one FIFO buffer per process (instead of one buffer per pair of processes in peer-to-peer systems). Round-based communication corresponds to sequences of rounds in which processes can first send messages, then only receive (and receives must be in the same round as their sends). A system is called synchronizable if every execution can be re-scheduled into an equivalent execution that is a sequence of rounds. We know from previous results that reachability is PSPACE-complete for synchronizable systems. In this talk we show that we can check if a mailbox system is synchronizable thanks to a novel automata-based approach. From this we get that checking synchronizability is PSPACE-complete. The same question is undecidable under peer-to-peer semantics. We also show that model-checking synchronizable systems for a natural subclass of regular properties is a PSPACE-complete problem. Joint work with Anca Muscholl & Grégoire Sutre. Programming Monday November 18, 2024, 10AM, 3071 Guillaume Baudart (IRIF) Natural Language Intermediate Representation for Mechanized Theorem Proving Formal theorem proving is challenging for humans as well as for machines. Thanks to recent advances in LLM capabilities, we believe natural language can serve as a universal interface for reasoning about formal proofs. In this talk, 1) we introduce Pétanque, a new lightweight environment to interact with the Coq theorem prover; 2) we present two interactive proof protocols leveraging natural language as an intermediate representation for designing proof steps; 3) we implement beam search over these interaction protocols, using natural language to rerank proof candidates; and 4) we use Pétanque to benchmark our search algorithms on different datasets. We will then discuss the limitations of our approach and possible future directions. Enumerative and analytic combinatorics Tuesday November 19, 2024, 11AM, Salle 3071 Clément Chenevière (LISN, Université Paris-Saclay) Une nouvelle description des treillis m-cambriens Les treillis cambriens, introduits par N. Reading en 2006, sont une généralisation du treillis de Tamari, à tout choix d'élément de Coxeter, dans tout groupe de Coxeter fini. Le treillis de Tamari correspond au “type A linéaire”. Ces ordres partiels admettent plusieurs descriptions, non trivialement équivalentes. Celles-ci donnent lieu à une généralisation commune, comme définie par C. Stump, H. Thomas et N. Williams. Toutefois, aucune de ces descriptions ne fournit de modèle combinatoire pratique. Dans un travail en cours avec Wenjie Fang et Corentin Henriet, nous proposons une nouvelle définition équivalente des treillis m-cambriens. Nous donnons un critère de comparaison simple et effectif sur des objets simples appelés m-partitions non croisées. Cette définition est obtenue en montrant qu'il existe une unique chaîne c-croissante entre n'importe quelle paire d'éléments comparables, et cette dernière est calculée par un algorithme glouton. Ce faisant, nous introduisons un ordre partiel intéressant sur les intervalles d'un treillis cambriens, qui est nouveau, même pour le cas du treillis de Tamari. Proofs, programs and systems Tuesday November 19, 2024, 3PM, TBA Pedro Amorim To be announced. Algorithms and complexity Tuesday November 19, 2024, 11AM, Salle 3052 Philip Verduyn Lunel (LIP6) Quantum Position Verification Protocols: Security and Practical Considerations In this talk we will give an overview of the area of position verification protocols. In position verification, the idea is to use an individual's geographical location as a cryptographic credential. In a position-verification protocol, the limitations imposed by the speed of light, as described by special relativity, are used to verify that a party is at their claimed location. This task has been shown to be impossible to implement using only classical information. Initially, the hope was that using quantum information we could construct secure quantum position verification (QPV) protocols. However, it has been shown that any QPV protocol can be broken by attackers that use an amount of entanglement exponential in the input size. Thus, unconditionally-secure quantum position-verification protocols do not exist. From a practical point of view, not all is lost. The exponential upper bound for a general attack is still astronomically large for only a relatively small input. Thus, we can still hope for practically secure QPV protocols. This raises the problem of designing protocols that are secure in a practical setting. In this talk we will present an overview of the field and present some proposed protocols and discuss their advantages and drawbacks. We will also discuss the best known entanglement bounds. Proofs, programs and systems Thursday November 21, 2024, 10:30AM, ENS Lyon Tba CHOCOLA seminar series Non-permanent members' seminar Thursday November 21, 2024, 4PM, Salle 3052 Manu Catz (PhD Student) Polygraphs and Oriented Shapes The most accessible way to visualize a (small) category is to consider its objects as vertices and its morphisms as oriented edges, forming some sort of graph. Polygraphs extend this intuition to form higher categories, where higher cells can be seen as oriented faces between edges, oriented solids between faces, &c. I will illustrate this construction with two families of categories, the oriented simplices and the oriented cubes, as well as showcase two operations that relate them when seen as constructed by a parametric language. References: Polygraphs: Dimitri Ara et al. Polygraphs: From Rewriting to Higher Categories. Orientals: Ross Street. “The algebra of oriented simplexes” ; Dimitri Ara, Yves Lafont, and François Métayer. Orientals as free algebras. Oriented Cubes: Iain R. Aitchison. The geometry of oriented cubes. Parametricity: Hugo Herbelin and Ramkumar Ramachandra. A parametricity-based formalization of semi-simplicial and semi- cubical sets. Automata Friday November 22, 2024, 2PM, Salle 3052 Pierre Letouzey (IRIF) Generalizing some Hofstadter functions: G, H and beyond Joint work with Shuo Li (U. Winnipeg) and Wolfgang Steiner (IRIF) Hofstadter's G function is recursively defined via $G(0)=0$ and then $G(n)=n-G(G(n-1))$. Following Hofstadter, a family $(F_k)$ of similar functions is obtained by varying the number $k$ of nested recursive calls in this equation. We present here a few nice properties of these functions. In particular, they can be described via some infinite morphic words generalizing the Fibonacci word. This was crucial for proving that this family is ordered pointwise: for all $k$ and $n$, $F_k(n) \le F_{k+1}(n)$. Moreover, these functions have a simple behavior on well-chosen numerical representations (Zeckendorf decompositions for some Fibonacci-like sequences). Thanks to that, we were also able to estimate the discrepancies for these $F_k$, i.e. the maximal distances between each $F_k$ and its linear equivalent. This whole work was formally proved using the Coq proof assistant (except for a beautiful fractal!) and we will give a gentle introduction to this Coq development.