Sciences du logiciel - Xavier Leroy

Xavier LeroyCollège de FranceScience du logicielAnnée 2023-202406 - Structures de contrôle : de « goto » aux effets algébriques : Théorie des effets : des monades aux effets algébriques

Xavier LeroyCollège de FranceScience du logicielAnnée 2023-2024Séminaire - Andrew Kennedy : Compiling with ContinuationsAndrew KennedyMeta

Xavier LeroyCollège de FranceScience du logicielAnnée 2023-202405 - Structures de contrôle : de « goto » aux effets algébriques : Pratique des effets : des exceptions aux gestionnaires d'effets

Xavier LeroyCollège de FranceScience du logicielAnnée 2023-202404 - Structures de contrôle : de « goto » aux effets algébriques : Programmer ses structures de contrôle : continuations et opérateurs de contrôle

Xavier LeroyCollège de FranceScience du logicielAnnée 2023-2024Séminaire - Delphine Demange : Représentations intermédiaires pour la compilation : s'affranchir du graphe de flot de contrôleDelphine DemangeUniversité de Rennes

Xavier LeroyCollège de FranceScience du logicielAnnée 2023-2024Séminaire - Caroline Collange : Comment concilier parallélisme et contrôle ? Approches des architectures de processeurs généralistes et graphiquesCaroline CollangeInria

Xavier LeroyCollège de FranceScience du logicielAnnée 2023-202403 - Structures de contrôle : de « goto » aux effets algébriques : Chassez le contrôle... : la programmation déclarative

Xavier LeroyCollège de FranceScience du logicielAnnée 2023-202402 - Structures de contrôle : de « goto » aux effets algébriques : Structures de contrôle avancées : des subroutines aux coroutines et au parallélisme

Xavier LeroyCollège de FranceScience du logicielAnnée 2023-202401 - Structures de contrôle : de « goto » aux effets algébriques : Naissance des structures de contrôle : du « goto » à la programmation structurée

Xavier LeroyCollège de FranceScience du logicielAnnée 2022-2023Structures de données persistantesSéminaire - Pierre-Etienne Meunier : Une algèbre de modifications, ou : le contrôle de versions pour tous

Xavier LeroyCollège de FranceScience du logicielAnnée 2022-2023Structures de données persistantesÀ la recherche du vecteur perdu : limites théoriques et conclusionsJusqu'à quel point une structure de données persistante peut être efficace ? Y a-t-il forcément un surcoût par rapport à une structure transiente ? Le dernier cours essaiera de répondre à ces questions, d'abord en passant en revue les meilleures implémentations connues des tableaux persistants, purement fonctionnelles ou non, puis en étudiant les bornes inférieures sur l'efficacité des modèles de calcul « LISP pur » et « LISP impur » établies par Ben-Armarm, Galil, et Pippenger.

Xavier LeroyCollège de FranceScience du logicielAnnée 2022-2023Structures de données persistantesSéminaire - Arthur Charguéraud : Comment allier persistance et performanceCet exposé explore trois approches permettant d'optimiser les performances de programmes exploitant des structures persistantes. La première approche consiste à optimiser les structures purement fonctionnelles en augmentant l'arité des feuilles et des nœuds des arbres. La deuxième approche consiste à exploiter les effets de bords pour réaliser la persistance. La troisième approche consiste à modifier l'interface en autorisant des versions transitoires non persistantes, selon la technique dite de « transience ». Je montrerai comment mettre en pratique ces trois approches sur des diverses structures : piles, files, tableaux, et séquences sécables et concaténables.

Xavier LeroyCollège de FranceScience du logicielAnnée 2022-2023Structures de données persistantesDe la dérivation formelle à la navigation dans une structure : contextes, zippers, index, etc.Il est souvent utile de pouvoir désigner une partie d'une structure de données (par exemple, un sous-arbre d'un arbre) et opérer sur cette partie de manière locale. Dans les algèbres de termes, cela se modélise à l'aide de contextes. Cependant, les « zippers » de Huet, une présentation duale des contextes, permet de se déplacer dans un terme de manière algorithmiquement efficace. Nous verrons comment les types des contextes et des zippers s'obtiennent systématiquement à partir d'un type algébrique en utilisant les mêmes règles que pour la dérivation de fonctions à une variable. Nous ferons ensuite le lien entre zippers et index (« fingers »), une technique algorithmique classique pour tenir à jour des pointeurs à l'intérieur d'un arbre.

Xavier LeroyCollège de FranceScience du logicielAnnée 2022-2023Structures de données persistantesSéminaire - KC Sivaramakrishnan : Mergeable Replicated Data TypesReplicated data types (RDTs) are specialised data structures that allow for concurrent modification of multiple replicas, even when they are geographically dispersed, without requiring coordination between them. However, constructing efficient and correct RDTs is challenging due to the complexity involved in reasoning about independently evolving states of replicas and resolving conflicts between them.In this talk, I will introduce Mergeable Replicated Data Types (MRDTs), a practical approach to constructing and verifying RDTs that is both efficient and correct. MRDTs build on the concept of a distributed version control system like Git, but extend it to arbitrary data types rather than just files. The key idea is to make sequential data types suitable for distribution by equipping them with a three-way merge function that reconciles conflicting versions. I will discuss how this merge function captures the complexities of distribution, simplifying both implementation and verification. Furthermore, I will discuss the critical role played by persistent data structures in MRDTs, as well as the inherent trade-off between persistence and efficiency in distributed data stores.

Xavier LeroyCollège de FranceScience du logicielAnnée 2022-2023Structures de données persistantesSystèmes de numération et types non réguliersUn système de numération permet de représenter efficacement de grands nombres en donnant des poids différents aux chiffres successifs (par exemple, 1, 10, 100, 1 000, etc.). Cette idée inspire aussi la conception de structures persistantes remarquablement efficaces, notamment pour les listes à accès direct et les files de priorité. Nous décrirons ensuite l'utilisation de types algébriques non réguliers pour implémenter de telles structures de manière plus simple et mieux contrôlée par le typage. Nous terminerons par l'étude des « finger trees » de Hinze et Paterson, une structure polyvalente qui applique plusieurs de ces techniques.