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.

Xavier LeroyCollège de FranceScience du logicielAnnée 2022-2023Structures de données persistantesSéminaire - Jean-Christophe Filliatre : Structures de données semi-persistantes

Xavier LeroyCollège de FranceScience du logicielAnnée 2022-2023Structures de données persistantesConcilier amortissement et persistance : de l'importance de la paresseDans 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 LeroyCollège de FranceScience du logicielAnnée 2022-2023Structures de données persistantesSéminaire - Tobias Nipkow : Verification of functional data structures: Correctness and complexityThe 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 LeroyCollège de FranceScience du logicielAnnée 2022-2023Structures de données persistantesSéminaire - Tobias Nipkow : Verification of functional data structures: Correctness and complexityThe 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 LeroyCollège de FranceScience du logicielAnnée 2022-2023Structures de données persistantesConcilier amortissement et persistance : de l'importance de la paresseL'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 LeroyCollège de FranceScience du logicielAnnée 2022-2023Structures de données persistantesArbres équilibrés + copie de branches = persistanceCopier 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 LeroyCollège de FranceScience du logicielAnnée 2022-2023Structures de données persistantesIntroduction aux structures persistantes et à la programmation purement fonctionnelleCe 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 LeroyCollège de FranceScience du logicielAnnée 2021-2022Sé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 LeroyCollège de FranceScience du logicielAnnée 2021-2022Sé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 LeroyCollège de FranceScience du logicielAnnée 2021-2022Sé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 LeroyCollège de FranceScience du logicielAnnée 2021-2022Sé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 LeroyCollège de FranceScience du logicielAnnée 2021-2022Sé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, des garanties de base (sûreté des valeurs et de la mémoire) indispensables pour l'isolation logicielle à des garanties d'intégrité plus fines s'appuyant sur l'abstraction de types et l'encapsulation procédurale des valeurs. Nous parlerons aussi des ownership types et des assertions en logique de séparation, et de leurs utilisations possibles pour la sécurité.

Xavier LeroyCollège de FranceScience du logicielAnnée 2021-2022Sé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, des garanties de base (sûreté des valeurs et de la mémoire) indispensables pour l'isolation logicielle à des garanties d'intégrité plus fines s'appuyant sur l'abstraction de types et l'encapsulation procédurale des valeurs. Nous parlerons aussi des ownership types et des assertions en logique de séparation, et de leurs utilisations possibles pour la sécurité.

Xavier LeroyCollège de FranceScience du logicielAnnée 2021-2022Sé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. Nous passerons en revue plusieurs mécanismes d'isolation : mémoire virtuelle, software fault isolation (SFI), sandboxing, et contrôle d'accès au niveau des interfaces logicielles (API).

Xavier LeroyCollège de FranceScience du logicielAnnée 2021-2022Sé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. Nous passerons en revue plusieurs mécanismes d'isolation : mémoire virtuelle, software fault isolation (SFI), sandboxing, et contrôle d'accès au niveau des interfaces logicielles (API).

Xavier LeroyCollège de FranceScience du logicielAnnée 2021-2022Sé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. Nous passerons en revue plusieurs mécanismes d'isolation : mémoire virtuelle, software fault isolation (SFI), sandboxing, et contrôle d'accès au niveau des interfaces logicielles (API).

Xavier LeroyCollège de FranceScience du logicielAnnée 2021-2022Sé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. Nous passerons en revue plusieurs mécanismes d'isolation : mémoire virtuelle, software fault isolation (SFI), sandboxing, et contrôle d'accès au niveau des interfaces logicielles (API).

Xavier LeroyCollège de FranceScience du logicielAnnée 2021-2022Sé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 à travers un programme, ou bien dynamiquement, ou bien statiquement à l'aide de systèmes de types ou de logiques de programmes.

Xavier LeroyCollège de FranceScience du logicielAnnée 2021-2022Sé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 à travers un programme, ou bien dynamiquement, ou bien statiquement à l'aide de systèmes de types ou de logiques de programmes.

Xavier LeroyCollège de FranceScience du logicielAnnée 2021-2022Sé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 étudierons ensuite quelques attaques récentes et les vulnérabilités logicielles qu'elles exploitent.

Xavier LeroyCollège de FranceScience du logicielAnnée 2021-2022Sé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 étudierons ensuite quelques attaques récentes et les vulnérabilités logicielles qu'elles exploitent.

Xavier LeroyCollège de FranceScience du logicielAnnée 2020-2021Logiques de programmes : quand la machine raisonne sur ses logicielsDans 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 séparante, familièrement appelé « baguette magique » en raison de sa forme, qui est l'adjoint de la conjonction séparante, au même titre que l'implication usuelle est l'adjoint de la conjonction usuelle. Cette « baguette magique » facilite le raisonnement en logique de séparation, notamment via la règle de conséquence ramifiée ou via un calcul de plus faibles préconditions.La deuxième extension permet de vérifier des processus qui partagent des données mais y accèdent en lecture seule, sans modifications. Il s'agit d'associer des permissions aux cellules de la mémoire, ces permissions pouvant être partielles (permettant uniquement la lecture) ou complètes (permettant aussi l'écriture et la libération). Deux modèles bien connus de permissions partielles sont les permissions fractionnaires et les permissions comptées. Nous avons illustré l'utilisation de ces dernières pour vérifier un verrou à lecteurs multiples implémenté par deux sémaphores.Le « code fantôme » est la troisième technique étudiée dans cette séance. Il s'agit de commandes qui ne sont pas exécutées dans le programme final, mais contribuent à définir des « variables fantômes » qui simplifient la vérification. Dans le cadre du calcul parallèle, code et variables fantômes permettent de garder trace des calculs faits par chacun des processus et comment ces calculs individuels contribuent à l'exécution globale du programme.La dernière extension que nous avons décrite permet de stocker en mémoire des verrous et leur invariant de ressources, tout comme les données protégées par ces verrous. Cela permet de spécifier et de vérifier des algorithmes parallèles à grain fin, comme nous l'avons illustré avec une structure de liste simplement chaînée avec verrouillage couplé.Aussi disparates qu'elles peuvent sembler, ces extensions et bien d'autres sont des cas particuliers d'un petit nombre de notions plus générales, comme le montre l'infrastructure logique Iris.

