Logic, Computer Science, and Discrete Mathematics

Organiser: Sébastien Tavenas.

Yannick Mogge, *Hamburg University of Technology*.
Nov. 14, 2024, 10 a.m.
TLR
limd
**TBA**
## Abstract

TBA

Kenji Maillard, *INRIA Rennes*.
Nov. 7, 2024, 10 a.m.
TLR
limd
**TBA**
## Abstract

TBA

Alan Schmitt, *INRIA, Research Center Rennes*.
Oct. 10, 2024, 10 a.m.
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*.
Sept. 26, 2024, 10 a.m.
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, .
July 12, 2024, 10 a.m.
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é*.
June 20, 2024, 10 a.m.
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*.
June 13, 2024, 10 a.m.
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*.
May 30, 2024, 10 a.m.
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, .
May 16, 2024, 10 a.m.
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.

Colin Weill-Duflos, *LAMA*.
March 21, 2024, 10 a.m.
TLR
limd
**Digital Calculus Frameworks and Comparative Evaluation of their Laplace-Beltrami operators**
## Abstract

In a first part I'll will broadly cover the topic of what the Laplace- Beltrami is, its different characterization and its many uses in computer graphics.

Then I'll cover our works on the topic of building this operator (along with a wider digital calculus framework) on digital surfaces (boundary of voxels). These surfaces cannot benefit directly from the classical mesh calculus frameworks. In our recent work, we propose two new calculus frameworks dedicated to digital surfaces, which exploit a corrected normal field. First we build a corrected interpolated calculus by defining inner products with position and normal interpolation in the Grassmannian. Second we present a corrected finite element method which adapts the standard Finite Element Method with a corrected metric per element. Experiments show that these digital calculus frameworks seem to converge toward the continuous calculus, offer a valid alternative to classical mesh calculus, and induce effective tools for digital surface processing tasks.

Adrienne Lancelot, *IRIF, Université de Paris*.
March 7, 2024, 10 a.m.
TLR
limd
**Normal Form Bisimulations by Value**
## Abstract

Normal form bisimilarities are a natural form of program equivalence resting on open terms, first introduced by Sangiorgi in call-by-name. The literature contains a normal form bisimilarity for Plotkin’s call-by-value 𝜆-calculus, Lassen’s enf bisimilarity, which validates all of Moggi’s monadic laws and can be extended to validate 𝜂. It does not validate, however, other relevant principles, such as the identification of meaningless terms—validated instead by Sangiorgi’s bisimilarity—or the commutation of lets. These shortcomings are due to issues with open terms of Plotkin’s calculus. We introduce a new call-by-value normal form bisimilarity, deemed net bisimilarity, closer in spirit to Sangiorgi’s and satisfying the additional principles. We develop it on top of an existing formalism designed for dealing with open terms in call-by-value. It turns out that enf and net bisimilarities are incomparable, as net bisimilarity does not validate Moggi’s laws nor 𝜂. Moreover, there is no easy way to merge them. To better understand the situation, we provide an analysis of the rich range of possible call-by-value normal form bisimilarities, relating them to Ehrhard’s relational model.

Lê Thành Dũng Nguyễn, *LIP, ENS Lyon*.
Feb. 22, 2024, 10 a.m.
TLR
limd
**Implicit automata in typed λ-calculi I: aperiodicity in a non-commutative logic**
## Abstract

We give a characterization of star-free languages (a well-known subclass of regular languages) in a λ-calculus with support for non-commutative affine types (in the sense of linear logic), via the algebraic characterization of the former using aperiodic monoids. This was the first result in a research program that Cécilia Pradic (Swansea University) and I have carried out since my PhD, on which I will say a few words.

Tom Hirschowitz, .
Feb. 15, 2024, 10 a.m.
8D-104 Iseran
limd
**A semantic notion of inference rule for (dependent, quantitative) type theory**
## Abstract

Type theory is a family of formal systems ranging from programming language semantics to the foundations of mathematics. In practice, type theories are defined by means of “inference rules”. Everyone in the community understands them to some extent, but they do not have any commonly accepted rigorous interpretation. Or, rather, they have several interpretations, none of which is entirely satisfactory.

In this work, after a brief overview of the literature, we introduce a rigorous, semantic notion of inference rule, our thesis being that most syntactic inference rules written in practice may be directly interpreted in this framework. If time permits, we will sketch how this covers quantitative type theories.

This is joint work in progress with André Hirschowitz and Ambroise Lafont.

Jacques-Olivier Lachaud, *LAMA, Chambéry*.
Feb. 8, 2024, 10 a.m.
TLR
limd

Michela Ascolese, *University of Florence*.
Jan. 18, 2024, 11 a.m.
TLR
limd
**Polytime algorithms for the reconstruction of 3-uniform hypergraphs**
## Abstract

I describe a P-time heuristic to reconstruct a subclass of degree sequences of 3-uniform hypergraphs. The heuristic bases on some geometrical properties of the involved hypergraphs and also produces a small set of ambiguous hyperedges that has to be individually considered.

