Sciences du logiciel - Xavier Leroy
About
Available on
Community
203 episodes
Xavier Leroy Collège de France Science du logiciel Année 2023-2024 Séminaire - Daan Leijen : Design and Compilation of Efficient Effect Handlers in the Koka Language Daan Leijen Microsoft Research
Xavier Leroy Collège de France Science du logiciel Année 2023-2024 08 - Structures de contrôle : de « goto » aux effets algébriques : 08 - Structures de contrôle : de « goto » aux effets algébriques : Logiques de programmes pour le contrôle et les effets
Xavier Leroy Collège de France Science du logiciel Année 2023-2024 Séminaire - Matija Pretnar : How Mathematics Guides Effect Handlers Matija Pretnar Université de Ljubljana
Xavier Leroy Collège de France Science du logiciel Année 2023-2024 07 - Structures de contrôle : de « goto » aux effets algébriques : Typage et analyse statique des effets
Xavier Leroy Collège de France Science du logiciel Année 2023-2024 Séminaire - Olivier Danvy : Les continuations : cinq minutes pour les apprendre, toute une vie pour les comprendre Olivier Danvy National University of Singapore
Xavier Leroy Collège de France Science du logiciel Année 2023-2024 06 - Structures de contrôle : de « goto » aux effets algébriques : Théorie des effets : des monades aux effets algébriques
Xavier Leroy Collège de France Science du logiciel Année 2023-2024 Séminaire - Andrew Kennedy : Compiling with Continuations Andrew Kennedy Meta
Xavier Leroy Collège de France Science du logiciel Année 2023-2024 05 - Structures de contrôle : de « goto » aux effets algébriques : Pratique des effets : des exceptions aux gestionnaires d'effets
Xavier Leroy Collège de France Science du logiciel Année 2023-2024 04 - Structures de contrôle : de « goto » aux effets algébriques : Programmer ses structures de contrôle : continuations et opérateurs de contrôle
Xavier Leroy Collège de France Science du logiciel Année 2023-2024 Séminaire - Delphine Demange : Représentations intermédiaires pour la compilation : s'affranchir du graphe de flot de contrôle Delphine Demange Université de Rennes
Xavier Leroy Collège de France Science du logiciel Année 2023-2024 Séminaire - Caroline Collange : Comment concilier parallélisme et contrôle ? Approches des architectures de processeurs généralistes et graphiques Caroline Collange Inria
Xavier Leroy Collège de France Science du logiciel Année 2023-2024 03 - Structures de contrôle : de « goto » aux effets algébriques : Chassez le contrôle... : la programmation déclarative
Xavier Leroy Collège de France Science du logiciel Année 2023-2024 02 - 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 Leroy Collège de France Science du logiciel Année 2023-2024 01 - Structures de contrôle : de « goto » aux effets algébriques : Naissance des structures de contrôle : du « goto » à la programmation structurée
Xavier Leroy Collège de France Science du logiciel Année 2022-2023 Structures de données persistantes Séminaire - Pierre-Etienne Meunier : Une algèbre de modifications, ou : le contrôle de versions pour tous
Xavier Leroy Collège de France Science du logiciel Année 2022-2023 Structures de données persistantes À la recherche du vecteur perdu : limites théoriques et conclusions Jusqu'à 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 Leroy Collège de France Science du logiciel Année 2022-2023 Structures de données persistantes Séminaire - Arthur Charguéraud : Comment allier persistance et performance Cet 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 Leroy Collège de France Science du logiciel Année 2022-2023 Structures de données persistantes De 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 Leroy Collège de France Science du logiciel Année 2022-2023 Structures de données persistantes Séminaire - KC Sivaramakrishnan : Mergeable Replicated Data Types Replicated 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 Leroy Collège de France Science du logiciel Année 2022-2023 Structures de données persistantes Systèmes de numération et types non réguliers Un 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.
Xavier Leroy Collège de France Science du logiciel Année 2022-2023 Structures de données persistantes Séminaire - Jean-Christophe Filliatre : Structures de données semi-persistantes
Xavier Leroy Collège de France Science du logiciel Année 2022-2023 Structures de données persistantes Concilier amortissement et persistance : de l'importance de la paresse Dans ce cours, nous nous intéresserons aux structures de données persistantes dont l'implémentation utilise « sous le capot » des structures impératives et de la mutation en place, tout en préservant une interface purement fonctionnelle. Nous partirons des tableaux fonctionnels de Baker, qui combinent un tableau impératif et des liste de différences, puis introduirons progressivement la technique des « fat nodes » de Driscoll, Sarnak, Sleator et Tarjan, qui donne un procédé systématique pour rendre persistante une structure d'arbre impérative.
Xavier Leroy Collège de France Science du logiciel Année 2022-2023 Structures de données persistantes Séminaire - Tobias Nipkow : Verification of functional data structures: Correctness and complexity The talk gives a brief overview of our book "Functional Algorithms, Verified!" and its approach to verifying not just correctness but also running time of a large collection of functional algorithms. Then, two examples are presented in more detail: real time queues and double-ended queues that are implemented purely functionally with the help of stacks and whose operations have guaranteed constant running time.
Xavier Leroy Collège de France Science du logiciel Année 2022-2023 Structures de données persistantes Séminaire - Tobias Nipkow : Verification of functional data structures: Correctness and complexity The talk gives a brief overview of our book "Functional Algorithms, Verified!" and its approach to verifying not just correctness but also running time of a large collection of functional algorithms. Then, two examples are presented in more detail: real time queues and double-ended queues that are implemented purely functionally with the help of stacks and whose operations have guaranteed constant running time.
Xavier Leroy Collège de France Science du logiciel Année 2022-2023 Structures de données persistantes Concilier amortissement et persistance : de l'importance de la paresse L'amortissement est un principe de conception de structures de données qui vise à garantir un coût moyen par opération sur toute séquence d'opérations, le coût élevé de certaines opérations étant amorti par le coût faible d'opérations précédentes. Après un rappel des principes de l'amortissement et de l'analyse en temps amorti, le cours montrera des exemples de structures de données persistantes qui ont une complexité O(1) à condition d'être utilisées de manière linéaire. Nous étudierons ensuite l'approche d'Okasaki pour concilier amortissement et persistance générale (non linéaire), utilisant l'évaluation paresseuse (à la demande) de certains calculs.
Xavier Leroy Collège de France Science du logiciel Année 2022-2023 Structures de données persistantes Arbres équilibrés + copie de branches = persistance Copier et modifier une branche d'un arbre équilibré, tout en partageant les sous-arbres non modifiés avec l'arbre d'origine, est une technique simple et générale pour construire de nombreuses structures de données persistantes ayant des complexités O(log n). Le cours montrera cette technique à l'œuvre sur des structures de type « dictionnaire » : arbres de recherche, arbres préfixes, arbres préfixes avec hachage (HAMT), arbres de Braun, etc.
Xavier Leroy Collège de France Science du logiciel Année 2022-2023 Structures de données persistantes Introduction aux structures persistantes et à la programmation purement fonctionnelle Ce premier cours décrira l'émergence des structures de données persistantes dans deux contextes historiques différents : l'émergence des langages de programmation purement fonctionnels et de leurs approches équationnelles de dérivation et de vérification des programmes, d'une part, et de l'autre l'apparition de besoins nouveaux, notamment en algorithmique géométrique, de partager efficacement les représentations en mémoire de plusieurs structures de données qui diffèrent en peu de points. Nous verrons au passage nos premiers exemples de structures persistantes, à base de listes, d'arbres binaires, ou de tableaux avec historiques de modifications.
Xavier Leroy Collège de France Science du logiciel Année 2021-2022 Sécurité du logiciel : quel rôle pour les langages de programmation ? Compiler un programme source en code machine peut être l'occasion de le rendre plus résistant à certaines attaques. Cependant, de nombreuses optimisations de compilation, pourtant sémantiquement correctes, peuvent affaiblir la sécurité du programme. Nous verrons comment caractériser ces différences de sécurité entre un fragment de programme source et son code compilé à l'aide d'outils sémantiques classiques : l'équivalence observationnelle et le problème de la full abstraction. Nous présenterons quelques approches qui ont été proposées pour compiler tout en préservant les équivalences observationnelles.
Xavier Leroy Collège de France Science du logiciel Année 2021-2022 Sécurité du logiciel : quel rôle pour les langages de programmation ? Compiler un programme source en code machine peut être l'occasion de le rendre plus résistant à certaines attaques. Cependant, de nombreuses optimisations de compilation, pourtant sémantiquement correctes, peuvent affaiblir la sécurité du programme. Nous verrons comment caractériser ces différences de sécurité entre un fragment de programme source et son code compilé à l'aide d'outils sémantiques classiques : l'équivalence observationnelle et le problème de la full abstraction. Nous présenterons quelques approches qui ont été proposées pour compiler tout en préservant les équivalences observationnelles.
Xavier Leroy Collège de France Science du logiciel Année 2021-2022 Sécurité du logiciel : quel rôle pour les langages de programmation ? Compiler un programme source en code machine peut être l'occasion de le rendre plus résistant à certaines attaques. Cependant, de nombreuses optimisations de compilation, pourtant sémantiquement correctes, peuvent affaiblir la sécurité du programme. Nous verrons comment caractériser ces différences de sécurité entre un fragment de programme source et son code compilé à l'aide d'outils sémantiques classiques : l'équivalence observationnelle et le problème de la full abstraction. Nous présenterons quelques approches qui ont été proposées pour compiler tout en préservant les équivalences observationnelles.
