Sciences du logiciel - Xavier Leroy

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...

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...

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 m...

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, constructin...

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 remarquablem...

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 fonc...

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....

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é...

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...

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 équat...

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...

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...

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 ? Qu'il soit vérifié dynamiquement (pendant l'exécution) ou statiquement (par analyse préalable), le typage est un aspect essentiel des langages de programmation de haut niveau. Dans ce cours, nous étudierons les contributions du typage à la sécurité des logiciels,...

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 ? L'isolation d'un logiciel possiblement malveillant ou compromis est nécessaire pour qu'il ne puisse pas compromettre d'autres logiciels s'exécutant dans le même environnement et encore moins les mécanismes de sécurité du système d'exploitation et du matériel. Nou...

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 ? L'isolation d'un logiciel possiblement malveillant ou compromis est nécessaire pour qu'il ne puisse pas compromettre d'autres logiciels s'exécutant dans le même environnement et encore moins les mécanismes de sécurité du système d'exploitation et du matériel. Nou...

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 ? Certaines informations sont plus confidentielles que d'autres, ou plus digne de confiance que d'autres. Après une introduction aux politiques de confidentialité de Bell-Lapadula et d'intégrité de Biba, nous étudierons comment contrôler les flux d'information à tr...

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 ? Comment rendre un logiciel résistant non seulement aux « bugs » et aux pannes involontaires, mais aussi aux attaques et à l'utilisation malveillante ? C'est le problème général de la sécurité du logiciel, que nous introduirons dans ce premier cours. Nous étudiero...

Xavier Leroy Collège de France Science du logiciel Année 2020-2021 Logiques de programmes : quand la machine raisonne sur ses logiciels Dans le cinquième cours, nous avons étudié quatre extensions des logiques de séparation des précédents cours qui permettent ou facilitent la spécification et la vérification d'une plus large classe de programmes. La première extension est l'opérateur d'implication...

Xavier Leroy Collège de France Science du logiciel Année 2020-2021 Logiques de programmes : quand la machine raisonne sur ses logiciels Dans le cinquième cours, nous avons étudié quatre extensions des logiques de séparation des précédents cours qui permettent ou facilitent la spécification et la vérification d'une plus large classe de programmes. La première extension est l'opérateur d'implication...

Xavier Leroy Collège de France Science du logiciel Année 2020-2021 Logiques de programmes : quand la machine raisonne sur ses logiciels Dans le cinquième cours, nous avons étudié quatre extensions des logiques de séparation des précédents cours qui permettent ou facilitent la spécification et la vérification d'une plus large classe de programmes. La première extension est l'opérateur d'implication...

Xavier Leroy Collège de France Science du logiciel Année 2020-2021 Logiques de programmes : quand la machine raisonne sur ses logiciels Les processeurs multicœurs sont un exemple d'architecture parallèle à mémoire partagée, où plusieurs unités de calcul travaillent simultanément sur une mémoire commune. La programmation de ces architectures est difficile : il faut maîtriser les interférences possi...