Séminaire de l'équipe
Logique, Informatique et Mathématiques Discrètes


Organisateur: Sébastien Tavenas.

Lien ical.

Qi Qiu, Équipe CAPP, Laboratoire LIG, Université Grenoble Alpes. 2:00:00 22 mai 2025 10:00 TLR limd
TBA
Abstract

TBA

Elies Harington, Équipe Cosynus, laboratoire LIX, École Polytechnique. 2:00:00 24 avril 2025 10:00 TLR limd
TBA
Abstract

TBA

Robin Jourde, Equipe LIMD. 2:00:00 27 mars 2025 14:00 8B 228/30 limd
(Abstract) GSOS for trace equivalence
Abstract

Abstract GSOS is a categorical framework for operational semantics, in which rules are modeled as natural transformations of a certain type. Rule systems that fit the constraints imposed by the framework are guaranteed to have desirable properties, mainly that coalgebraic behavioural equivalence, which roughly corresponds to bisimilarity, is a congruence. While bisimilarity is central in process algebra, it is far from the only notion of process equivalence of interest. However, abstract GSOS is not easily applicable to these other equivalences. This work focuses on the other extremum of the linear time-branching time spectrum (bisimilarity being the finest), namely trace equivalence. We wonder under which assumptions on abstract GSOS laws this notion of equivalence is a congruence. A study of trace equivalence for a concrete instance of abstract GSOS (to labelled transition systems with explicit termination) identifies necessary and sufficient conditions to this end. We then transpose abstract GSOS to Kleisli semantics and investigate how, with conditions on the monad (affineness) and the GSOS law (dubbed linearity and smoothness) inspired by the concrete study, trace equivalence can be shown to be a congruence.

Yannick Zakowski, INRIA, LIP - ENS LYON. 2:00:00 20 mars 2025 10:30 TLR limd
Interprètes abstraits : Une approche monadique de leur vérification modulaire
Abstract

Dans cet exposé, je commencerai par mettre en contexte une série de travaux explorant dans un sens large une méthodologie basée sur des représentations «shallow» de calculs dans Rocq. Je me concentrerai ensuite plus spécifiquement sur un travail récent qui argue que de tels interprètes monadiques construits comme des couches d'interprétation empilées sur la monade libre constituent une manière prometteuse d'implémenter et de vérifier des interprètes abstraits.

L'approche permet des preuves modulaires de la correction des interprètes résultants. Nous fournissons des combinateurs génériques de contrôle de flôt abstraits dont la correction est prouvée une fois pour toute relativement à leur contrepartie concrète. Nous démontrons comment relier des gestionnaires concrets implémentant des effets à des variantes abstraites de ces gestionnaires, en capturant essentiellement la correction habituelle des fonctions de transfert dans le contexte des interprètes monadiques. Enfin, nous fournissons des résultats génériques pour transporter les résultats de correction par interprétation des effets d'état et d'échec.

Nous avons formalisé tous les combinateurs et théories susmentionnés dans Rocq, et démontré leurs avantages en implémentant et en prouvant la correction de deux interprètes abstraits illustratifs pour un langage impératif structuré et un assembleur jouet.

Cette contribution est un travail conjoint avec Sébastien Michelland et Laure Gonnord, et a fait l'objet d'un article à ICFP'24.

David Monniaux, CNRS - Laboratoire Verimag. 2:00:00 12 mars 2025 10:00 TLR limd
Adventures with formally verified Coq code and unverified OCaml code
Abstract

It is commonplace to split a complex, formally verified piece of software (e.g., CompCert) into a formally verified part (e.g. written in Coq/Rocq) and an unverified part (e.g., written in OCaml). There are many pitfalls when doing this (types of values exchanged, assumptions of purity, modeling of pointer equality…). We shall in particular discuss situations where the unverified part submits a result, together with an optional certificate, to a verified checker, and illustrate them with examples from the Verified Polyhedra Library and CompCert- Chamois .

Karim Nour, Equipe LIMD. 2:00:00 20 février 2025 09:30 TLR limd
Introduction au mu-calcul
Abstract

Le but de mon exposé est de vous présenter mon thème de recherche, qui était également celui de l'équipe de logique lors de sa création. L'objectif est d'étudier la relation entre les démonstrations mathématiques complètement formalisées et la programmation à l'aide d'un langage fonctionnel très basique.

Plusieurs questions nous intéressent dans ce domaine :

  • Comment programmer correctement des fonctions sur des types de données ?
  • Comment extraire le contenu algorithmique des preuves mathématiques ?
  • Quelles sont les propriétés de cette relation entre preuves et programmes ?

