Les cartes bicolorées à bord apparaissent dans de nombreux contextes : elles sont notamment un cas particulier du modèle d'Ising. Ainsi, dans le cas d'un bord monochromatique, très naturel pour le modèle d'Ising, les cartes bicolorées ont été énumérées par plusieurs méthodes, tant analytiques que bijectives. Cependant, pour l'étude de modèles de cartes aléatoires, il est plus naturel de considérer d'autres conditions de bord, comme la condition dite alternante. Dans cet exposé, je présenterai les résultats et les principaux arguments d'un travail en commun avec Jérémie Bouttier, où nous utilisons des outils de combinatoire analytique pour énumérer les cartes bicolorées à bord alternant. Les résultats intermédiaires que je présenterai feront aussi apparaître d'autres motivations pour s'intéresser à ces conditions de bord.

Necula (PLDI'2000) and Tristan, Gouvereau, Morrisett (PLDI'2011) established that symbolic execution combined with rewriting is effective in validating the code produced by state-of-the-art compilers applying various optimizations. In the meantime, Tristan and Leroy (POPL'2008) used formally-verified symbolic execution to certify the schedules produced by untrusted oracles – optimizing pipeline usage – within the CompCert compiler. Alas, their formally-verified checker had exponential complexity and was thus never integrated into mainline CompCert.

With Cyril Six and David Monniaux, we solved this performance issue with formally verified hash-consing within the symbolic execution. And we successfully applied this technique to implement within CompCert effective optimizations targeting superscalar (or VLIW) in-order processors.

The talk will actually start by briefly introducing a sound Foreign Function Interface for embedding OCaml oracles within Coq. Hence, it will explain how we used it in this application.

IRIF Cake^TM is an amazing opportunity to meet people while simultaneously eating cakes baked by your fellow colleagues! Join us every Thursday, at 5pm, in front of room 3052 (Sophie Germain 3rd floor) for a weekly feast. You can also express your cooking skills and volunteer to bake a cake by sending an email to cake@irif.fr.

La diagonale ensembliste d’un polytope a le défaut rédhibitoire de ne pas être cellulaire: son image n’est pas une union de cellules. Notre but sera ici de développer une théorie générale, basée sur la méthode introduite par N. Masuda, H. Thomas, A. Tonks et B. Vallette, afin de comprendre et de manipuler les approximations cellulaires de la diagonale d’un polytope quelconque. Cette théorie nous permettra d’attaquer le problème de l’approximation cellulaire de la diagonale des opéraèdres, une famille de polytopes allant des associaèdres aux permutoèdres, et qui code les opérades à homotopie près. Nous obtiendrons ainsi une formule explicite pour le produit tensoriel de deux telles opérades, aux propriétés combinatoires intéressantes.

Référence: https://arxiv.org/abs/2110.14062

Regular languages can be actively learned with membership and equivalence queries in polynomial time. The learning algorithm, called the L^* algorithm, constructs iteratively the right congruence relation of a given regular language L, and returns the minimal DFA recognizing L. The L^* algorithm has been adapted to various types of automata: tree automata, weighted automata, nominal automata. However, an extension to infinite-word automata has been elusive. In this talk, I will present an extension of the active learning framework, in which the algorithm can ask syntactic queries about the automaton representing a given infinite-word language.

First, I will discuss why extending L^*, which asks only semantic queries, to infinite-words languages is difficult. Next, I will present an alternative approach; instead of learning some automaton for a hidden language, we assume that there is a hidden automaton and the algorithm is supposed to learn an equivalent automaton. In this approach, the learning algorithm is allowed to ask standard semantic queries (membership and equivalence) and loop-index queries regarding the structure of the hidden automaton. These queries do not reveal the full structure of the automaton and hence do not trivialize the learning task.

In the extended framework, there are polynomial-time learning algorithms for various types of infinite-word automata: deterministic Buechi automata, LimSup-automata, deterministic parity automata and limit-average automata.

Finally, the idea to incorporate syntactic queries can be adapted to the pushdown framework; I will briefly discuss the learning algorithm for deterministic visibly pushdown automata.

Software systems and the artifacts they consist of often exist in many different variants. When creating new variants, developers typically rely on the “clone and own” strategy of copying and modifying existing variants, a simple and intuitive approach with significant long-term disadvantages. In this talk, I present a line of work on supporting variants in software engineering by explicitly addressing variability as a feature in graph transformations. I focus on three transformation scenarios: one where the input graph has variability (representing the established notion of a software product line), one where rules have variability (leading to variability-based rules), and a combination of the first two scenarios. Each scenario is supported with formal constructions, efficient transformation algorithms, and tool support. Our work shows that a systematic way of supporting variability in transformations can improve the maintainability and the performance of a software system.

Zoom meeting registration link

YouTube live stream

We discuss the issue of deciding the first-order theory of integer linear arithmetic, also known as Presburger arithmetic. Whereas optimal decision procedures based on either quantifier-elimination or automata constructions are known for this theory, the current procedures based on manipulating semilinear sets (i.e. sets that geometrically characterise the solutions of a formula) are extremely inefficient. We address this issue by deriving a new algorithm for computing the complement of a semilinear set, which in particular is optimal for nested complementations. Alongside solving the aforementioned discrepancy between semilinear-based algorithms and other types of procedures, this result allows us to characterise the Vapnik-Chervonenkis dimension of Presburger arithmetic, which is found to be doubly-exponential. The results in this talk are joint work with Christoph Haase and Dmitry Chistikov.

The problem of generalizing the notion of polynomial time to a type-two setting, where inputs include not only finitary data, e.g., numbers or strings of symbols, but also functions on such data, was first posed by Constable in 1973. Mehlhorn subsequently proposed a solution, based on a generalization Cobham's scheme-based approach which uses limited recursion on notation. The resulting class was shown to be robust with respect to oracle Turing machine (OTM) computation, but the problem of providing a purely machine-based characterization remained open for almost two decades, when Kapron and Cook gave a solution using notions of function length and second-order polynomials. While a natural generalization of the usual notion of poly-time, this characterization still had some shortcomings, as function length is itself not a feasible notion. A charaterization using ordinary polynomials remained an elusive goal.

Recently, we have provided several such characterizations. The underlying idea is to bound run time in terms of an ordinary polynomial in the largest answer returned by an oracle, while imposing a constant upper bound on the number of times an oracle query (answer) may exceed all previous ones in size. The resulting classes are contained in Mehlhorn's class, and when closed under composition are in fact equivalent.

In this talk we will present these recent results and follow-up work involving new scheme-based characterizations of Mehlhorn's class, as well as a recent characterization using a tier-based type system for a simple imperative programming language with oracle calls.

(Joint work with F. Steinberg, and with E. Hainry, J.-Y. Marion, and R. Pechoux.)

In this talk we present some basic notions of convexity, from a quantum-algorithmic point of view. The talk will consist of two parts. We first warm-up by introducing some classical first- and second-order methods for convex optimization. Then, we move on to more structured convex problems, introduce linear programming and the basic ideas of interior-point methods. We mention some quantum algorithms for LPs and SDPs. In the second part of the talk we discuss sampling, and in particular its applications to estimating volumes of polytopes. We present the basic classical sampling algorithms (ball walk and hit-and-run), and the general framework for applying these algorithms to volume estimation. We conclude by discussing the opportunities for quantum speedups - in particular, we present a high-level overview of the work by Chakrabarti, Childs, Hung, Li, Wang and Wu from 2019.

We study a family of distributors-induced bicategorical models of lambda-calculus, proving that they can be syntactically presented via intersection type systems. We first introduce a class of 2-monads whose algebras are monoidal categories modelling resource management. We lift these monads to distributors and define a parametric Kleisli bicategory, giving a sufficient condition for its cartesian closure. In this framework we define a proof-relevant semantics: the interpretation of a term associates to it the set of its typing derivations in appropriate systems. We prove that our model characterize solvability, adapting reducibility techniques to our setting. We conclude by describing two examples of our construction.

IRIF Cake^TM is an amazing opportunity to meet people while simultaneously eating cakes baked by your fellow colleagues! Join us every Thursday, at 5pm, in front of room 3052 (Sophie Germain 3rd floor) for a weekly feast. You can also express your cooking skills and volunteer to bake a cake by sending an email to cake@irif.fr.