Xavier LeroyCollège de FranceScience du logicielAnnée 2020-2021Logiques de programmes : quand la machine raisonne sur ses logicielsDans 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 séparante, familièrement appelé « baguette magique » en raison de sa forme, qui est l'adjoint de la conjonction séparante, au même titre que l'implication usuelle est l'adjoint de la conjonction usuelle. Cette « baguette magique » facilite le raisonnement en logique de séparation, notamment via la règle de conséquence ramifiée ou via un calcul de plus faibles préconditions.La deuxième extension permet de vérifier des processus qui partagent des données mais y accèdent en lecture seule, sans modifications. Il s'agit d'associer des permissions aux cellules de la mémoire, ces permissions pouvant être partielles (permettant uniquement la lecture) ou complètes (permettant aussi l'écriture et la libération). Deux modèles bien connus de permissions partielles sont les permissions fractionnaires et les permissions comptées. Nous avons illustré l'utilisation de ces dernières pour vérifier un verrou à lecteurs multiples implémenté par deux sémaphores.Le « code fantôme » est la troisième technique étudiée dans cette séance. Il s'agit de commandes qui ne sont pas exécutées dans le programme final, mais contribuent à définir des « variables fantômes » qui simplifient la vérification. Dans le cadre du calcul parallèle, code et variables fantômes permettent de garder trace des calculs faits par chacun des processus et comment ces calculs individuels contribuent à l'exécution globale du programme.La dernière extension que nous avons décrite permet de stocker en mémoire des verrous et leur invariant de ressources, tout comme les données protégées par ces verrous. Cela permet de spécifier et de vérifier des algorithmes parallèles à grain fin, comme nous l'avons illustré avec une structure de liste simplement chaînée avec verrouillage couplé.Aussi disparates qu'elles peuvent sembler, ces extensions et bien d'autres sont des cas particuliers d'un petit nombre de notions plus générales, comme le montre l'infrastructure logique Iris.

Xavier LeroyCollège de FranceScience du logicielAnnée 2020-2021Logiques de programmes : quand la machine raisonne sur ses logicielsDans 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 séparante, familièrement appelé « baguette magique » en raison de sa forme, qui est l'adjoint de la conjonction séparante, au même titre que l'implication usuelle est l'adjoint de la conjonction usuelle. Cette « baguette magique » facilite le raisonnement en logique de séparation, notamment via la règle de conséquence ramifiée ou via un calcul de plus faibles préconditions.La deuxième extension permet de vérifier des processus qui partagent des données mais y accèdent en lecture seule, sans modifications. Il s'agit d'associer des permissions aux cellules de la mémoire, ces permissions pouvant être partielles (permettant uniquement la lecture) ou complètes (permettant aussi l'écriture et la libération). Deux modèles bien connus de permissions partielles sont les permissions fractionnaires et les permissions comptées. Nous avons illustré l'utilisation de ces dernières pour vérifier un verrou à lecteurs multiples implémenté par deux sémaphores.Le « code fantôme » est la troisième technique étudiée dans cette séance. Il s'agit de commandes qui ne sont pas exécutées dans le programme final, mais contribuent à définir des « variables fantômes » qui simplifient la vérification. Dans le cadre du calcul parallèle, code et variables fantômes permettent de garder trace des calculs faits par chacun des processus et comment ces calculs individuels contribuent à l'exécution globale du programme.La dernière extension que nous avons décrite permet de stocker en mémoire des verrous et leur invariant de ressources, tout comme les données protégées par ces verrous. Cela permet de spécifier et de vérifier des algorithmes parallèles à grain fin, comme nous l'avons illustré avec une structure de liste simplement chaînée avec verrouillage couplé.Aussi disparates qu'elles peuvent sembler, ces extensions et bien d'autres sont des cas particuliers d'un petit nombre de notions plus générales, comme le montre l'infrastructure logique Iris.

Xavier LeroyCollège de FranceScience du logicielAnnée 2020-2021Logiques de programmes : quand la machine raisonne sur ses logicielsDans 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 séparante, familièrement appelé « baguette magique » en raison de sa forme, qui est l'adjoint de la conjonction séparante, au même titre que l'implication usuelle est l'adjoint de la conjonction usuelle. Cette « baguette magique » facilite le raisonnement en logique de séparation, notamment via la règle de conséquence ramifiée ou via un calcul de plus faibles préconditions.La deuxième extension permet de vérifier des processus qui partagent des données mais y accèdent en lecture seule, sans modifications. Il s'agit d'associer des permissions aux cellules de la mémoire, ces permissions pouvant être partielles (permettant uniquement la lecture) ou complètes (permettant aussi l'écriture et la libération). Deux modèles bien connus de permissions partielles sont les permissions fractionnaires et les permissions comptées. Nous avons illustré l'utilisation de ces dernières pour vérifier un verrou à lecteurs multiples implémenté par deux sémaphores.Le « code fantôme » est la troisième technique étudiée dans cette séance. Il s'agit de commandes qui ne sont pas exécutées dans le programme final, mais contribuent à définir des « variables fantômes » qui simplifient la vérification. Dans le cadre du calcul parallèle, code et variables fantômes permettent de garder trace des calculs faits par chacun des processus et comment ces calculs individuels contribuent à l'exécution globale du programme.La dernière extension que nous avons décrite permet de stocker en mémoire des verrous et leur invariant de ressources, tout comme les données protégées par ces verrous. Cela permet de spécifier et de vérifier des algorithmes parallèles à grain fin, comme nous l'avons illustré avec une structure de liste simplement chaînée avec verrouillage couplé.Aussi disparates qu'elles peuvent sembler, ces extensions et bien d'autres sont des cas particuliers d'un petit nombre de notions plus générales, comme le montre l'infrastructure logique Iris.

