Séminaire tutoré

M2 IMD, 2023—2024

Cette page rassemble les informations et ressources relatives au séminaire tutoré du M2 IMD, organisé par Shantanu Das (LIS) et Pierre Guillon (I2M)

Le programme du séminaire est organisé en deux temps:

• les premières séances sont assurées par des chercheurs et chercheuses des équipes impliquées dans le master;
• les séances suivantes sont consacrées à des présentations d’articles travaillés par les étudiantes et étudiants.

Tous les exposés sont donnés en anglais. Ils ont généralement lieu le lundi après-midi sur le campus de Luminy.

Pour les présentations d’articles :

• Chaque étudiante ou étudiant choisit un article de recherche, en anglais, parmi les propositions ci-dessous.
• Ce choix est arrêté au plus tard le 10 novembre.
• L’exposé donné au séminaire consiste en la présentation de l’article choisi. Cette présentation doit être focalisée sur les aspects classiques (contexte, objectif, résultats obtenus, perspectives) et détailler un peu la partie technique de l'article.

Séances

06 novembre, 14h00 (E.06.13): Invited Seminar -- Victor Chepoi (LIS)

Boundary rigidity of CAT(0) cube complexes.
In this talk, we show that finite CAT(0) cube complexes can be reconstructed from their boundary distances (computed in their 1-skeleta). This result was conjectured by Haslegrave, Scott, Tamitegama, and Tan (2023). The reconstruction of a finite cell complex from the boundary distances is the discrete version of the boundary rigidity problem, which is a classical problem from Riemannian geometry. In the proofs, we use the bijection between CAT(0) cube complexes and median graphs and the corner peelings of median graphs. (Joint work with J. Chalopin)

16 novembre, 14h00 (E.06.13): Invited Seminar -- Yann-Situ Gazull (LIS)

An Introduction to Homology and Holes. (slides sources)
Algebraic topology is a field of mathematics that studies the topology of shapes and spaces with algebraic structures (group, fields, ...). In computer science, a useful subfield of algebraic topology is called homology. Interestingly, this subfield is closely related to the intuitive concept of holes. In this presentation, we will see how we can define holes and homology, both intuitively and formally. Then, some personal research work about how to "measure" geometric holes will be presented.

22 novembre, 14h00 (E.01.12): Invited Seminar -- Guy McCusker (University of Bath)

An introduction to quantitative relational models.
Denotational semantics studies proofs and programs by interpreting them in a mathematical model. This talk will give an introduction to denotational semantics for the typed lambda-calculus, starting with the simplest possible model based on sets and functions, and progressing via Scott’s graph models to relational models that can reveal quantitative aspects of program behaviour. No familiarity with denotational semantics will be assumed.

11 décembre, 14h : Séance Annulé

18 décembre, 14h (E.06.13):

Raphaël LAURENT: On Non-Computable Functions

Yao David KOLEGAIN:Assigning meaning to programs

Leonardo VENTURA:Towards an Algebraic Theory of Boolean Circuits

08 janvier, 14h (E.06.13):

Denis BELLE:On the Space Complexity of Randomized Synchronization

Thibault SCHNEEBERGER: Periodicity and Immortality in Reversible Computing

15 janvier, 14h (E.06.13):

Valentino BOUCARD:Cooperative mobile guards in grids

Houssein MANSOUR:Tilings, tiling spaces and topology

Nino DAUVIER:Non-idempotent intersection types for the Lambda-Calculus

22 janvier, 14h (E.06.13):

Rita ARFOUL:Belenios: a simple private and verifiable electronic voting system

Marco SANTAMARIA:On linear combinations of lambda-terms

Camilo NUNEZ RUBIANO:The theory of timed automata

Articles proposés

Pour chaque article, on indique la personne qui l’a proposé : cette personne acceptera probablement (mais pas nécessairement) de correspondre et discuter avec vous pour éclairer votre lecture si nécessaire.

Non-idempotent intersection types for the Lambda-Calculus de A. Bucciarelli, D. Kesner & D. Ventura. Logic Journal of the IGPL, 25(4):431--464, 2017.

Proposé par Lionel Vaux Auclair (I2M), qui écrit:

Ce papier revisite des caractérisations de la normalisation (de tête, faible, forte, etc. ) au moyen de systèmes de types avec intersection non idempotente. C’est un outil récent qui provient de travaux en logique linéaire et qui a trouvé sa place dans la boîte à outils du logicien/sémanticien dans la dernière décennie.

Linear lambda terms as invariants of rooted trivalent maps de N. Zeilberger. Journal of Functional Programming, Volume 26, 2016.

Proposé par Lionel Vaux Auclair (I2M), qui écrit:

Ce papier revisite une correspondance précédemment établie entre une certaine classe de λ-termes et une certaine classe de cartes combinatoires (qui sont une représentation combinatoire de graphes plongés sur des surfaces et considérés à déformation près). C’est un peu technique mais au bout du chemin on trouve une reformulation du théorème des 4 couleurs comme une propriété de typage.

