Navigation – Plan du site

AccueilVolumes119Cours et recherches des professeursI. Sciences mathématiques, physiq...Mathématiques et sciences informa...Sciences du logiciel

Cours et recherches des professeurs
I. Sciences mathématiques, physiques et naturelles
Mathématiques et sciences informatiques

Sciences du logiciel

Xavier Leroy
p. 21-33

Plan

Haut de page

Notes de la rédaction

La série de cours et de séminaires « Programmer = démontrer ? La correspondance de Curry-Howard aujourd’hui » est disponible en audio et vidéo, sur le site internet du Collège de France (https://www.college-de-france.fr/site/xavier-leroy/course-2018-2019.htm), ainsi que la leçon inaugurale « Le logiciel, entre l’esprit et la matière » (https://www.college-de-france.fr/site/xavier-leroy/inaugural-lecture-2018-2019.htm). Celle-ci a également fait l’objet d’une publication : X. Leroy, Le Logiciel, entre l’esprit et la matière, Paris, Collège de France/Fayard, coll. « Leçons inaugurales du Collège de France », vol. 284, 2019 ; édition numérique : Collège de France, 2019, https://doi.org/10.4000/books.cdf.7671, http://books.openedition.org/cdf/7671

Texte intégral

Enseignement

Leçon inaugurale – Le logiciel, entre l’esprit et la matière

1La leçon inaugurale a rappelé à quel point l’informatique trouve ses racines dans la logique mathématique. Comme Leibniz avec son calculus ratiocinator, de nombreux logiciens ont cherché dans le calcul une source de vérités absolues. C’est en travaillant sur le programme de Hilbert, une tentative ambitieuse de refondation des mathématiques, que Church en 1936 et Turing en 1937 ont créé la théorie de la calculabilité. La machine de Turing et le lambda-calcul de Church, apparus à cette occasion, sont les grands ancêtres des microprocesseurs et des langages de programmation contemporains.

2L’informatique n’est pas uniquement l’étude de ce qui est calculable : c’est l’étude de ce qui est calculable de manière efficace et effective. D’un côté, l’algorithmique conçoit les algorithmes efficaces et étudie leurs performances ; de l’autre, les sciences du logiciel construisent le chemin qui va des algorithmes abstraits à leur exécution effective et correcte par la machine. Cela passe notamment par des langages et outils de programmation qui, des langages d’assemblage de 1950 aux langages fonctionnels contemporains, ont fait d’immenses progrès.

3Alors que nous confions de plus en plus de responsabilités aux ordinateurs, le problème principal n’est plus de développer le logiciel, mais de le vérifier. Comment s’assurer de sa justesse et de son innocuité ? Les méthodes empiriques à base de tests atteignent leurs limites et se complètent de méthodes formelles, où le programme est vu comme une définition mathématique, et sa vérification comme la démonstration, automatisée ou assistée par l’ordinateur, des propriétés attendues du programme. Introduites à la fin des années 1960, les méthodes formelles atteignent aujourd’hui une maturité telle que la vérification de langages et d’outils de programmation comme les compilateurs est possible.

4Finalement, le logiciel ne serait-il que de la logique qui s’exécute sur l’ordinateur de manière algorithmiquement efficace ? Souhaitons-le, tant cette rigueur formelle est nécessaire pour faire confiance au logiciel aujourd’hui omniprésent.

Cours – Programmer = démontrer ? La correspondance de Curry-Howard aujourd’hui

5La leçon inaugurale a rappelé les liens historiques entre logique et informatique. Le cours 2018-2019 de la chaire Sciences du logiciel étudié un autre lien, de nature mathématique celui-là (il s’agit d’un isomorphisme), entre langages de programmation et logiques mathématiques. Dans cette approche, démontrer un théorème, c’est la même chose que d’écrire un programme ; énoncer le théorème, c’est la même chose que de spécifier le type du programme.

6Cette correspondance entre démonstration et programmation a d’abord été observée dans un cas simple par deux logiciens : Curry en 1958, puis Howard en 1969. Le résultat semblait tellement anecdotique que Howard ne l’a jamais soumis à une revue, se contentant de faire circuler des photocopies de ses notes manuscrites. Rarement photocopie a eu un tel impact scientifique, tant cette correspondance de Curry-Howard est entrée en résonance avec le renouveau de la logique et l’explosion de l’informatique théorique des années 1970 pour s’imposer dès 1980 comme un lien structurel profond entre langages et logiques, entre programmation et démonstration.

7Aujourd’hui, il est naturel de se demander quelle est la « signification logique » de tel ou tel trait de langage de programmation, ou encore quel est le « contenu calculatoire » de tel ou tel théorème mathématique (c’est-à-dire, quels algorithmes se cachent dans sa démonstration ?). Plus important encore, la correspondance de Curry-Howard a débouché sur des outils informatiques comme Coq et Agda, qui sont à la fois des langages de programmation et des logiques mathématiques, et s’utilisent aussi bien pour écrire et vérifier des programmes que pour énoncer et aider à démontrer des théories mathématiques.

8Le cours a retracé ce bouillonnement d’idées à la frontière entre logique et informatique, et mis l’accent sur les résultats récents et les problèmes ouverts dans ce domaine. Le séminaire a donné la parole à sept experts du domaine pour des approfondissements et des points de vue complémentaires.

Cours 1 – Les chemins d’une découverte : la correspondance de Curry-Howard, 1930-1970

9Le premier cours a retracé les trois chemins qui mènent à la découverte de Curry et Howard : le lambda-calcul, la logique intuitionniste, et les systèmes de types simples.

10Vers 1930, Church introduit la lambda-notation λx.e pour désigner la fonction qui à x associe e, et l’utilise pour unifier diverses notations mathématiques faisant intervenir des variables liées (sommes, limites, quantificateurs, etc.). Son premier lambda-calcul, publié en 1932 et 1933, est une logique mathématique qui utilise la lambda-notation pour représenter les ensembles. Cette logique est rapidement abandonnée car incohérente. En revanche, débarrassé de ses connecteurs logiques, le lambda-calcul pur s’impose dès 1936 comme un formalisme fondamental de la calculabilité, en équivalence avec les machines de Turing, puis, dès le langage Lisp (1960), comme noyau des langages fonctionnels de programmation.

11La logique intuitionniste, introduite par Glivenko et Heyting vers 1928, formalise la notion de démonstration constructive, qui est un aspect important de l’intuitionnisme, la philosophie des mathématiques fondée par Brouwer. Suivant l’interprétation BHK (Brouwer, Heyting, Kolmogorov) de l’intuitionnisme, les seules propositions vraies en logique intuitionniste sont celles qui sont justifiées par une construction, c’est à dire un objet mathématique qui atteste de leur véracité. Ainsi, une construction de ∃x.P est une paire d’une valeur pour x et d’une construction de P(x). Les démonstrations non constructives de ∃x.P sont donc exclues.

12Les types sont présents dans de nombreux langages de programmation pour détecter des erreurs de programmation et clarifier le sens des programmes. En logique, ils apparaissent dès 1908 dans les travaux de Russell pour rejeter des termes absurdes comme x ∉ x (« x n’appartient pas à lui-même ») et les paradoxes qui en découlent. Partant de la théorie des types de Russell, plusieurs simplifications débouchent sur le lambda-calcul simplement typé publié par Church en 1940.

13Tout est en place pour qu’entrent en résonance lambda-calcul typé et logique intuitionniste. Une première observation, due à Curry en 1958, est que si on lit les types de fonctions τ → σ comme l’implication P ⇒ Q des propositions, la règle de typage de l’application est la règle de déduction modus ponens, et les types des combinateurs S, K, I du lambda-calcul sont les axiomes définissant l’implication dans une logique à la Hilbert. Mais il faut attendre 1969 pour que Howard construise la correspondance complète entre lambda-calcul typé et logique intuitionniste. Non seulement les types correspondent aux propositions et les termes aux constructions (au sens BHK), mais encore l’évaluation des termes par beta-réductions correspond à l’élimination des coupures dans les démonstrations, du moins pour le fragment implicatif.

Cours 2 – Polymorphisme à tous les étages ! Du système F au calcul des constructions

14La correspondance de Curry-Howard n’est-elle qu’une agréable coïncidence entre une logique intuitionniste et un lambda-calcul typé tous deux peu expressifs ? De nombreuses extensions qui apparaissent dans les années 1970 et 1980 montrent que ce n’est pas le cas.

15Le typage polymorphe est la première de ces extensions. Il apparaît indépendamment dans les travaux de Girard (1971) et de Reynolds (1974). Reynolds est un informaticien et cherche à assouplir le typage du lambda-calcul de manière à pouvoir typer des fonctions génériques comme le tri, qui appliquent un même algorithme à des données de différents types. Girard est un logicien qui cherche une interprétation fonctionnelle (comme l’interprétation BHK) pour l’arithmétique du second ordre, une logique suffisamment puissante pour exprimer l’analyse. Ils convergent sur le même système de types, appelé lambda-calcul polymorphe par Reynolds et système F par Girard, qui se révèle extrêmement expressif.

16D’autres formes de polymorphisme apparaissent ensuite : les constructeurs de types (types paramétrés par des types) et les types dépendants (types paramétrés par des termes). Ces formes de paramétrisation s’ajoutent à celles du lambda-calcul (termes paramétrés par des termes) et de système F (termes paramétrés par des types), débouchant sur des formalismes inutilement complexes.

17Une « grande unification » apparaît dès le début des années 1970 avec la théorie intuitionniste des types de Martin-Löf, suivie en 1986 par le calcul des constructions de Coquand et Huet, puis en 1988 par les Pure Type Systems de Berardi. Les types et les termes partagent la même syntaxe ; un seul lambda et une seule application traitent toutes les formes de paramétrisation. Cependant, identifier entièrement types et termes via un type de tous les types, comme dans une première version de la théorie des types de Martin-Löf, mène à l’incohérence logique. Il reste nécessaire de stratifier types et termes, ce qui se fait à l’aide d’univers. De nombreux systèmes de types intéressants s’obtiennent en variant le nombre et les relations entre univers.

18En l’espace de vingt ans, la correspondance de Curry-Howard s’est non seulement étendue à des logiques et des langages typés très expressifs, mais encore a inspiré des systèmes formels utilisables à la fois comme logiques et comme langages de programmation, tels la théorie des types de Martin-Löf et le calcul des constructions.

Cours 3 – Des armes de construction massive : types algébriques, prédicats inductifs, GADT

19Le cours a débuté par un historique des types de données dans les langages de programmation : tableaux en Fortran, enregistrements (records) en Cobol, unions disjointes en Algol 68, références et pointeurs en Algol W, ainsi que les types universels des S-expressions en Lisp et des termes en Prolog. Les types algébriques, introduits dans le langage HOPE et popularisés par ML et Haskell, unifient toutes ces notions. Les types algébriques sont des sommes de produits, récursives et nommées. Ils peuvent exprimer de nombreuses structures de données informatiques, ainsi que la conjonction et la disjonction dans une approche de Curry-Howard.

20Les lambda-calculs étudiés dans les cours précédents ne fournissent pas de types de données, car ils peuvent être définis en termes de fonctions, généralisant l’astucieux codage fonctionnel des nombres entiers introduit par Church. Ce codage est bien typé dans les systèmes F et Fω, mais avec des restrictions sur les analyses de cas que l’on peut faire sur les données. Ainsi, on ne peut pas démontrer 0 ≠ 1 avec le codage de Church typé !

21Pour dépasser ces restrictions, Paulin-Mohring et Pfenning introduisent en 1989 les types inductifs, une variante des types algébriques compatibles avec la théorie des types. En moins, la récursion est restreinte et une condition de positivité est ajoutée afin de préserver la normalisation forte et la cohérence logique. En plus, les types inductifs peuvent être dépendants. Par la correspondance de Curry-Howard, ils deviennent des prédicats inductifs, avec lesquels on peut définir les connecteurs logiques « et », « ou », « il existe ». Une extension naturelle, les familles inductives, permet d’exprimer tous les prédicats définissables par règles d’inférence, y compris l’égalité et les ordres bien fondés.

22Le cheminement des idées continue : des types algébriques en programmation vers les types et familles inductifs en logique, puis retour en programmation avec les types algébriques généralisés, Generalized Algebraic Data Types (GADT). Imaginés par Augustsson et Petersson en 1994, puis intégrés dans Haskell en 2007 et OCaml en 2012, les GADT sont une extension des types algébriques permettant d’exprimer certaines propriétés des données dans le style des prédicats inductifs, incluant des égalités entre types et des quantificateurs existentiels, sans pour autant nécessiter toute la mécanique des types dépendants.

23La recherche autour des types inductifs reste active : quelles sont les bonnes conditions de garde qui garantissent la normalisation ? Peut-on identifier des valeurs d’un type inductif, réalisant ainsi le quotient de ce type par une relation d’équivalence ? Le dixième cours est revenu sur cette dernière question.

Cours 4 – Il faut qu’une porte soit ouverte ou fermée ! Logique classique, continuations, opérateurs de contrôle

[NDLR : Voir développement dans le résumé complet ci-joint en téléchargement.]

Cours 5 – Peut-on changer le monde ? Programmation impérative, effets monadiques, effets algébriques

[NDLR : Voir développement dans le résumé complet ci-joint en téléchargement.]

Cours 6 – Des théorèmes gratuits : la paramétricité

[NDLR : Voir développement dans le résumé complet ci-joint en téléchargement.]

Cours 7 – Le forcing, une transformation de programme comme une autre ?

[NDLR : Voir développement dans le résumé complet ci-joint en téléchargement.]

Cours 8 – À pas comptés : les techniques de step-indexing

[NDLR : Voir développement dans le résumé complet ci-joint en téléchargement.]

Cours 9 – Sisyphe heureux : types infinis, démonstrations par coinduction, et programmation réactive

[NDLR : Voir développement dans le résumé complet ci-joint en téléchargement.]

Cours 10 – Qu’est-ce que l’égalité ? De Leibniz à la théorie homotopique des types

[NDLR : Voir développement dans le résumé complet ci-joint en téléchargement.]

Cours 11 – Conclusion et discussions

[NDLR : Voir développement dans le résumé complet ci-joint en téléchargement.]

Séminaires : en relation avec le sujet du cours

Séminaire 1 – Les types dépendants : tout un programme !

Pierre-Évariste Dagand (CNRS, laboratoire LIP6, Paris), le 28 novembre 2018

24Le premier séminaire a consisté en une défense et illustration de la programmation avec types dépendants dans le langage Agda. Le conférencier est parti d’un problème classique : la sémantique d’un langage d’expressions arithmétiques et sa compilation vers le code d’une machine à pile. Il a montré que de nombreux cas d’erreurs sont à traiter si on n’emploie que des types simples, mais disparaissent si on indexe les expressions et les instructions de la machine par les types des valeurs produites. Cela garantit par construction que le compilateur préserve les types. Les instructions peuvent aussi être indexées par leur sémantique opérationnelle, ce qui garantit par construction que le compilateur est correct (préserve la sémantique), atteignant ainsi un point extrême de la programmation à types dépendants.

Séminaire 2 – Mathématiques assistées par ordinateur

Assia Mahboubi (Inria, équipe Gallinette, Nantes), le 5 décembre 2018

25Le deuxième séminaire a été consacré aux utilisations dans la recherche en mathématiques de l’ordinateur en général, et en particulier des assistants de preuve (Coq, HOL, Mizar, etc.). Depuis longtemps employé comme support d’expériences et aide à l’intuition, le calcul sur ordinateur peut aussi contribuer à part entière à la démonstration de grands théorèmes. L’oratrice a développé l’exemple de la démonstration par Helfgott de la conjecture faible de Goldbach, qui fait appel à des encadrements numériques d’intégrales ; elle et ses coauteurs ont pu démontrer formellement ces encadrements via une arithmétique d’intervalles vérifiée en Coq. Cependant, la formalisation « sur machine » des structures algébriques usuelles pose des problèmes subtils notamment liés à « l’ambiguïté typique » entre une structure et son ensemble support. Après les premiers succès, où l’assistance de l’ordinateur a permis d’achever des démonstrations longues (théorème des quatre couleurs, conjecture de Kepler), verrons-nous un nouveau style de mathématiques émerger de l’utilisation de ces assistants ?

Séminaire 3 – Programmer avec Coq : récursion et filtrage dépendant

Matthieu Sozeau (Inria, équipe PiR2, Paris), le 12 décembre 2018

26Le troisième séminaire a continué l’exploration de la programmation avec types dépendants débutée au premier séminaire. L’orateur a identifié deux écueils majeurs pour programmer dans une théorie des types comme celle de Coq : la partialité et la non-terminaison, et a montré comment l’utilisation de types dépendants permet de rendre les fonctions totales et d’en démontrer la terminaison. Se pose cependant le problème du filtrage dépendant, c’est-à-dire l’analyse par cas sur ces types dépendants, qui est plus complexe que le filtrage non-dépendant usuel.

Séminaire 4 – Peut-on dupliquer un objet ? Linéarité et contrôle
des ressources

Guillaume Munch-Maccagnoni (Inria, équipe Gallinette, Nantes), le 19 décembre 2018

27Au contraire de la programmation fonctionnelle pure, la programmation système doit gérer des ressources limitées par la physique de la machine : mémoire, fichiers, etc. Il faut en particulier assurer que ces ressources ne sont ni dupliquées ni perdues. Le conférencier a développé le concept de linéarité comme discipline de programmation système, mais aussi sous l’angle de la logique linéaire, en enfin sous forme de systèmes de types comme celui du langage Rust.

Séminaire 5 – Réalisabilité et forcing

Alexandre Miquel (Université de la République, Montevideo), le 16 janvier 2019

28Ce séminaire a approfondi la technique de forcing de Cohen et l’analyse de son contenu calculatoire abordées dans le septième cours. Le conférencier a ensuite expliqué la théorie de la réalisabilité, une méthode de construction de modèles de la logique formalisant et étendant l’interprétation BHK, et montré ses liens formels avec le forcing : la réalisabilité peut être vue comme un forcing non commutatif. Poursuivant cette unification, il a introduit la notion d’algèbre implicative, une structure qui représente uniformément programmes et types, réalisateurs et formules logiques.

Séminaire 6 – Sémantique des programmes fonctionnels probabilistes, à la lumière de la logique linéaire

Christine Tasson (Université Paris Diderot, laboratoire IRIF), le 23 janvier 2019

29Le sixième séminaire a étudié les langages probabilistes. Il s’agit de langages fonctionnels simples comme PCF auxquels on ajoute de l’aléatoire, par exemple une primitive qui s’évalue en 0 avec probabilité ½ et en 1 avec probabilité ½. Ces langages servent notamment à l’étude de l’inférence Bayésienne. La conférencière a développé des sémantiques dénotationnelles pour le langage PCF probabiliste utilisant des espaces cohérents probabilistes. Elle a dégagé des liens avec la logique linéaire et notamment son fragment semi-polarisé, qui correspond, au sens de Curry-Howard, au calcul call-by-push-value de Levy.

Séminaire 7 – Du calcul des constructions à la théorie des types univalents

Thierry Coquand (Université de Göteborg), le 30 janvier 2019

30Le dernier séminaire a conclu la série par une perspective personnelle sur l’histoire et l’actualité de la théorie des types. Le conférencier est revenu sur son invention avec Huet du calcul des constructions, le formalisme à la base de l’assistant de preuves Coq. Le calcul des constructions est apparu comme une synthèse entre les travaux de de Bruijn sur le système Automath pour la mécanisation des mathématiques, les travaux de Girard sur le système Fω, et les travaux de Martin-Löf sur sa théorie des types. Ces formalismes débouchent aujourd’hui sur une approche nouvelle et prometteuse de la notion mathématique d’identification entre deux collections, généralisant les notions d’isomorphismes entre structures algébriques et de transport de propriétés.

Recherche

31Je suis responsable scientifique de l’équipe-projet Inria Gallium, localisée au centre Inria de Paris. Les travaux de l’équipe visent à améliorer la fiabilité et la sécurité du logiciel au moyen de nouveaux langages de programmation, plus expressifs et plus sûrs, et de la vérification formelle de programmes et d’outils de programmation. Les principaux résultats de l’équipe pendant l’année universitaire 2018-2019 sont listés ci-dessous. Une description plus détaillée est disponible dans le rapport annuel d’activité Inria de l’équipe, https://raweb.inria.fr/​rapportsactivite/​RA2018/​gallium/​.

Vérification formelle d’algorithmes et de leur complexité

32À l’aide d’une logique de séparation étendue avec des crédits de temps, nous avons vérifié formellement la complexité de plusieurs algorithmes, dont un algorithme particulièrement complexe de détection incrémentale de cycles. Nous avons introduit la notion duale de reçus de temps afin d’établir des bornes inférieures sur les temps d’exécution, ce qui a permis de montrer par exemple l’absence de débordements arithmétiques dans l’algorithme union-find.

Vérification formelle de compilateurs et outils de programmation

33Nous avons poursuivi le développement de CompCert, le compilateur C formellement vérifié : ajout et vérification d’une passe d’optimisation de type if-conversion pour éliminer des branchements conditionnels ; introduction de nouveaux mécanismes pour spécifier les fonctions prédéfinies par le compilateur ; et poursuite de l’effort d’industrialisation en partenariat avec la société AbsInt GmbH. Plus en amont, nous explorons une nouvelle manière de formaliser la sémantique dénotationnelle d’un langage de programmation sous une forme exécutable, s’appuyant sur la monade de partialité de Capretta mentionnée dans le neuvième cours.

Programmation fonctionnelle typée en OCaml

34Nous avons poursuivi le développement du langage OCaml et de son implémentation : extensions du filtrage sur les GADT, introduction de nouveaux mécanismes de substitution dans les modules et leurs signatures, améliorations des performances du code compilé et du gestionnaire de mémoire (GC), et refonte des mécanismes d’autoconfiguration et de construction du système.

Modélisation et test de modèles mémoire faiblement cohérents

35Notre étude formelle et expérimentale des modèles mémoires fournis par les processeurs multi-cœurs contemporains se poursuit, avec notamment une étude des comportements en mémoire des codes auto-modifiants sur architecture ARM. Plus en amont, nous avons travaillé sur un nouveau formalisme pour décrire les modèles mémoire, inspiré par les sémantiques à jeux et les structures d’événements.

Publications

36Acar U., Aksenov V., Charguéraud A. et Rainey M., « Provably and practically efficient granularity control », in : PPoPP 2019: 24th ACM Symposium on Principles and Practice of Parallel Programming, New York, Association for Computing Machinery, 2019, p. 213-228, https://doi.org/​10.1145/​3293883.3295725.

Acar U., Charguéraud A., Guatto A., Rainey M. et Sieczkowski F., « Heartbeat scheduling: Provable efficiency for nested parallelism. », in : PLDI 2018: 39th ACM Conference on Programming Language Design and Implementation, New York, Association for Computing Machinery, 2018, p. 769-782.

Aksenov V., Synchronization Costs in Parallel Programs and Concurrent Data Structures, thèse de doctorat, université ITMO de Saint-Pétersbourg et université Paris Diderot, sept. 2018.

Alglave J., Maranget L., McKenney P., Parri A. et Stern A., « Frightening small children and disconcerting grown-ups: Concurrency in the Linux kernel », in : ASPLOS 2018: 23rd ACM International Conference on Architectural Support for Programming Languages and Operating Systems, New York, Association for Computing Machinery, 2018, p. 405-418.

Bozman C., Canou B., Di Cosmo R., Couderc P., Gesbert L., Henry G., Le Fessant F., Mauny M., Morel C. et Peyrot L., « Learn-OCaml : un assistant à l’enseignement d’OCaml », in : JFLA (Journées francophones des langages applicatifs) 2019 (Les Rousses, 2019), hal-01962838.

Guéneau A., Charguéraud A. et Pottier F., « A fistful of dollars: Formalizing asymptotic complexity claims via deductive program verification », in : ESOP 2018: 27th European Symposium on Programming, Lecture Notes in Computer Science, vol. 10801, 2018, p. 533-560.

Guéneau A., Jourdan J.-H., Charguéraud A. et Pottier F., « Formal proof and analysis of an incremental cycle detection algorithm », in J. Harrison, J. O’Leary et A. Tolmach (dir.), ITP 2019: 10th Conference on Interactive Theorem Proving (Portland, 8-12 septembre 2019), Leibniz International Proceedings in Informatics, vol. 141, 2019, p. 18:1-18:20.

Kremer S., Mé L., Rémy D. et Roca V., Cybersecurity. Current challenges and Inria’s research directions, Rocquencourt, Inria, coll. « White Book », vol. 3, 2019.

Kästner D., Wünsche U., Barrho J., Schlickling M., Schommer B., Schmidt M., Ferdinand C., Leroy X. et Blazy S., « CompCert: Practical experience on integrating and qualifying a formally verified optimizing compiler », in : ERTS 2018: Embedded Real Time Software and Systems (Toulouse, 31 janvier-2 février 2018), hal-01643290. .

Mével G., Jourdan J.-H. et Pottier F., « Time credits and time receipts in Iris », in : ESOP 2019: 28th European Symposium on Programming, Lecture Notes in Computer Science, vol. 11423, 2019, p. 1-27.

Schommer B., Cullmann C., Gebhard G., Leroy X., Schmidt M. et Wegener S., « Embedded program annotations for WCET analysis », in : WCET 2018: 18th International Workshop on Worst-Case Execution Time Analysis, OpenAccess Series in Informatics (OASIcs), vol. 63, 2018, 8:1-8:13.

Haut de page

Pour citer cet article

Référence papier

Xavier Leroy, « Sciences du logiciel »L’annuaire du Collège de France, 119 | 2022, 21-33.

Référence électronique

Xavier Leroy, « Sciences du logiciel »L’annuaire du Collège de France [En ligne], 119 | 2022, mis en ligne le 01 mars 2022, consulté le 19 janvier 2026. URL : http://journals.openedition.org/annuaire-cdf/16737 ; DOI : https://doi.org/10.4000/annuaire-cdf.16737

Haut de page

Auteur

Xavier Leroy

Professeur au Collège de France

Articles du même auteur

Haut de page

Droits d’auteur

Le texte et les autres éléments (illustrations, fichiers annexes importés), sont « Tous droits réservés », sauf mention contraire.

Haut de page
Rechercher dans OpenEdition Search

Vous allez être redirigé vers OpenEdition Search