We introduce judgemental theories and their calculi to frame type theory and proof theory in the same mathematical framework. Our analysis sheds light on both the topics, providing a new point of view. In the case of type theory, we provide an abstract definition of type constructor featuring the usual formation, introduction, elimination and computation rules. In proof theory we offer a deep analysis of structural rules, demystifying some of their properties, and putting them into context. We finish the paper discussing the internal logic of a topos, a predicative topos, an elementary 2-topos et similia, and show how these can be organized in judgemental theories.

The talk is based on a joint work with Greta Coraglia: https://arxiv.org/abs/2111.09438

Let $\mathcal{S}$ be a family of (not necessarily axis parallel) squares in the plane. The \emph{transversal number} of $\mathcal{S}$, denoted by $\tau(\mathcal{S})$, is the minimum number of points needed to hit all the squares in $\mathcal{S}$, and the \emph{independence number} of $\mathcal{S}$, denoted by $\nu(\mathcal{S})$, is the maximum number of pairwise disjoint squares in $\mathcal{S}$.

Clearly, $\tau(\mathcal{S})$ is at least $\nu(\mathcal{S})$. We prove that $\tau(\mathcal{S}) \leq 10 \nu(\mathcal{S})$ and present a family where $\tau(\mathcal{S}) = 3\nu(\mathcal{S})$.

During the talk, we will sketch the proof of the main result and remark how to extend our approach to families of rectangles with \emph{bounded aspect ratios}.

This is joint work with András Sebő.

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