L'exposé sera en français, avec des diapositives en anglais, et ne nécessitera pas de connaissances avancées dans ce domaine.

Srijani Mukherjee, équipe LIMD. 2:00:00 13 février 2025 10:00 TLR limd
Graph-Oriented Information Fusion for Solar PV Performance Analysis
Abstract

Solar photovoltaic (PV) systems are complex, dynamic systems influenced by a wide range of environmental and operational factors. Accurately modelling their performance and detecting anomalies require integrating diverse data sources and capturing intricate dependencies. In this talk will present a graph-oriented information fusion framework designed to enhance solar PV performance analysis. The framework begins with the analysis of temperature and irradiance data using graph-based techniques, which are then extended to incorporate additional PV parameters such as module temperature, ambient air temperature, global shortwave and longwave radiation, and power output. By constructing temporal graphs, the framework captures both spatial and temporal dependencies, enabling a holistic understanding of system behaviour under varying conditions. This talk will explain the development of a Temporal Graph Neural Network (TGN) model that leverages these fused data sources for performance prediction and anomaly detection. The TGN model integrates Graph Convolutional Networks (GCNs) and Gated Recurrent Units (GRUs) to simultaneously model spatial and temporal dependencies, offering a robust approach to analyse complex PV system dynamics. The talk will highlight the mathematical foundations of the framework, including network analysis, information fusion, and deep learning, and demonstrate its practical applications in solar PV diagnostics. By combining diverse data sources and advanced graph-based techniques, this framework provides a powerful tool for improving the reliability and efficiency of solar energy systems.

Jules Armand, LIMD. 2:00:00 30 janvier 2025 10:00 TLR limd
Reconstruction des circuits arithmétiques génériques de profondeur constante.
Abstract

