60 épisodes

Écrire un petit programme informatique est facile. Concevoir et réaliser un logiciel complet qui soit fiable, pérenne et résistant aux attaques reste extraordinairement difficile. C'est le but des sciences du logiciel que de concevoir et développer les principes, les formalismes mathématiques, les techniques empiriques et les outils informatiques nécessaires pour concevoir, programmer et vérifier des logiciels fiables et sécurisés.

L'enseignement de la chaire Sciences du logiciel vise à explorer cette problématique et à présenter la recherche contemporaine dans ce domaine. Le cours privilégie les approches dites « formelles », par opposition à l'empirisme souvent de mise en génie logiciel. Ces approches s'appuient sur des fondements mathématiquement rigoureux, connus ou en émergence : sémantiques formelles, logiques de programmes, systèmes déductifs, équivalences de programmes, calculs de processus… Historiquement, ces concepts ont émergé de considérations de programmation très terre-à-terre avant de se parer de rigueur mathématique. Le cours s'efforce de retracer ce cheminement des idées en partant de l'intuition du programmeur et en allant jusqu'à la mécanisation de ces approches formelles.

Les premières années de cet enseignement auraient pu s'intituler « Programmer, démontrer », car ils ont exploré plusieurs modes d'interaction entre la programmation de logiciels et la démonstration d'énoncés mathématiques : programmer puis démontrer, comme dans les logiques de programmes pour la vérification déductive ; programmer pour démontrer, comme dans les logiques constructives et l'assistant à la démonstration Coq ; enfin, programmer égale démontrer, comme dans la féconde correspondance de Curry-Howard, objet de la première année du cours.

La recherche de la chaire Sciences du logiciel s'effectue dans le cadre de l'équipe-projet Cambium, commune avec l'Inria. Les travaux de l'équipe visent à améliorer la fiabilité, la sûreté et la sécurité du logiciel en faisant progresser les langages de programmation et les méthodes de vérification formelle de programmes. Les principaux thèmes de recherche sont les systèmes de types et les algorithmes d'inférence de types, la vérification déductive de programmes, le parallélisme à mémoire partagée, et les modèles mémoires faiblement cohérents. L'équipe conçoit et développe deux grands logiciels de recherche qui intègrent et font passer dans la pratique bon nombre de ses résultats : OCaml, un langage de programmation fonctionnel statiquement typé et son implémentation, et CompCert, un compilateur formellement vérifié pour logiciels embarqués critiques.

Sciences du logiciel - Xavier Leroy Collège de France

    • Éducation
    • 4,0 • 1 note

Écrire un petit programme informatique est facile. Concevoir et réaliser un logiciel complet qui soit fiable, pérenne et résistant aux attaques reste extraordinairement difficile. C'est le but des sciences du logiciel que de concevoir et développer les principes, les formalismes mathématiques, les techniques empiriques et les outils informatiques nécessaires pour concevoir, programmer et vérifier des logiciels fiables et sécurisés.

L'enseignement de la chaire Sciences du logiciel vise à explorer cette problématique et à présenter la recherche contemporaine dans ce domaine. Le cours privilégie les approches dites « formelles », par opposition à l'empirisme souvent de mise en génie logiciel. Ces approches s'appuient sur des fondements mathématiquement rigoureux, connus ou en émergence : sémantiques formelles, logiques de programmes, systèmes déductifs, équivalences de programmes, calculs de processus… Historiquement, ces concepts ont émergé de considérations de programmation très terre-à-terre avant de se parer de rigueur mathématique. Le cours s'efforce de retracer ce cheminement des idées en partant de l'intuition du programmeur et en allant jusqu'à la mécanisation de ces approches formelles.

Les premières années de cet enseignement auraient pu s'intituler « Programmer, démontrer », car ils ont exploré plusieurs modes d'interaction entre la programmation de logiciels et la démonstration d'énoncés mathématiques : programmer puis démontrer, comme dans les logiques de programmes pour la vérification déductive ; programmer pour démontrer, comme dans les logiques constructives et l'assistant à la démonstration Coq ; enfin, programmer égale démontrer, comme dans la féconde correspondance de Curry-Howard, objet de la première année du cours.

La recherche de la chaire Sciences du logiciel s'effectue dans le cadre de l'équipe-projet Cambium, commune avec l'Inria. Les travaux de l'équipe visent à améliorer la fiabilité, la sûreté et la sécurité du logiciel en faisant progresser les langages de programmation et les méthodes de vérification formelle de programmes. Les principaux thèmes de recherche sont les systèmes de types et les algorithmes d'inférence de types, la vérification déductive de programmes, le parallélisme à mémoire partagée, et les modèles mémoires faiblement cohérents. L'équipe conçoit et développe deux grands logiciels de recherche qui intègrent et font passer dans la pratique bon nombre de ses résultats : OCaml, un langage de programmation fonctionnel statiquement typé et son implémentation, et CompCert, un compilateur formellement vérifié pour logiciels embarqués critiques.

    Séminaire - Daan Leijen : Design and Compilation of Efficient Effect Handlers in the Koka Language

    Séminaire - Daan Leijen : Design and Compilation of Efficient Effect Handlers in the Koka Language

    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

    • 55 min
    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

    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

    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

    • 1h 22 min
    Séminaire - Matija Pretnar : Effect handlers and mathematically inspired language constructs

    Séminaire - Matija Pretnar : Effect handlers and mathematically inspired language constructs

    Xavier Leroy
    Collège de France
    Science du logiciel
    Année 2023-2024

    Séminaire - Matija Pretnar : Effect handlers and mathematically inspired language constructs

    Matija Pretnar
    Université de Ljubljana

    • 1h 3 min
    07 - Structures de contrôle : de « goto » aux effets algébriques : Typage et analyse statique des effets

    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

    07 - Structures de contrôle : de « goto » aux effets algébriques : Typage et analyse statique des effets

    • 1h 19 min
    Séminaire - Olivier Danvy : Les continuations : cinq minutes pour les apprendre, toute une vie pour les comprendre

    Séminaire - Olivier Danvy : Les continuations : cinq minutes pour les apprendre, toute une vie pour les comprendre

    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

    • 58 min
    06 - Structures de contrôle : de « goto » aux effets algébriques : Théorie des effets : des monades aux effets algébriques

    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

    06 - Structures de contrôle : de « goto » aux effets algébriques : Théorie des effets : des monades aux effets algébriques

    • 1h 16 min

Avis

4,0 sur 5
1 note

1 note

Classement des podcasts dans Éducation

"Comment tu fais ?" by Laury Thilleman
Laury Thilleman
Paroles Paroles
aura
La vie suffit !
Chloé Bloom
Ces questions que tout le monde se pose
Maud Ankaoua
T'as qui en Histoire ?
Stéphane Genêt
Allez j'ose !
Martange