Xavier LeroyCollège de FranceScience du logicielAnnée 2020-2021Logiques de programmes : quand la machine raisonne sur ses logicielsDans 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 séparante, familièrement appelé « baguette magique » en raison de sa forme, qui est l'adjoint de la conjonction séparante, au même titre que l'implication usuelle est l'adjoint de la conjonction usuelle. Cette « baguette magique » facilite le raisonnement en logique de séparation, notamment via la règle de conséquence ramifiée ou via un calcul de plus faibles préconditions.La deuxième extension permet de vérifier des processus qui partagent des données mais y accèdent en lecture seule, sans modifications. Il s'agit d'associer des permissions aux cellules de la mémoire, ces permissions pouvant être partielles (permettant uniquement la lecture) ou complètes (permettant aussi l'écriture et la libération). Deux modèles bien connus de permissions partielles sont les permissions fractionnaires et les permissions comptées. Nous avons illustré l'utilisation de ces dernières pour vérifier un verrou à lecteurs multiples implémenté par deux sémaphores.Le « code fantôme » est la troisième technique étudiée dans cette séance. Il s'agit de commandes qui ne sont pas exécutées dans le programme final, mais contribuent à définir des « variables fantômes » qui simplifient la vérification. Dans le cadre du calcul parallèle, code et variables fantômes permettent de garder trace des calculs faits par chacun des processus et comment ces calculs individuels contribuent à l'exécution globale du programme.La dernière extension que nous avons décrite permet de stocker en mémoire des verrous et leur invariant de ressources, tout comme les données protégées par ces verrous. Cela permet de spécifier et de vérifier des algorithmes parallèles à grain fin, comme nous l'avons illustré avec une structure de liste simplement chaînée avec verrouillage couplé.Aussi disparates qu'elles peuvent sembler, ces extensions et bien d'autres sont des cas particuliers d'un petit nombre de notions plus générales, comme le montre l'infrastructure logique Iris.

Xavier LeroyCollège de FranceScience du logicielAnnée 2020-2021Logiques de programmes : quand la machine raisonne sur ses logicielsDans 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 séparante, familièrement appelé « baguette magique » en raison de sa forme, qui est l'adjoint de la conjonction séparante, au même titre que l'implication usuelle est l'adjoint de la conjonction usuelle. Cette « baguette magique » facilite le raisonnement en logique de séparation, notamment via la règle de conséquence ramifiée ou via un calcul de plus faibles préconditions.La deuxième extension permet de vérifier des processus qui partagent des données mais y accèdent en lecture seule, sans modifications. Il s'agit d'associer des permissions aux cellules de la mémoire, ces permissions pouvant être partielles (permettant uniquement la lecture) ou complètes (permettant aussi l'écriture et la libération). Deux modèles bien connus de permissions partielles sont les permissions fractionnaires et les permissions comptées. Nous avons illustré l'utilisation de ces dernières pour vérifier un verrou à lecteurs multiples implémenté par deux sémaphores.Le « code fantôme » est la troisième technique étudiée dans cette séance. Il s'agit de commandes qui ne sont pas exécutées dans le programme final, mais contribuent à définir des « variables fantômes » qui simplifient la vérification. Dans le cadre du calcul parallèle, code et variables fantômes permettent de garder trace des calculs faits par chacun des processus et comment ces calculs individuels contribuent à l'exécution globale du programme.La dernière extension que nous avons décrite permet de stocker en mémoire des verrous et leur invariant de ressources, tout comme les données protégées par ces verrous. Cela permet de spécifier et de vérifier des algorithmes parallèles à grain fin, comme nous l'avons illustré avec une structure de liste simplement chaînée avec verrouillage couplé.Aussi disparates qu'elles peuvent sembler, ces extensions et bien d'autres sont des cas particuliers d'un petit nombre de notions plus générales, comme le montre l'infrastructure logique Iris.

Xavier LeroyCollège de FranceScience du logicielAnnée 2020-2021Logiques de programmes : quand la machine raisonne sur ses logicielsLes 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 possibles entre les actions des processus, et éviter les courses critiques (race conditions) entre des écritures et des lectures simultanées.Quelles logiques de programmes nous permettent de vérifier des programmes parallèles à mémoire partagée ? Pour répondre à cette question, le quatrième cours a introduit la logique de séparation concurrente (Concurrent Separation Logic, CSL), une extension de la logique de séparation avec des règles de raisonnement sur le parallélisme et l'exclusion mutuelle.La logique de séparation décrit très simplement le calcul parallèle sans partage de ressources, où les processus s'exécutent en parallèle sur des portions disjointes de la mémoire. C'est le cas de nombreux algorithmes récursifs sur les tableaux ou sur les arbres, où les appels récursifs s'effectuent sur des sous-arbres ou sous-tableaux disjoints.La CSL, comme introduite par O'Hearn en 2004, ajoute des règles de raisonnement sur les sections critiques permettant à plusieurs processus d'accéder à des ressources partagées à condition que ces accès s'effectuent en exclusion mutuelle. Les ressources partagées sont décrites par des formules de logique de séparation qui doivent être invariantes en dehors des sections critiques. Cela permet de décrire non seulement de nombreux idiomes de synchronisation entre processus, mais aussi les transferts de ressources qui s'effectuent implicitement lors de ces synchronisations.Nous avons défini une CSL pour le petit langage du précédent cours enrichi de constructions décrivant le parallélisme et les instructions atomiques. Nous avons montré comment construire sur ce langage et cette logique des sémaphores binaires, des sections critiques, et des schémas producteur-consommateur. Enfin, nous avons montré la correction sémantique de cette CSL en reprenant une démonstration publiée par Vafeiadis en 2011.