(Leftmost-Outermost) Beta Reduction is Invariant, Indeed de B. Accattoli & U. Dal Lago. Logical Methods in Computer Science, March 9, 2016, Volume 12, Issue 1.

Proposé par Lionel Vaux Auclair (I2M), qui écrit:

Ce papier démontre que le nombre d’étapes de β-réduction gauche menant à une forme normale est une notion raisonnable de temps de calcul. L’article est long et technique mais bien organisé : on peut naviguer dedans pour en tirer l’essentiel sans nécessairement détailler toutes les étapes.

Belenios: a simple private and verifiable electronic voting system de V. Cortier, P. Gaudry, & S. Glondu. Foundations of Security, Protocols, and Equational Reasoning, LNCS volume 11565, pages 214-238, 2019.

Proposé par Arnaud Labourel (LIS).

Exploring Unknown Undirected Graphs de P. Panaite & A. Pelc. Journal of Algorithms, Volume 33, Issue 2, pages 281-295, 1999.

Proposé par Arnaud Labourel (LIS).

Infinite λ-calculus and non-sensible models d’Alessandro Berarducci. Theoretical Computer Science Volume 212, Issues 1–2, 6 February 1999.

Proposé par Rémy Cerda (I2M), qui écrit:

Il s'agit de l'une des premières présentations d'un λ-calcul infinitaire (les termes et les séquences de réduction peuvent être infinis), contemporaine de celle de Kennaway et al. Ici, il s'agit de la version la plus « sauvage » du calcul infinitaire mais elle est présentée de manière très lisible, sans bureaucratie sur l'infini (ordinaux, coinduction, …). L'auteur reprend plein de notions classiquement définies en λ-calcul (résidus, réduction de tête, standardisation, …), et aboutit à un modèle du λ-calcul qui raffine celui des arbres de Böhm.

Nominal Techniques de Andrew Pitts. ACM SIGLOG News, Volume 3, Number 1, January 2016.

Proposé par Rémy Cerda (I2M), qui écrit:

Les notions de variable et de champ d'une variable sont centrales en informatique — qu'elle soit théorique (α-équivalence en λ-calcul) ou appliquée (variables locales et globales d'un langage de programmation) — mais aussi aux fondements des mathématiques. Développées depuis vingt ans, les techniques nominales donnent une formalisation abstraite de ces notions, applicable dans un cadre ensembliste aussi bien que catégorique. L'article propose un survol pédagogique de ces techniques.

Balanced Allocations de Y. Azar, A. Z. Broder, A. R. Karlin, E. Upfal. Proceedings of the 26th ACM Symposium on Theory of Computing (STOC), 1994.

Proposé par Shantanu Das (LIS), qui écrit:

The paper studies a simple randomized algorithm for placing n balls into n bins, that achieves a balanced partition. This has important consequences for the problems of load balancing and resource allocation.

Cooperative mobile guards in grids d’A. Kosowski, M. Małafiejski, & P. Żyliński. Computational Geometry 37.2, 2007.

Proposé par Shantanu Das (LIS).

Towards an Algebraic Theory of Boolean Circuits d’Yves Lafont. Journal of Pure and Applied Algebra 184 (2-3), p. 257–310, Elsevier (2003).

Proposé par Yves Lafont (I2M).

Generators and relations for n-qubit Clifford operators de P. Selinger. Logical Methods in Computer Science 11(2:10), p. 1–17 (2015).

Proposé par Yves Lafont (I2M).

On the cancellation law among finite relational structures de L. Lovász. Periodica Mathematica Hungarica 1, pages 145–156 (1971).

Proposé par Enrico Porreca (LIS) qui écrit:

Il s’agit d’un article classique de Lovász sur le produit direct de relations, dont les résultats sont parfois très utiles en théorie des graphes (et ailleurs…) ; notamment, au delà du sujet principal, on y retrouve un théorème dont la restriction aux graphes dit que G₁ et G₂ sont isomorphes si et seulement si, pour tout graphe H, il y a le même nombre d’homomorphismes de H vers G₁ et vers G₂.

Notions of Computation and Monads de E. Moggi. Information and Computation 93(1): 55-92 (1991)

Proposé par Étienne Miquey (I2M)

On Linear Combinations of lambda -Terms de Lionel Vaux. Proceedings of 18th International Conference on Term Rewriting and Applications (RTA) pages 374-388, 2007.

Proposé par Étienne Miquey (I2M)

On Non-Computable Functions de T. Rado. Bell System Technical Journal, 41: 3. pages 877-884, 1962.

Proposé par Kevin Perrot (LIS), qui écrit:

Pour ouvrir la discussion/présentation je conseille la lecture de ce billet de blog par Scott Aaronson.

Tiling the Plane with a Fixed Number of Polyominoes de N. Ollinger. Proceedings of 3rd Conf. on Language and Automata Theory and Applications (LATA) 2009.

Proposé par Kevin Perrot (LIS), qui écrit:

It is proven that any set of Wang tiles can be simulated by 5 polyominoes, hence the tiling problem for polyonminoes is undecidable even when restricted to tile sets of only 5 polynominoes.

Probabilistic Operational Semantics for the Lambda Calculus de U. Dal Lago & M. Zorzi. RAIRO - Theoretical Informatics and Applications, (46)3. pages 413 - 450, 2012.

Proposé par Raphaëlle Crubillé (LIS) qui a écrit:

Ce papier explore de manière systématique comment les notions standard de sémantique opérationelle pour le lambda-calcul (call-by-value, call-by-name, small-step semantics, big-step semantics) peuvent être généralisés lorsqu'on ajoute un opérateur de choix probabiliste.

Assigning meaning to programs de Robert Floyd. Proceedings of AMS Symp. on Applied Mathematics, pp. 19–31, Vol. 19, 1967.

Proposé par Alexey Muranov (I2M).

Automatic verification of multi-agent systems in parameterised grid-environments de B. Aminof, A. Murano, S. Rubin, & F. Zuleger. Proceedings of the 15th Conf. on Autonomous Agents and Multiagent Systems (AAMAS), pages 1190-1199, (2016).

Proposé par Maria Kokkou (LIS) qui écrit:

A self-contained introduction to both multi-agent systems and parameterised verification, it includes a lot of natural language explanations and motivating examples. Some familiarity with logic and automata is needed to be able to read the proofs but overall it is easy to read and touches on many topics and techniques that can be otherwise hard to understand or connect.

The theory of timed automata de R. Alur & D. Dill. Real-Time: Theory in Practice. REX 1991. LNCS volume 600, 1992.

Proposé par Karoliina Lehtinen (LIS).

Alternating tree automata, parity games, and modal mu-calculus de Thomas Wilke. Bulletin of the Belgian Mathematical Society--Simon Stevin 8.2, pages 359-391, 2001.

Proposé par Karoliina Lehtinen (LIS).

Cellular Automata and Powers of p/q de J. Kari & J. Kopra.

Proposé par Pierre Guillon (I2M), qui écrit:

• AC et théorie des nombres,
• un AC qui fait des multiplications et du coup des orbites parcourent tous les mots finis.

Groups defined by Automata de L. Bartholdi & P. V. Silva. Handbook of Automata Theory (II.) pages 871-911, 2021.

Proposé par Pierre Guillon (I2M), qui écrit:

survol sur les groupes automatiques, puis sur les groupes d'automates.

Decidability of the HD0L ultimate periodicity problem de Fabien Durand. RAIRO Theoretical Informatics and Applications 47(2): 201-214 (2013)

Proposé par Pierre Guillon (I2M).

On the Space Complexity of Randomized Synchronization de Faith E. Fich, Maurice Herlihy & Nir Shavit. Journal of ACM 45(5): 843-862 (1998).

Proposé par Corentin Travers (LIS), qui écrit:

Sur la complexité en mémoire de quelques algorithmes en mémoire partagée.

On time-symmetry in cellular automata de A. Gajardo, J. Kari, & A. Moreira. Journal of Computer and System Sciences, Volume 78, Issue 4, pages 1115-1126, 2012.

Proposé par Guillaume Theyssier et Pierre Guillon (I2M), qui écrivent:

• quand la dynamique est proche de la dynamique inverse…;
• facile sauf la fin, nouveau par rapport au cours mais connecté à des notions vues, permet de faire une belle présentation.

Periodicity and Immortality in Reversible Computing de J. Kari & N. Ollinger. Proceedings of 33rd Symposium MFCS 2008.

Proposé par Guillaume Theyssier et Pierre Guillon (I2M), qui écrivent:

• indécidabilité de la périodicité des machines de Turing, puis des AC;
• gros résultat, beau mélange de modèles de calcul et systèmes dynamiques.

On the Undecidability of the Tiling Problem de J. Kari. Proceedings of 34th Conf. on Current Trends in Theory and Practice of Computer Science (SOFSEM) 2008.

Proposé par Guillaume Theyssier et Pierre Guillon (I2M), qui écrivent:

une preuve de l'indécidabilité du problème du pavage (y compris dans le plan hyperbolique) en passant par l'indécidabilité de la mortalité des fonctions affines par morceaux.

Tilings, tiling spaces and topology de L. Sadun. Philosophical Magazine 86: 875-881, (2006)

Proposé par Pierre Arnoux (I2M)

comme sujets indépendants quelques chapitres du livre. Par exemple, le début du chapitre 2 (définitions équivalentes des mots sturmiens) ou du chapitre 8 (théorème de Fine et Wilf) font déjà deux sujets sûrs.

Paperfolding morphisms, planefilling curves, and fractal tiles de M. Dekking. Theoretical Computer Science 414(1): 20-37 (2012)

Proposé par Pierre Arnoux (I2M).

Archives

Ici on trouve des exemples d’articles proposés les années précédentes.

https://www.i2m.univ-amu.fr/perso/lionel.vaux/ens/imd-seminaire/#articles