Andrea Frosini, *University of Florence*.
Jan. 18, 2024, 10 a.m.
TLR
limd
**On the reconstruction of 3-uniform hypergraphs from unique degree sequences**
## Abstract

We consider the problem of detecting and reconstructing degree sequences of 3-uniform hypergraphs. The problem is known to be NP-hard, so some subclasses are inspected in order to detect instances that admit a P-time reconstruction algorithm. Here, I consider instances having specific numerical patterns and I show how to easily reconstruct them.

Nacim Oijid, *LIRIS , Université Lyon 1*.
Jan. 11, 2024, 10 a.m.
TLR
limd
**Complexity of Maker-Breaker Games on edge sets of graphs**
## Abstract

We initiate the study of the algorithmic complexity of Maker-Breaker games played on edge sets of graphs for general graphs. We mainly consider three of the big four such games: the connectivity game, perfect matching game, and H-game. Maker wins if she claims the edges of a spanning tree in the first, a perfect matching in the second, and a copy of a fixed graph H in the third. We prove that deciding who wins the perfect matching game and the H-game is PSPACE-complete, even for the latter in graphs of small diameter if H is a tree. Seeking to find the smallest graph H such that the H-game is PSPACE-complete, we also prove that there exists such an H of order 51.

On the positive side, we show that the connectivity game and arboricity-k game are polynomial-time solvable. We then give several positive results for the H-game, first giving a structural characterization for Breaker to win the P4-game, which gives a linear-time algorithm for the P4-game. We provide a structural characterization for Maker to win the K_{1,l}-game in trees, which implies a linear-time algorithm for the K_{1,l}-game in trees. Lastly, we prove that the K_{1,l}-game in any graph, and the H-game in trees are both FPT parameterized by the length of the game. We leave the complexity of the last of the big four games, the Hamiltonicity game, as an open question.

Clément Blaudeau, *Cambium team, Inria Paris*.
Dec. 7, 2023, 10:15 a.m.
TLR
limd
**Retrofitting OCaml modules, an Fω-inspired approach for a modern module system**
## Abstract

ML modules offer large-scale notions of composition and modularity. Provided as an additional layer on top of the core language, they have proven both vital to the working OCaml and SML programmers, and inspiring to other use-cases and languages. Unfortunately, their meta-theory remains difficult to comprehend, and more recent extensions (abstract signatures, module aliases) lack a complete formalization. Building on a previous translation from ML modules to Fω, we propose a new comprehensive description of a significant subset of OCaml modules, including both applicative and generative functors and transparent ascription -- a useful new feature. By exploring the translations both to and from Fω, we provide a complete description of the signature avoidance issue, as well as insights on the limitations and benefits of the path-based approach of OCaml type-sharing.

Greta Coraglia, *LUCI Lab, University of Milan*.
Nov. 30, 2023, 10 a.m.
TLR
limd
**Categorical models of subtyping**
## Abstract

We start from categorical semantics of dependent types and propose structural rules involving a new notion of subtyping. We begin by recalling a few classical models, which traditionally have been heavily set-based: this is the case for categories with families, categories with attributes, and natural models. In particular, all of them can be traced back to certain discrete fibrations. We extend this intuition to the case of general, non necessarily discrete, fibrations, and use the newly found structure on the fibers to interpret a form of subtyping. Interestingly, the emerging notion turns out to be closely related to that of coercive subtyping. This is joint work with J. Emmenegger.

Peio Borthelle, .
Nov. 23, 2023, 10 a.m.
TLR
limd
**Operational game semantics, certified in Coq**
## Abstract

Une sémantique des jeux opérationelle certifiée en Coq

La sémantique des jeux opérationelle (OGS) est une méthode pour transformer l'évaluateur d'un langage de programmation en une sémantique correcte vis-à-vis de l'équivalence contextuelle, basée sur l'interprétation des termes ouvert comme des "stratégies" pour interagir avec n'importe quel environnement d'exécution. Avec mes encadrants de thèse j'ai développé une formalisation en Coq de cette construction en s'abstrayant légèrement des détails syntaxiques du langage considéré. Je vais commencer par motiver et présenter le fonctionnement intuitif des OGS, puis donner un aperçu de nos contributions. Et enfin pour les plus courageux détailler un point technique de la preuve de correction: la propriété "d'avancement" de la composition d'une stratégie active avec une stratégie passive.

Operational game semantics, certified in Coq

Operational game semantics (OGS) is a method to transform an evaluator for a programming language into a semantic space which is correct with respect to contextual equivalence. It is based on interpreting open terms as "strategies" to interact with any execution environment. With my doctoral advisors I have developped a Coq formalization of this construction, abstracting away some syntactic details of the considered language. I will start this talk by motivating and presenting OGS intuitively, and will then give a high level view of our contributions. Finally for the bravest I will detail a technical point of the correction proof, namely the "progress" property of the composition of an active strategy with a passive strategy.