Xavier LeroyCollège de FranceScience du logicielAnnée 2020-2021Logiques de programmes : quand la machine raisonne sur ses logicielsLes 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 possibles entre les actions des processus, et éviter les courses critiques (race conditions) entre des écritures et des lectures simultanées.Quelles logiques de programmes nous permettent de vérifier des programmes parallèles à mémoire partagée ? Pour répondre à cette question, le quatrième cours a introduit la logique de séparation concurrente (Concurrent Separation Logic, CSL), une extension de la logique de séparation avec des règles de raisonnement sur le parallélisme et l'exclusion mutuelle.La logique de séparation décrit très simplement le calcul parallèle sans partage de ressources, où les processus s'exécutent en parallèle sur des portions disjointes de la mémoire. C'est le cas de nombreux algorithmes récursifs sur les tableaux ou sur les arbres, où les appels récursifs s'effectuent sur des sous-arbres ou sous-tableaux disjoints.La CSL, comme introduite par O'Hearn en 2004, ajoute des règles de raisonnement sur les sections critiques permettant à plusieurs processus d'accéder à des ressources partagées à condition que ces accès s'effectuent en exclusion mutuelle. Les ressources partagées sont décrites par des formules de logique de séparation qui doivent être invariantes en dehors des sections critiques. Cela permet de décrire non seulement de nombreux idiomes de synchronisation entre processus, mais aussi les transferts de ressources qui s'effectuent implicitement lors de ces synchronisations.Nous avons défini une CSL pour le petit langage du précédent cours enrichi de constructions décrivant le parallélisme et les instructions atomiques. Nous avons montré comment construire sur ce langage et cette logique des sémaphores binaires, des sections critiques, et des schémas producteur-consommateur. Enfin, nous avons montré la correction sémantique de cette CSL en reprenant une démonstration publiée par Vafeiadis en 2011.

Xavier LeroyCollège de FranceScience du logicielAnnée 2020-2021Logiques de programmes : quand la machine raisonne sur ses logicielsDans le troisième cours, nous avons étudié les structures de données et la vérification de programmes qui les manipulent. Les tableaux sont la plus ancienne des structures de données. Une extension simple de la logique de Hoare avec une règle pour l'affectation à un élément d'un tableau permet de spécifier et de vérifier de nombreux programmes utilisant des tableaux, comme par exemple les tris en place.Les pointeurs, aussi appelés références, permettent de représenter de nombreuses structures de données : graphes, listes chaînées, arbres... Un codage des pointeurs en termes de tableaux globaux, comme proposé par R. Burstall (1972) et développé par R. Bornat (2000), se révèle efficace pour vérifier des algorithmes opérant sur des graphes, mais très lourd pour les algorithmes sur les listes et autres structures chaînées. En effet, il est difficile d'éviter les situations de partage, d'alias et d'interférence qui peuvent invalider ces structures.C'est en cherchant à décrire et maîtriser ces phénomènes d'interférence que J. C. Reynolds, rejoint ensuite par P. O'Hearn et H. Yang, invente entre 1997 et 2001 la logique de séparation. Cette logique met en avant l'importance du raisonnement local et des règles d'encadrement associées, le besoin d'associer une empreinte mémoire à chaque assertion, et le concept de conjonction séparante entre assertions.Nous avons illustré l'approche en développant une logique de séparation pour un petit langage fonctionnel et impératif doté de variables immuables et de pointeurs vers des cases mémoires mutables. Cette logique de séparation permet de décrire très précisément de nombreuses structures de données par des prédicats de représentation : listes simplement ou doublement chaînées, listes circulaires, arbres, etc., et de spécifier et vérifier leurs principales opérations.Enfin, nous avons esquissé deux démonstrations de la correction sémantique de cette logique de séparation, l'une reposant sur une propriété de non-déterminisme de l'allocation mémoire ; l'autre, sur une quantification sur tous les encadrements possibles.

Xavier LeroyCollège de FranceScience du logicielAnnée 2020-2021Logiques de programmes : quand la machine raisonne sur ses logicielsDans le troisième cours, nous avons étudié les structures de données et la vérification de programmes qui les manipulent. Les tableaux sont la plus ancienne des structures de données. Une extension simple de la logique de Hoare avec une règle pour l'affectation à un élément d'un tableau permet de spécifier et de vérifier de nombreux programmes utilisant des tableaux, comme par exemple les tris en place.Les pointeurs, aussi appelés références, permettent de représenter de nombreuses structures de données : graphes, listes chaînées, arbres... Un codage des pointeurs en termes de tableaux globaux, comme proposé par R. Burstall (1972) et développé par R. Bornat (2000), se révèle efficace pour vérifier des algorithmes opérant sur des graphes, mais très lourd pour les algorithmes sur les listes et autres structures chaînées. En effet, il est difficile d'éviter les situations de partage, d'alias et d'interférence qui peuvent invalider ces structures.C'est en cherchant à décrire et maîtriser ces phénomènes d'interférence que J. C. Reynolds, rejoint ensuite par P. O'Hearn et H. Yang, invente entre 1997 et 2001 la logique de séparation. Cette logique met en avant l'importance du raisonnement local et des règles d'encadrement associées, le besoin d'associer une empreinte mémoire à chaque assertion, et le concept de conjonction séparante entre assertions.Nous avons illustré l'approche en développant une logique de séparation pour un petit langage fonctionnel et impératif doté de variables immuables et de pointeurs vers des cases mémoires mutables. Cette logique de séparation permet de décrire très précisément de nombreuses structures de données par des prédicats de représentation : listes simplement ou doublement chaînées, listes circulaires, arbres, etc., et de spécifier et vérifier leurs principales opérations.Enfin, nous avons esquissé deux démonstrations de la correction sémantique de cette logique de séparation, l'une reposant sur une propriété de non-déterminisme de l'allocation mémoire ; l'autre, sur une quantification sur tous les encadrements possibles.

