TBA
Polynomial diagrams (also known as containers) are a categorification of the notion of polynomial. They can be defined in any category with pullbacks, where they form a bicategory. In the setting of homotopy type theory, we show that the (wild) category of polynomial diagrams in types can be recovered as a Kleisli category over the category of spans of types, thus fitting spans and polynomials respectively as the linear and non-linear part of a homotopical model of Linear Logic. If time allows, I will talk about how this fits in a framework of infinity-categorical models of Linear Logic that we are currently developing.
Proof complexity aims to analyse the power of formal proof systems. Specifically, it is the study of the resources required to certify the truth of mathematical statements. It plays a crucial role in computational complexity and it has close connections to circuit complexity, automated reasoning, and mathematical logic.
A key direction in proof complexity is algebraic proof complexity, which analyses proof systems that use algebraic representations of logical formulas. These systems provide insight into the power and limitations of algebraic methods in proof complexity. Among them, the Ideal Proof System (IPS), introduced by Grochow and Pitassi, is the focus of this talk. IPS represents proofs as algebraic circuits verifying the unsatisfiability of polynomial equations.
In this talk, we will explore the IPS proof system, its connections to algebraic complexity, and recent developments in its study. We will discuss lower bounds for IPS, structural properties of algebraic proofs, and their implications for classical proof complexity questions. Finally, we will highlight open problems and future directions in the field.
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.
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.
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 .
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 :
L'exposé sera en français, avec des diapositives en anglais, et ne nécessitera pas de connaissances avancées dans ce domaine.
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.
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.
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).
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.
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.
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
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.
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.
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).
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.
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.
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.
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).