Les circuits arithmétiques sont un modèle de calcul des polynômes multivariés sur un corps $\mathbb{K}$. Des problèmes classiques difficiles sur les circuits sont notamment les questions de calcul de bornes inférieures (quelle est la taille minimale d'un circuit calculant un certain polynôme), de test d'identité (donné un circuit, quelle est la complexité de tester si ce circuit calcule le polynôme identiquement nul) ou de reconstruction (Étant donné un accès oracle à un polynôme $f$ calculé par un certain circuit $C$, peut-on reconstruire un circuit similaire $C'$ calculant $f$). On se penchera sur le dernier problème. La question de la reconstruction est ouverte dans le cas général mais il existe des méthodes de reconstruction pour certaines classes de circuits et notamment pour des sous-familles de profondeur constante.

Etienne Moutot, CR CNRS - équipe GDAC à l'I2M, Aix-Marseille. 2:00:00 23 janvier 2025 10:00 TLR limd
Compter des couplages parfait en réécrivant des graphes
Abstract

Les langages graphiques sont des formalismes de plus en plus utilisés dans le contexte de l'informatique quantique. Ils permettent de faire des calculs sans utiliser d'équations, uniquement par des opérations de réécriture de diagrammes. Dans cet exposés, je commencerai par une petite introduction douce au ZW-calcul, inventé en 2010 par Coecke and Kissinger. Je montrerai que ce langage graphique peut être utilisé pour traiter des problème complètement combinatoires (et "classiques"), comme le comptage de couplages parfaits dans des graphes. En utilisant ce formalisme, nous sommes parvenus (avec Titouan Carette, Thomas Perez et Renaud Vilmart) à une nouvelle technique permettant de compter les couplages parfaits d'un graphe planaire en un nombre polynomial d'opérations (un résultat dû à Kasteleyn en 1967 en utilisant la notion d'orientations Pfaffiennes).

Antoine Dailly, INRAE. 2:00:00 16 janvier 2025 10:00 TLR limd
Un canadien voyage sur un graphe planaire extérieur...
Abstract

Le Voyageur Canadien essaye, dans un graphe pondéré donné, d'aller d'un sommet à un autre. Mais certaines arêtes sont bloquées ; il les découvre en visitant une de leurs extrémités. Une façon d'évaluer la stratégie du voyageur est de chercher à minimiser le ratio entre la distance parcourue et celle qui l'aurait été avec l'information parfaite : c'est le ratio compétitif. Il est connu qu'aucune stratégie ne peut avoir de ratio compétitif meilleur que 2k+1 (où k est le nombre d'arêtes bloquées), même dans les graphes planaires non-pondérés de largeur arborescente 2.

Nous étudions le cas des graphes planaires extérieurs, où nous déterminons une stratégie ayant ratio compétitif 9 dans le cas non-pondéré (ce qui implique un ratio constant lorsque l'écart entre les pondérations est borné). Nous montrons aussi que cette valeur de 9 est une borne inférieure : il existe une famille sur laquelle aucune stratégie ne peut avoir de ratio compétitif 9-epsilon. Enfin, nous montrons que le ratio compétitif ne peut pas être borné dans les graphes planaires extérieurs arbitrairement pondérés.

Loïc Pujet, University of Stockholm, Department of mathematics. 2:00:00 5 décembre 2024 10:00 TLR limd
"Si ça marche, chante et vole comme un Coq, alors c'est un Coq" ~ Étendre Coq avec le Pouvoir de l'Observation
Abstract

La théorie des types observationnelle (OTT) est une extension de la théorie des types dépendants conçue par Altenkirch et McBride dans les années 2000. L'idée centrale d'OTT est qu'en modifiant le concept d'égalité, il devient possible d'avoir des types quotients et des fonctions extensionnelles sans compromettre le caractère constructif de la théorie des types dépendants.

Lors de cet exposé, j'expliquerai comment combiner la théorie observationnelle d'Altenkirch et McBride avec le Calcul des Constructions, la théorie des types qui sous-tend l'assistant à la preuve Coq. En particulier, j'expliquerai comment caractériser l'égalité des types inductifs de Coq, et comment les éliminateurs des types indexés utilisent une règle de calcul délicate à intégrer à la théorie.

Si le temps le permet, j'en profiterai pour faire une démonstration de la branche expérimentale Coq-observationnel, et pour discuter d'avancées récentes dans la sémantique ensembliste de la théorie des types observationnelle.

Yannick Mogge, Hamburg University of Technology. 2:00:00 14 novembre 2024 10:00 TLR limd
Speed and size of dominating sets in domination games
Abstract

We consider Maker-Breaker domination games, a variety of positional games, in which two players (Dominator and Staller) alternately claim vertices of a given graph. Dominator's goal is to fully claim all vertices of a dominating set, while Staller tries to prevent Dominator from doing so, or at least tries to delay Dominator's win for as long as possible.

We prove a variety of results about domination games, including the number of turns Dominator needs to win and the size of a smallest dominating set that Dominator can occupy. We could also show that speed and size can be far apart, and we prove further non-intuitive statements about the general behaviour of such games.

We also consider the Waiter-Client version of such games.

Co-authors (all from Hamburg University of Technology as well): Ali Deniz Bagdas, Dennis Clemens, Fabian Hamann

Kenji Maillard, INRIA Rennes. 2:00:00 7 novembre 2024 10:00 TLR limd
Martin-Löf à la Coq et autres contes de théorie des types formalisées
Abstract

La théorie des types dépendants sert de fondations à une famille d'assistants à la preuve dont Agda, Coq et Lean sont trois représentants modernes. La correction de ces implémentations reposent sur des propriétés métathéoriques des systèmes de types dépendants telle que l'existence de formes canonique, la décidabilité de la conversion ou du typage, dont les preuves sont notoirement complexes. Dans cette présentation, j'expliquerai les difficultés qui se présentent pour méchaniser de telles preuves de propriété métathéorique ainsi que les solutions retenues pour établir formellement des résultats de normalisation et de décidabilité de la théorie des types de Martin-Löf dans l'assistant de preuves Coq. J'esquisserai comment ce projet donne aussi l'opportunité de développer des extensions expressives des assistants à la preuve tout en préservant des fondations solides.

Alan Schmitt, INRIA, Research Center Rennes. 2:00:00 10 octobre 2024 10:00 TLR limd
Effects in Skel From Exceptions to Delimited Computation
Abstract

Skeletal Semantics is a meta-language to describe the semantics of programming languages. We present it through several examples, highlighting how complex features can be captured in a readable way using monads. These features range from simple effects like exceptions to more complex ones like generators.

Laurent Feuilloley, LIRIS, Université Lyon 1. 2:00:00 26 septembre 2024 10:00 TLR limd
Introduction to local certification
Abstract

In this talk I will introduce local certification, a notion originating from distributed computing that sheds a new light on the structure of graphs. After giving intuitions about the notion, I will review the recent developments, and make connections with other areas of theoretical computer science (including complexity and logic).

Enzo Mauti, . 2:00:00 12 juillet 2024 10:00 TLR limd
Utilisation of flows in graphs for Image Segmentation: Min Cut Max Flow
Abstract

L'exposé portera sur les calculs de flows maximaux dans les graphes avec l'algorithme de Ford-Fulkerson, puis de l'utilisation de ces flows pour la segmentation d'image. Je parlerais aussi des différentes implémentations de ces algorithmes pour améliorer leur efficacité ou modifier leur comportement par rapport aux images choisies. Je terminerai par quelques exemples concrets de certaines implémentations que j'aurais pu essayer et conclurais.

Grégory Chichery, LIS, Aix-Marseille Université. 2:00:00 20 juin 2024 10:00 TLR limd
Lifting final coalgebras and initial algebras, a reconstruction
Abstract

Many categorical models of linear logic with fixed points arise as total categories over the category Rel of sets and relations. They are form ∫Q, the Grothendieck category for a functor Q : Rel -> Pos. We will define the concepts of fixed points and Grothendieck category and then we give a result to lift functor from the base category to the total category and studies also how to lift fixed points. In particular, the category of coalgebras for the lifted functor is a total category, and when Q factors through SLatt, the category of posets with joins and maps that preserve them, we found the same result.

Kave Salamatian, LISTIC, Université Savoie Mont Blanc. 2:00:00 13 juin 2024 10:00 TLR limd
Ironing the Graphs: Toward a Correct Geometric Analysis of Large-Scale Graphs
Abstract

Graph embedding approaches attempt to project graphs into geometric entities, {\em i.e.}, manifolds. At its core, the idea is that the geometric properties of the projected manifolds are helpful in the inference of graph properties. However, the choice of the embedding manifold is critical and, if incorrectly performed, can lead to misleading interpretations due to incorrect geometric inference. We argue that the classical embedding techniques cannot lead to correct geometric interpretation as the microscopic details, {\em e.g.}, curvature at each point, of manifold, that are needed to derive geometric properties in Riemannian geometry methods are not available, and we cannot evaluate the impact of the underlying space on geometric properties of shapes that lie on them. We advocate that for doing correct geometric interpretation the embedding of a graph should be done over regular constant curvature manifolds. To this end, we present an embedding approach, the discrete Ricci flow graph embedding (dRfge) based on the discrete Ricci flow that adapts the distance between nodes in a graph so that the graph can be embedded onto a constant curvature manifold that is homogeneous and isotropic, {\em i.e.}, all directions are equivalent and distances comparable, resulting in correct geometric interpretations. A major contribution of this paper is that for the first time, we prove the convergence of discrete Ricci flow to a constant curvature and stable distance metric over the edges. A drawback of using the discrete Ricci flow is the high computational complexity that prevented its usage in large-scale graph analysis. Another contribution of our work is a new algorithmic solution that makes it feasible to calculate the Ricci flow for graphs of up to 50k nodes, and beyond. The intuitions behind the discrete Ricci flow make it possible to obtain new insights into the structure of large-scale graphs.

Krzysztof Worytkiewicz, LAMA. 2:00:00 30 mai 2024 10:00 TLR limd
Implicative Assemblies
Abstract

Implicative algebras, recently discovered by Miquel, are combinatorial structures unifying classical and intuitionistic realizability as well as forcing. In this talk we introduce implicative assemblies as sets valued in the separator of an underlying implicative algebra. Given a fixed implicative algebra A, implicative assemblies over A organise themselves in a category AsmA with tracked set-theoretical functions as morphisms. We show that AsmA is a quasitopos with a natural numbers object (NNO).

Pierre-Étienne Meunier, . 2:00:00 16 mai 2024 10:00 8B-232 limd
Projet Pijul, un système de contrôle de versions
Abstract

Comment un résultat de catégories a inspiré une solution aux problèmes de performance de Darcs. Darcs est un système de contrôle de versions sorti en 2005, basé sur des patchs, ce qui le rendait extrêmement simple à utiliser et particulièrement rigoureux, en particulier dans sa gestion des conflits. Seul problème, il prenait parfois un temps exponentiel en la taille de l'histoire pour son opération la plus courante (appliquer des patchs). Je vous expliquerai comment nous avons résolu le problème, en utilisant des catégories et des structures de données purement fonctionnelles, pour concevoir un algo en temps logarithmique pour tous les cas (sauf un cas dégénéré en temps linéaire).

Le résultat est un système déterministe (ce qui le distingue de tous les autres outils de contrôle de versions), facile à apprendre et à utiliser, tout en passant à des échelles qu'aucun autre système de contrôle de versions distribué ne peut atteindre.