Xavier LeroyCollège de FranceScience du logicielAnnée 2020-2021Logiques de programmes : quand la machine raisonne sur ses logicielsLe deuxième cours a été consacré à l'étude approfondie des « logiques de Hoare », c'est-à-dire des logiques de programmes qui suivent l'approche introduite par C. A. R. Hoare en 1969. Nous avons défini une telle logique de programmes pour le langage IMP, un petit langage impératif à contrôle structuré que nous avions déjà étudié dans le cours 2019-2020 « Sémantiques mécanisées ». Nous avons ensuite développé diverses extensions de cette logique : règles de raisonnement dérivées ou admissibles, non-déterminisme, erreurs dynamiques, contrôle non structuré, etc.La suite du cours a étudié les liens entre la logique de programmes et la sémantique opérationnelle du langage IMP. Nous avons défini et démontré la correction sémantique de la logique : toutes les propriétés d'un programme dérivables par les règles de la logique sont bien vérifiées par toutes les exécutions concrètes du programme. Plusieurs techniques de démonstration ont été esquissées : inductives, co-inductives, ou encore par comptage de pas (step-indexing).La complétude est la propriété réciproque de la correction sémantique : toute propriété vraie de toutes les exécutions d'un programme peut-elle s'exprimer comme un triplet de Hoare et se dériver par règles de la logique ? Une logique complète permettrait de décider le problème de l'arrêt. La complétude absolue est donc impossible pour un langage Turing-complet. En revanche, la logique de Hoare satisfait une propriété de complétude relative montrant qu'elle est aussi expressive qu'un raisonnement direct sur les exécutions des programmes, à logique ambiante fixée.Enfin, nous avons discuté des possibilités d'automatiser une vérification déductive à base de logique de Hoare. À condition de fournir manuellement les invariants des boucles, un calcul de plus faible précondition, ou de plus forte postcondition, permet de réduire la vérification d'un programme en logique de Hoare à la vérification d'un ensemble d'implications en logique du premier ordre, tâche qui peut être confiée à des démonstrateurs automatiques ou assistés.

Xavier LeroyCollège de FranceScience du logicielAnnée 2020-2021Logiques de programmes : quand la machine raisonne sur ses logicielsLe deuxième cours a été consacré à l'étude approfondie des « logiques de Hoare », c'est-à-dire des logiques de programmes qui suivent l'approche introduite par C. A. R. Hoare en 1969. Nous avons défini une telle logique de programmes pour le langage IMP, un petit langage impératif à contrôle structuré que nous avions déjà étudié dans le cours 2019-2020 « Sémantiques mécanisées ». Nous avons ensuite développé diverses extensions de cette logique : règles de raisonnement dérivées ou admissibles, non-déterminisme, erreurs dynamiques, contrôle non structuré, etc.La suite du cours a étudié les liens entre la logique de programmes et la sémantique opérationnelle du langage IMP. Nous avons défini et démontré la correction sémantique de la logique : toutes les propriétés d'un programme dérivables par les règles de la logique sont bien vérifiées par toutes les exécutions concrètes du programme. Plusieurs techniques de démonstration ont été esquissées : inductives, co-inductives, ou encore par comptage de pas (step-indexing).La complétude est la propriété réciproque de la correction sémantique : toute propriété vraie de toutes les exécutions d'un programme peut-elle s'exprimer comme un triplet de Hoare et se dériver par règles de la logique ? Une logique complète permettrait de décider le problème de l'arrêt. La complétude absolue est donc impossible pour un langage Turing-complet. En revanche, la logique de Hoare satisfait une propriété de complétude relative montrant qu'elle est aussi expressive qu'un raisonnement direct sur les exécutions des programmes, à logique ambiante fixée.Enfin, nous avons discuté des possibilités d'automatiser une vérification déductive à base de logique de Hoare. À condition de fournir manuellement les invariants des boucles, un calcul de plus faible précondition, ou de plus forte postcondition, permet de réduire la vérification d'un programme en logique de Hoare à la vérification d'un ensemble d'implications en logique du premier ordre, tâche qui peut être confiée à des démonstrateurs automatiques ou assistés.

