Mars 2018 — Géométrie et Topologie du Calcul

« Homologie algorithmique pour les objets discrets » par A. Gonzales-Lorenzo (LIRIS)
« Topological and algorithmic tools for computability in distributed computing » par D. Imbs (LIS)
« Un contre-exemple à la conjecture de Thiagarajan sur les structures d’évènements régulières » par J. Chalopin (LIS)

Orateur : Aldo Gonzales-Lorenzo (post-doc LIRIS)
Titre : Homologie algorithmique pour les objets discrets

Résumé : La théorie de l’homologie formalise la notion de trou dans un espace. Pour un sous-ensemble de l’espace Euclidien, on définit une séquence de groupes d’homologie, dont leurs rangs sont interprétés comme le nombre de trous de chaque dimension. Ainsi, β0 (le rang du groupe d’homologie de dimension zéro) est le nombre de composantes connexes, β1 est le nombre de tunnels ou anses et β2 est le nombre de cavités. Ces groupes sont calculables quand l’espace est décrit d’une façon combinatoire, comme c’est le cas pour les complexes simpliciaux ou cubiques. À partir d’un objet discret (un ensemble de pixels, voxels ou leur analogue en dimension supérieure) nous pouvons construire un complexe cubique et donc calculer ses groupes d’homologie.

Dans cette présentation je parlerai de deux approches relatives au calcul de l’homologie sur des objets discrets. Primo, je présenterai le champ de vecteurs discret homologique, une structure combinatoire qui permet de calculer les groupes d’homologie. Secundo, je présenterai deux mesures (l’épaisseur et la largeur) associées aux trous d’un objet discret, ce qui permet d’obtenir une signature topologique et géométrique plus intéressante que les simples nombres de Betti.


Orateur : Damien Imbs (LIS AMU, new MCF)
Titre : Topological and algorithmic tools for computability in distributed computing

Résumé : One of the major breakthroughs in distributed computing was the discovery of its links with algebraic topology. This result earned its authors the Gödel prize in 2004. Topological tools are especially useful to prove impossibility results.

In this talk, I will present such topological tools and how to use them to prove the impossibility of distributed problems. In particular, I will show how to use Sperner’s Lemma to prove the impossibility of Set Agreement, a fundamental distributed problem, in a specific model. I will then present algorithmic techniques to extend this result to various distributed models of computation.


Orateur : Jeremie Chalopin (LIS AMU)
Titre : Un contre-exemple à la conjecture de Thiagarajan sur les structures d’évènements régulières
Résumé : On présente un contre-exemple à la conjecture de Thiagarajan (1996 et 2002) affirmant que les structures d’évènements régulières correspondent exactement à celles obtenues comme dépliages des réseaux de Petri 1-safe finis. Les structures d’évènements, les automates de trace sont des modèles fondamentaux pour la théorie de la concurrence. Il existe des interprétations élégantes de ces structures comme des objets combinatoires et géométriques, et on peut reformuler la conjecture dans ce cadre. Plus précisément, les domaines des structures d’évènements correspondent exactement aux graphes médians pointés et aux complexes cubiques CAT(0) pointés. Une condition nécessaire pour que la conjecture de Thiagarajan soit vérifiée est que les domaines des structures d’évènements régulières admettent un joli étiquetage régulier (regular nice labelling). Pour réfuter cette conjecture, on décrit le domaine d’une structure d’évènement régulière qui n’admet pas de tel étiquetage. Notre contre-exemple est basé sur une construction de Wise (1996 et 2007) d’un complexe de carrés de courbure non-positive dont le revêtement universel est un complexe de carrés CAT(0) contenant un plan muni d’un pavage apériodique.

Février 2018 — Logique et Méthodes Formelles

« When type theory meets model-checking » par C. Grellois (LIS)
« Programs as formulas » par M. Cristia (U. N. Rosario)
« On The Complexity of Resource-Bounded Logics » par S. Demri (LSV)

Orateur : Charles Grellois (LIS)
Titre : When type theory meets model-checking
Résumé : Type theory and model-checking are two formal methods, aiming at ensuring the correctness of programs. In type theory, the idea is to annotate the instructions of the program with the properties they satisfy, so as to statically control how they will evolve during the computation, and to conclude that the program is correct — or not. In model-checking, one typically abstracts the program as a mathematical model, as a graph for instance, representing an approximation of its behavior. Then, an appropriate logical formula is devised over this program, and an algorithm checks automatically whether the abstract model satisfies the requirement. In the analysis of functional programs, higher-order constructions are possible: one can define functions that themselves take functions as inputs. Type theory is particularly useful to analyze such situations, as I will explain during the talk. I will first give a brief idea of what model-checking is, then explain what are the basics of type theory, and in a third time show how they where combined by Kobayashi in 2009 to perform model-checking of functional programs. If time allows, I will spend the last minutes giving an overview of the research I did in the last years building up on Kobayashi’s work and its extension by Kobayashi and Ong.


Orateur : Maximiliano Cristia (U. N. Rosario)
Titre : Programs as formulas (not as proofs)
Résumé : After the Curry-Howard correspondence and the type theories developed in the past decades, it emerged the idea of programs as proofs (of their properties). That is, if we have a proof P of a theorem T, we can make P a program whose type is T. This theory was a major breakthrough in programming language design and software verification. However, in this talk, I’ll show you an alternative and, in some sense, previous view: programs as formulas. In other words, let’s make the very formula to be a program; that is, we don’t need to make a proof to have a program. In particular I’m going to show {log} (setlog), which is a programming language but also an automated theorem prover. In {log} formulas are programs, and programs are formulas. We can use the same tool and the same language to specify programs, to simulate these specifications, to generate test cases and to prove properties of them. {log} works with formulas over the theory of finite sets, which allows for the specification of large classes of programs.


Orateur : Stephane Demri (LSV)
Titre : On The Complexity of Resource-Bounded Logics
Résumé : We characterise the complexity of model-checking problems for resource-bounded logics by taking advantage of recent results on decision problems for alternating VASS. For instance, we show that the model-checking problem for the logic RBATL is 2EXPTIME-complete and we establish that for RBATL* the problem remains decidable. A parameterised version of the logics is also discussed. This is a joint work with Natasha Alechina, Nils Bulling and Brian Logan.