Écoutez gratuitement ce podcast dans l'application :
Télécharger gratuitement dans l'App Store
radio.fr
Minuteur
Sauvegarde des favoris
75 épisodes
Séminaire - Davide Sangiorgi : Concurrency Theory: From Its Origins Towards a Science of Processes
05/11/2026 | 58 minXavier Leroy
Chaire Chaire Sciences du logiciel
Collège de France
Année 2026-2027
Davide Sangiorgi
Université de Bologne
Séminaire - Davide Sangiorgi : Concurrency Theory: From Its Origins Towards a Science of Processes01- Équivalences de programmes : Introduction à l'équivalence et au raffinement entre programmes
05/11/2026 | 1 h 30 minXavier Leroy
Chaire Sciences du logiciel
Année 2026-2027
Collège de France
01- Équivalences de programmes : Introduction à l'équivalence et au raffinement entre programmes
Résumé
Lors d'un développement logiciel, il est fréquent de devoir comparer les comportements de plusieurs versions du même fragment de programme afin de s'assurer qu'il n'y a pas de régression. Nous avons présenté deux exemples : l'optimisation (amélioration des performances) par réécriture progressive du code source, et la méthodologie de développement par raffinements successifs d'une spécification. Nous avons ensuite défini informellement les notions d'équivalence et de raffinement entre programmes, qui correspondent respectivement à l'égalité et à l'inclusion des ensembles de comportements observables. Ces notions sont faciles à caractériser pour des langages simples comme les expressions arithmétiques, mais deviennent de plus en plus délicates lorsqu'on ajoute des traits au langage comme les fonctions, l'évaluation paresseuse, l'ordre supérieur, le non-déterminisme, l'abstraction de types, ainsi que les fonctions et objets avec état mutable interne.
Nous avons ensuite défini l'équivalence observationnelle, aussi appelée équivalence contextuelle de Morris, en faisant une analogie avec les jeux de tests exhaustifs. En raison de sa définition très générale et de ses bonnes propriétés mathématiques, cette équivalence est considérée comme « l'étalon-or » des équivalences de programmes. Cependant, elle est très difficile à démontrer directement, ce qui explique pourquoi d'autres techniques de preuve d'équivalence ou de raffinement sont nécessaires. Nous en avons mentionné quatre : les sémantiques dénotationnelles, les bisimulations, les relations logiques et les logiques relationnelles, qui seront étudiées dans les séances suivantes du cours.Séminaire - David Pointcheval : Le chiffrement fonctionnel : agréger des données sensibles
18/12/2025 | 1 h 1 minXavier Leroy
Chaire Chaire Sciences du logiciel
Collège de France
Année 2025-2026
David Pointcheval
Cosmian
Séminaire - David Pointcheval : Le chiffrement fonctionnel : agréger des données sensibles07 - Le calcul sécurisé : calculer sur des données chiffrées ou privées : Sécuriser le calcul : nouvelles directions et conclusions
18/12/2025 | 1 h 23 minXavier Leroy
Chaire Chaire Sciences du logiciel
Collège de France
Année 2025-2026
07 - Le calcul sécurisé : calculer sur des données chiffrées ou privées : Sécuriser le calcul : nouvelles directions et conclusionsSéminaire - Michele Orrù : Des preuves zero-knowledge à l'anonymat en ligne
11/12/2025 | 55 minXavier Leroy
Chaire Chaire Sciences du logiciel
Collège de France
Michele Orrù
CNRS
Séminaire - Michele Orrù : Des preuves zero-knowledge à l'anonymat en ligne
Plus de podcasts Technologies
Podcasts tendance de Technologies
À propos de Sciences du logiciel - Xavier Leroy
É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.
Site web du podcastÉcoutez Sciences du logiciel - Xavier Leroy, Sortie de veille ou d'autres podcasts du monde entier - avec l'app de radio.fr
Obtenez l’app radio.fr gratuite
- Ajout de radios et podcasts en favoris
- Diffusion via Wi-Fi ou Bluetooth
- Carplay & Android Auto compatibles
- Et encore plus de fonctionnalités
Obtenez l’app radio.fr gratuite
- Ajout de radios et podcasts en favoris
- Diffusion via Wi-Fi ou Bluetooth
- Carplay & Android Auto compatibles
- Et encore plus de fonctionnalités
Sciences du logiciel - Xavier Leroy
Scannez le code,
Téléchargez l’app,
Écoutez.
Téléchargez l’app,
Écoutez.
Sciences du logiciel - Xavier Leroy: Podcasts du groupe
France