Xavier LeroyCollège de FranceScience du logicielAnnée 2020-2021Logiques de programmes : quand la machine raisonne sur ses logicielsRésuméComment s'assurer qu'un logiciel fait ce qu'il est censé faire ? Les méthodes classiques de vérification et de validation du logiciel, reposant sur le test, les revues et les analyses, ne suffisent pas toujours. La vérification déductive permet d'aller plus loin en établissant des propriétés vraies de toutes les exécutions possibles d'un programme, via des raisonnements formels au sein d'une logique appropriée : une logique de programmes. Le premier cours a illustré cette approche par la vérification déductive d'une fonction de recherche dichotomique dans un tableau trié, un algorithme très utilisé et souvent implémenté de manière incorrecte.Ensuite, le cours a retracé l'émergence de la vérification déductive et des logiques de programmes via trois publications fondatrices. La brève communication d'Alan Turing en 1949, intitulée « Checking a large routine », introduit deux idées majeures : les assertions logiques et les ordres de terminaison, et les illustre sur la vérification d'un petit programme exprimé par un organigramme. Trop en avance sur son temps, et jamais publié formellement, ce texte précurseur tombe dans l'oubli jusqu'en 1984.L'article de Robert W. Floyd de 1967, « Assigning meanings to programs », réinvente l'approche de Turing et l'approfondit considérablement, avec une formalisation complète des conditions de vérification qui garantissent qu'un programme est correctement annoté, et l'observation, révolutionnaire pour l'époque, qu'une telle formalisation constitue une sémantique formelle du langage de programmation utilisé.Enfin, l'article de C. A. R. Hoare de 1969, intitulé « An axiomatic basis for computer programming », constitue le manifeste de la vérification déductive moderne. L'article étend les résultats de Floyd à un langage à contrôle structuré (séquences, conditionnelles, boucles) et introduit des notations toujours utilisées aujourd'hui (les « triplets de Hoare »). Mais, au-delà des contributions techniques, cet article est visionnaire tant par son approche purement axiomatique de la vérification déductive que par son analyse lucide de l'intérêt pratique de cette approche.

Xavier LeroyCollège de FranceScience du logicielAnnée 2020-2021Logiques de programmes : quand la machine raisonne sur ses logicielsRésuméComment s'assurer qu'un logiciel fait ce qu'il est censé faire ? Les méthodes classiques de vérification et de validation du logiciel, reposant sur le test, les revues et les analyses, ne suffisent pas toujours. La vérification déductive permet d'aller plus loin en établissant des propriétés vraies de toutes les exécutions possibles d'un programme, via des raisonnements formels au sein d'une logique appropriée : une logique de programmes. Le premier cours a illustré cette approche par la vérification déductive d'une fonction de recherche dichotomique dans un tableau trié, un algorithme très utilisé et souvent implémenté de manière incorrecte.Ensuite, le cours a retracé l'émergence de la vérification déductive et des logiques de programmes via trois publications fondatrices. La brève communication d'Alan Turing en 1949, intitulée « Checking a large routine », introduit deux idées majeures : les assertions logiques et les ordres de terminaison, et les illustre sur la vérification d'un petit programme exprimé par un organigramme. Trop en avance sur son temps, et jamais publié formellement, ce texte précurseur tombe dans l'oubli jusqu'en 1984.L'article de Robert W. Floyd de 1967, « Assigning meanings to programs », réinvente l'approche de Turing et l'approfondit considérablement, avec une formalisation complète des conditions de vérification qui garantissent qu'un programme est correctement annoté, et l'observation, révolutionnaire pour l'époque, qu'une telle formalisation constitue une sémantique formelle du langage de programmation utilisé.Enfin, l'article de C. A. R. Hoare de 1969, intitulé « An axiomatic basis for computer programming », constitue le manifeste de la vérification déductive moderne. L'article étend les résultats de Floyd à un langage à contrôle structuré (séquences, conditionnelles, boucles) et introduit des notations toujours utilisées aujourd'hui (les « triplets de Hoare »). Mais, au-delà des contributions techniques, cet article est visionnaire tant par son approche purement axiomatique de la vérification déductive que par son analyse lucide de l'intérêt pratique de cette approche.

Xavier LeroyCollège de FranceScience du logicielAnnée 2019-2020Sémantiques mécanisées : quand la machine raisonne sur ses langages

Xavier LeroyCollège de FranceScience du logicielAnnée 2019-2020Sémantiques mécanisées : quand la machine raisonne sur ses langages

Xavier LeroyCollège de FranceScience du logicielAnnée 2019-2020Sémantiques mécanisées : quand la machine raisonne sur ses langages

Xavier LeroyCollège de FranceScience du logicielAnnée 2019-2020Sémantiques mécanisées : quand la machine raisonne sur ses langages

Xavier LeroyCollège de FranceScience du logicielAnnée 2019-2020Sémantiques mécanisées : quand la machine raisonne sur ses langages

Xavier LeroyCollège de FranceScience du logicielAnnée 2019-2020Sémantiques mécanisées : quand la machine raisonne sur ses langages

Xavier LeroyCollège de FranceScience du logicielAnnée 2019-2020Sémantiques mécanisées : quand la machine raisonne sur ses langages

Xavier LeroyCollège de FranceScience du logicielAnnée 2019-2020Sémantiques mécanisées : quand la machine raisonne sur ses langages

Xavier LeroyCollège de FranceScience du logicielAnnée 2019-2020Sémantiques mécanisées : quand la machine raisonne sur ses langages

Xavier LeroyCollège de FranceScience du logicielAnnée 2019-2020Sémantiques mécanisées : quand la machine raisonne sur ses langages

Xavier LeroyCollège de FranceScience du logicielAnnée 2019-2020Sémantiques mécanisées : quand la machine raisonne sur ses langages

Xavier LeroyCollège de FranceScience du logicielAnnée 2019-2020Sémantiques mécanisées : quand la machine raisonne sur ses langages

Xavier LeroyCollège de FranceScience du logicielAnnée 2019-2020Sémantiques mécanisées : quand la machine raisonne sur ses langages

Xavier LeroyCollège de FranceScience du logicielAnnée 2019-2020Sémantiques mécanisées : quand la machine raisonne sur ses langages

Xavier LeroyCollège de FranceScience du logicielAnnée 2019-2020Sémantiques mécanisées : quand la machine raisonne sur ses langages

Xavier LeroyCollège de FranceScience du logicielAnnée 2019-2020Sémantiques mécanisées : quand la machine raisonne sur ses langages

