Sign up to save your podcasts
Or
Share Sciences du logiciel - Xavier Leroy
Share to email
Share to Facebook
Share to X
Share to email
Share to Facebook
Share to X
Or
Sciences du logiciel - Xavier Leroy
By Collège de FranceTechnology
Sciences du logiciel - Xavier Leroy episodes
- 02- Équivalences de programmes : Approches dénotationnelles et full abstraction
Xavier Leroy
Chaire Sciences du logiciel
Collège de France
Année 2026-2027
02- Équivalences de programmes : Approches dénotationnelles et full abstraction
1 hr 23 min - Séminaire - Davide Sangiorgi : Concurrency Theory: From Its Origins Towards a Science of Processes
Xavier 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 Processes
59 min - 01- Équivalences de programmes : Introduction à l'équivalence et au raffinement entre programmes
Xavier 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.
1 hr 31 min - Séminaire - David Pointcheval : Le chiffrement fonctionnel : agréger des données sensibles
Xavier 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 sensibles
1 hr 2 min - 07 - Le calcul sécurisé : calculer sur des données chiffrées ou privées : Sécuriser le calcul : nouvelles directions et conclusions
Xavier 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 conclusions
1 hr 24 min - Séminaire - Michele Orrù : Des preuves zero-knowledge à l'anonymat en ligne
Xavier 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
55 min - 06 - Le calcul sécurisé : calculer sur des données chiffrées ou privées : Calcul vérifiable et preuves zero-knowledge
Xavier Leroy
Chaire Chaire Sciences du logiciel
Collège de France
Année 2025-2026
06 - Le calcul sécurisé : calculer sur des données chiffrées ou privées : Calcul vérifiable et preuves zero-knowledge
1 hr 26 min - Séminaire - Geoffroy Couteau : Calcul sécurisé et aléa corrélé, de la théorie à la pratique
Xavier Leroy
Chaire Chaire Sciences du logiciel
Collège de France
Année 2025-2026
Geoffroy Couteau
CNRS
Séminaire - Geoffroy Couteau : Calcul sécurisé et aléa corrélé, de la théorie à la pratique
56 min - 05 - Le calcul sécurisé : calculer sur des données chiffrées ou privées : Calcul multipartite sécurisé : circuits brouillés et transfert inconscient
Xavier Leroy
Chaire Chaire Sciences du logiciel
Collège de France
Année 2025-2026
05 - Le calcul sécurisé : calculer sur des données chiffrées ou privées : Calcul multipartite sécurisé : circuits brouillés et transfert inconscient
1 hr 17 min - Séminaire - Ilaria Chillotti : Chiffrement totalement homomorphe : panorama, applications et nouvelles directions
Xavier Leroy
Chaire Sciences du logiciel
Collège de France
Année 2025-2026
Séminaire - Ilaria Chillotti : Chiffrement totalement homomorphe : panorama, applications et nouvelles directions
Ilaria Chillotti
DESILO Inc
1 hr 2 min
About Sciences du logiciel - Xavier Leroy
From the publisher's feed
É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.