Xavier LeroyCollège de FranceScience du logicielAnnée 2019-2020Sémantiques mécanisées : quand la machine raisonne sur ses langages

Xavier LeroyCollège de FranceScience du logicielAnnée 2019-2020Sémantiques mécanisées : quand la machine raisonne sur ses langages

Xavier LeroyCollège de FranceScience du logicielAnnée 2019-2020Sémantiques mécanisées : quand la machine raisonne sur ses langages

Xavier LeroyCollège de FranceScience du logicielAnnée 2019-2020Sémantiques mécanisées : quand la machine raisonne sur ses langages

Xavier LeroyCollège de FranceScience du logicielAnnée 2019-2020Sémantiques mécanisées : quand la machine raisonne sur ses langages

Xavier LeroyCollège de FranceScience du logicielAnnée 2019-2020Sémantiques mécanisées : quand la machine raisonne sur ses langages

Xavier LeroyCollège de FranceScience du logicielAnnée 2019-2020Sémantiques mécanisées : quand la machine raisonne sur ses langages

Xavier LeroyCollège de FranceScience du logicielAnnée 2019-2020Sémantiques mécanisées : quand la machine raisonne sur ses langages

Xavier LeroyCollège de FranceScience du logicielAnnée 2018-2019Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui

Xavier LeroyCollège de FranceScience du logicielAnnée 2018-2019Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui

Xavier LeroyCollège de FranceScience du logicielAnnée 2018-2019Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui

Xavier LeroyCollège de FranceScience du logicielAnnée 2018-2019Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui

Xavier LeroyCollège de FranceScience du logicielAnnée 2018-2019Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui

Xavier LeroyCollège de FranceScience du logicielAnnée 2018-2019Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui

Xavier LeroyCollège de FranceScience du logicielAnnée 2018-2019Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui

Xavier LeroyCollège de FranceScience du logicielAnnée 2018-2019Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui

Xavier LeroyCollège de FranceScience du logicielAnnée 2018-2019Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui

Xavier LeroyCollège de FranceScience du logicielAnnée 2018-2019Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui

Xavier LeroyCollège de FranceScience du logicielAnnée 2018-2019Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui

Xavier LeroyCollège de FranceScience du logicielAnnée 2018-2019Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui

Xavier LeroyCollège de FranceScience du logicielAnnée 2018-2019Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui

Xavier LeroyCollège de FranceScience du logicielAnnée 2018-2019Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui

Xavier LeroyCollège de FranceScience du logicielAnnée 2018-2019Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui

Xavier LeroyCollège de FranceScience du logicielAnnée 2018-2019Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui

Xavier LeroyCollège de FranceScience du logicielAnnée 2018-2019Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui

Xavier LeroyCollège de FranceScience du logicielAnnée 2018-2019Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui

Xavier LeroyCollège de FranceScience du logicielAnnée 2018-2019Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui

Xavier LeroyCollège de FranceScience du logicielAnnée 2018-2019Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui

Xavier LeroyCollège de FranceScience du logicielAnnée 2018-2019Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui

Xavier LeroyCollège de FranceScience du logicielAnnée 2018-2019Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui

Xavier LeroyCollège de FranceScience du logicielAnnée 2018-2019Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui

Xavier LeroyCollège de FranceScience du logicielAnnée 2018-2019Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui

Xavier LeroyCollège de FranceScience du logicielAnnée 2018-2019Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui

Xavier LeroyCollège de FranceScience du logicielAnnée 2018-2019Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui

Xavier LeroyCollège de FranceScience du logicielAnnée 2018-2019Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui

Xavier LeroyCollège de FranceScience du logicielAnnée 2018-2019Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui

Xavier LeroyCollège de FranceScience du logicielAnnée 2018-2019Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui

Xavier LeroyCollège de FranceScience du logicielAnnée 2018-2019Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui

Xavier LeroyCollège de FranceScience du logicielAnnée 2018-2019Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui

Xavier LeroyCollège de FranceScience du logicielAnnée 2018-2019Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui

Xavier LeroyCollège de FranceScience du logicielAnnée 2018-2019Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui

Xavier LeroyCollège de FranceScience du logicielAnnée 2018-2019Leçon inaugurale : Le logiciel, entre l'esprit et la matière.Les travaux de recherche de Xavier LEROY portent d'une part sur les nouveaux langages et outils de programmation, et d'autre part sur la vérification formelle de logiciels critiques afin de garantir leur sûreté et leur sécurité. Il est l'architecte et l'un des principaux développeurs du langage de programmation fonctionnelle OCaml ainsi que du compilateur C formellement vérifié CompCert, deux grands logiciels issus de la recherche.Langages fonctionnels, systèmes de types et mise en pratique : les langages Caml Light et OCamlXavier LEROY a été formé aux mathématiques et à l'informatique à l'École normale supérieure, puis à l'INRIA où il a effectué sa thèse. Programmeur prodige, il s'est illustré par une série de travaux de premier plan sur les systèmes de types et les systèmes de modules pour les langages fonctionnels, qui ont abouti au développement de Caml Light, devenu aujourd'hui OCaml, l'un des deux langages fonctionnels typés les plus utilisés au monde, dans des domaines aussi divers que l'aéronautique, la finance ou encore le Web. Ce langage est le support de développement d'outils logiciels très variés comme l'assistant de preuve Coq, les analyseurs statiques Astrée et Frama-C, le compilateur SCADE 6 d'Estérel Technologies et la blockchain Tezos. OCaml a été utilisé dans de nombreux projets emblématiques comme la version web de Facebook Messenger, le logiciel MediaWiki ou encore l'infrastructure de virtualisation Docker.Preuve de programme, preuve de compilateurs et mise en pratique : le compilateur CompCert Xavier LEROY est également à l'origine de CompCert, qui est un compilateur C certifié, écrit et vérifié grâce à l'assistant de preuve Coq. Il s'agit d'une première mondiale à plusieurs titres : il autorise une vérification formelle d'une taille et d'une complexité sans précédent, et surtout, il offre la possibilité de disposer d'un compilateur certifié, étape clé dans la certification et la vérification automatique des chaînes logicielles, et donc vers la programmation « zéro défaut ». Ce fait d'arme a eu un impact considérable sur la nature même des grands programmes de recherche sur les logiciels. Nommé professeur au Collège de France, Xavier LEROY occupera la chaire Sciences du logiciel où il dispensera dès l'année académique 2018-2019 une série de cours intitulée Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui.Leçon inaugurale jeudi 15 novembre 2018 à 18h00

Xavier LeroyCollège de FranceScience du logicielAnnée 2018-2019Leçon inaugurale : Le logiciel, entre l'esprit et la matière.Les travaux de recherche de Xavier LEROY portent d'une part sur les nouveaux langages et outils de programmation, et d'autre part sur la vérification formelle de logiciels critiques afin de garantir leur sûreté et leur sécurité. Il est l'architecte et l'un des principaux développeurs du langage de programmation fonctionnelle OCaml ainsi que du compilateur C formellement vérifié CompCert, deux grands logiciels issus de la recherche.Langages fonctionnels, systèmes de types et mise en pratique : les langages Caml Light et OCamlXavier LEROY a été formé aux mathématiques et à l'informatique à l'École normale supérieure, puis à l'INRIA où il a effectué sa thèse. Programmeur prodige, il s'est illustré par une série de travaux de premier plan sur les systèmes de types et les systèmes de modules pour les langages fonctionnels, qui ont abouti au développement de Caml Light, devenu aujourd'hui OCaml, l'un des deux langages fonctionnels typés les plus utilisés au monde, dans des domaines aussi divers que l'aéronautique, la finance ou encore le Web. Ce langage est le support de développement d'outils logiciels très variés comme l'assistant de preuve Coq, les analyseurs statiques Astrée et Frama-C, le compilateur SCADE 6 d'Estérel Technologies et la blockchain Tezos. OCaml a été utilisé dans de nombreux projets emblématiques comme la version web de Facebook Messenger, le logiciel MediaWiki ou encore l'infrastructure de virtualisation Docker.Preuve de programme, preuve de compilateurs et mise en pratique : le compilateur CompCert Xavier LEROY est également à l'origine de CompCert, qui est un compilateur C certifié, écrit et vérifié grâce à l'assistant de preuve Coq. Il s'agit d'une première mondiale à plusieurs titres : il autorise une vérification formelle d'une taille et d'une complexité sans précédent, et surtout, il offre la possibilité de disposer d'un compilateur certifié, étape clé dans la certification et la vérification automatique des chaînes logicielles, et donc vers la programmation « zéro défaut ». Ce fait d'arme a eu un impact considérable sur la nature même des grands programmes de recherche sur les logiciels. Nommé professeur au Collège de France, Xavier LEROY occupera la chaire Sciences du logiciel où il dispensera dès l'année académique 2018-2019 une série de cours intitulée Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui.Leçon inaugurale jeudi 15 novembre 2018 à 18h00

Xavier LeroyCollège de FranceScience du logicielAnnée 2018-2019Leçon inaugurale : Le logiciel, entre l'esprit et la matière.Les travaux de recherche de Xavier LEROY portent d'une part sur les nouveaux langages et outils de programmation, et d'autre part sur la vérification formelle de logiciels critiques afin de garantir leur sûreté et leur sécurité. Il est l'architecte et l'un des principaux développeurs du langage de programmation fonctionnelle OCaml ainsi que du compilateur C formellement vérifié CompCert, deux grands logiciels issus de la recherche.Langages fonctionnels, systèmes de types et mise en pratique : les langages Caml Light et OCamlXavier LEROY a été formé aux mathématiques et à l'informatique à l'École normale supérieure, puis à l'INRIA où il a effectué sa thèse. Programmeur prodige, il s'est illustré par une série de travaux de premier plan sur les systèmes de types et les systèmes de modules pour les langages fonctionnels, qui ont abouti au développement de Caml Light, devenu aujourd'hui OCaml, l'un des deux langages fonctionnels typés les plus utilisés au monde, dans des domaines aussi divers que l'aéronautique, la finance ou encore le Web. Ce langage est le support de développement d'outils logiciels très variés comme l'assistant de preuve Coq, les analyseurs statiques Astrée et Frama-C, le compilateur SCADE 6 d'Estérel Technologies et la blockchain Tezos. OCaml a été utilisé dans de nombreux projets emblématiques comme la version web de Facebook Messenger, le logiciel MediaWiki ou encore l'infrastructure de virtualisation Docker.Preuve de programme, preuve de compilateurs et mise en pratique : le compilateur CompCert Xavier LEROY est également à l'origine de CompCert, qui est un compilateur C certifié, écrit et vérifié grâce à l'assistant de preuve Coq. Il s'agit d'une première mondiale à plusieurs titres : il autorise une vérification formelle d'une taille et d'une complexité sans précédent, et surtout, il offre la possibilité de disposer d'un compilateur certifié, étape clé dans la certification et la vérification automatique des chaînes logicielles, et donc vers la programmation « zéro défaut ». Ce fait d'arme a eu un impact considérable sur la nature même des grands programmes de recherche sur les logiciels. Nommé professeur au Collège de France, Xavier LEROY occupera la chaire Sciences du logiciel où il dispensera dès l'année académique 2018-2019 une série de cours intitulée Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui.Leçon inaugurale jeudi 15 novembre 2018 à 18h00