Search

Correction de quelques typos et de la mise en forme (césures).; Forges de l'Enseignement supérieur et de la Recherche Définition, usages, limitations rencontrées et analyse des besoins Collège Codes sources et logiciels du Comité pour lascience ouverte Forges de l'Enseignement supérieur et de la Recherche Définition, usages, limitations rencontrées et analyse des besoins Collège codes sources et logiciels du Comité pour la science ouverte Mai 2023 Conception graphique : opixido

Merci beaucoup de m'accueillir ici aujourd'hui. C'est un réel plaisir d'ouvrir cette session sur la place des logiciels dans la science ouverte. Permettez-moi de commencer par vous présenter un peu le contexte. Si nous regardons autour de nous, nous voyons des logiciels partout. Ils alimentent notre industrie, nourrissent les innovations et sont essentiels à la recherche universitaire. Ils sont le tissu qui lie nos vies numériques et professionnelles. C’est grâce aux logiciels que nous sommes...

Depuis plus de vingt ans, la communauté scientifique internationale affirme son soutien à la science ouverte comme fondement d’une recherche plus collaborative, transparente, intègre et proche de la société. Cette orientation s’est notamment traduite en France par l’adoption de deux Plans nationaux pour la science ouverte, en 2018 et 2021. Dans cette dynamique et à l’occasion de la présidence française du Conseil de l’Union européenne, la France a organisé les 4 et 5 février 2022 les Journées européennes de la science ouverte (OSEC). Cette conférence sur la transformation de l’écosystème de la recherche et de l’innovation en Europe a été l’occasion d’aborder en particulier la transparence des recherches en santé, l’avenir de l’édition scientifique et l’ouverture des codes et logiciels produits dans un contexte de recherche, mais aussi les transformations nécessaires de l’évaluation de la recherche, synthétisées dans l’Appel de Paris présenté lors de ces Journées et appelant à la création d’une coalition d’acteurs engagés pour une réforme du système actuel. Cet événement international a été organisé avec le soutien de l’Académie des sciences, du ministère de l’Enseignement supérieur et de la Recherche, du Centre national de la recherche scientifique (CNRS), de l’Institut national de la santé et de la recherche médicale (INSERM), du Haut Conseil de l’évaluation de la recherche et de l’enseignement supérieur (Hcéres), de l’Agence nationale de la recherche (ANR), de l’Université de Lorraine et de l’Université de Nantes.

International audience; Entrée qui décrit le Code Source dans le Dictionnaire du Numérique paru en Février 2022, ISBN 9781784058180

Software is a hybrid object in the world research as it is equally a driving force (as a tool), a result (as proof of the existence of a solution) and an object of study (as an artefact). This specific status means we need to define strategies, tools and procedures which are adapted to the various issues it raises. These include the citation of contributions to software design and production, the reproducibility of research results involving software and the wider usage and long-term sustainability of the software heritage created. This opportunity note by the Committee for Open Science's Free Software and Open Source Project Group describes the issues at stake and formulates actionable recommendations.; Le logiciel est un objet hybride au sein de la recherche, dont il est à la fois moteur (comme outil), résultat (comme preuve d’existence d’une solution) et objet d’études (comme artefact). Ce statut spécifique doit amener à la définition de stratégies, d’outils et de procédures adaptés aux différents enjeux qu’il soulève, tels que notamment : la citation des contributions relatives à la conception et à la production de logiciels, la reproductibilité des résultats de recherche faisant intervenir des logiciels, la valorisation et la pérennisation du patrimoine logiciel créé.

International audience; La plateforme Learn-OCaml est un assistant à l'enseignement du langage de program-mation OCaml, développée dans le cadre du projet éponyme porté par la Fondation OCaml, qui vise à soutenir et développer l'usage d'OCaml dans l'enseignement. La plateforme permet d'écrire des exercices munis de correcteurs automatiques qui peuvent tester non seulement la correction fonctionnelle des programmes soumis par les étudiants mais aussi la façon dont ces programmes sont écrits ou calculent. Dans cet article, nous présentons la plateforme dans son ensemble, le projet dans lequel s'inscrit son développement, et ses fonctionnalités principales, à travers notamment l'écriture d'un exercice et de son correcteur ainsi qu'un premier retour sur deux expériences d'usage menées à l'

International audience; Les logiciels sont devenus le support indissociable des connaissances techniques et scientifiques de l'humanité tout entière. Ils constituent un véritable socle pour les sciences. La préservation des logiciels est à la base de la reproductibilité. L'utilisation des logiciels intervient à toutes les étapes de la recherche, dans tous les domaines scientifiques, et se révèle essentielle à de multiples égards. La collaboration entre Software Heritage (SWH), Hal-Inria et le CCSD a permis l'ouverture de Hal vers le nouveau type de données scientifiques: le logiciel.

National audience; Aborder les sciences informatiques sans avoir recours à un ordinateur ? Découvrez comment à travers les activités proposées par Computer Science Unplugged.

Les TIC ont profondément changé l'écosystème de la publication scientifique, en révélant au grand jour un conflit d'intérêts grandissant entre les éditeurs d'un coté et tous les autres acteurs de l'autre. En partant d'une analyse précise des exigences minimales d'un système de publication scientifique, et du divorce qui se consomme entre auteurs, utilisateurs et éditeurs de la publication scientifique à cause de la révolution apportée par les TIC, nous mettons ici en évidence ce que la communauté scientifique peut faire, et commence déjà à faire par elle même, pour se libérer du joug désormais injustifié imposé par les éditeurs.

National audience; La qualification de « libres » pour des logiciels ne rime pas avec simplicité, loin de là : ces derniers posent des problèmes théoriques spécifiques liés à leur mode d'élaboration.

International audience; This note on the management of bibliographies explains the interest of properly separating content and form in bibliographic information, in order to reconcile the need for efficient management of a bibliographic database with the need to produce outputs in a variety of different styles. It uses for this the BibTeX format, very popular with users of LaTeX, a high quality typesetting system which is the de facto standard for communication and publication of scientific documents.; Cette note sur la gestion des bibliographies explique l'intérêt de bien séparer contenu et forme dans l’information bibliographique, afin de concilier le besoin d'une gestion efficace d'une base de données bibliographique avec le besoin de produire des sorties sous des formes et avec des styles différents. Elle utilise pour cela le format BibTeX, très populaire auprès des utilisateurs de LaTeX, un système de haute qualité qui est le standard de facto pour la communication et la publication de documents scientifiques.

International audience; This note on the management of bibliographies explains the interest of properly separating content and form in bibliographic information, in order to reconcile the need for efficient management of a bibliographic database with the need to produce outputs in a variety of different styles. It uses for this the BibTeX format, very popular with users of LaTeX, a high quality typesetting system which is the de facto standard for communication and publication of scientific documents.; Cette note sur la gestion des bibliographies explique l'intérêt de bien séparer contenu et forme dans l’information bibliographique, afin de concilier le besoin d'une gestion efficace d'une base de données bibliographique avec le besoin de produire des sorties sous des formes et avec des styles différents. Elle utilise pour cela le format BibTeX, très populaire auprès des utilisateurs de LaTeX, un système de haute qualité qui est le standard de facto pour la communication et la publication de documents scientifiques.

Mes recherches ont principalement porté sur la programmation par contraintes, avec deux thèmes de prédilection, les contraintes sur les réels et les contraintes sur les flottants.Sur les réels, ces travaux se caractérisent principalement par l’utilisation rigoureuse de relaxations linéaires pour la résolution de systèmes de contraintes sur les réels et d’optimisation globale d’une fonction réelle soumise à un ensemble de contraintes sur les réels. Dans le premier cas, notre approche s’appuie sur un filtrage global qui capture le sous-système linéaire augmenté d’un certain nombre de relaxations linéaires de termes non linéaires. Dans le second cas, les relaxations linéaires sont utilisées afin de déterminer une borne inférieure de la fonction objectif. Dans les deux cas, le calcul des coefficients des relaxations linéaires est effectué par des procédures rigoureuses garantes de la préservation de l’ensemble des solutions du problème initial, et le système linéaire obtenu est résolu à l’aide d’un simplexe dont le minimum global est lui aussi calculé de manière rigoureuse.Sur les flottants, ces recherches se sont traduites par l'introduction des contraintes sur les flottants. Ce type de contraintes particulières n’avait pas d’existence avant ces travaux. Elles sont pourtant nécessairement pour traiter des expressions faisant appel à des calculs sur les flottants, chose à laquelle de plus en plus de programmes font appel. Ces recherches partent de l’introduction d’un cadre pour les traiter correctement, pour s’attacher ensuite à améliorer le fonctionnement d’un solveur sur les flottants, que ce soit en introduisant une forme de filtrage plus performante basée sur une consistance de type 2B, en améliorant le fonctionnement de projections particulières telles que l’addition et la soustraction, en plongeant les contraintes sur les flottants dans les réels, ou en faisant collaborer contraintes sur les flottants et interprétation abstraite. Une application à la détection de fausses alarmes illustre le fonctionnement des outils développés sur un exemple industriel.

Software depend on third-party libraries to reduce development and maintenance costs. Developers have access to robust functionalities through an application programming interface designed by these libraries. However, due to the strong relationship with these libraries, developers have to reconsider their position when the software evolves. In this thesis, we identify several re-search problems involving these third-party libraries in a context of software maintenance. More specifically, a library may not satisfy the software new requirements and has to be replaced by anew one. We call this operation a library migration.We leverage three points that characterize the impediments met by developers in this situation.To which library should they migrate ? How to migrate their software ? Who can help them in this case ? This thesis suggests answers and exposes several contributions to these problems. We define three approaches that are evaluated through several case studies. To achieve this work, weuse a methodology based on software evolution analysis to observe and understand how software change. We describe numerous perspectives to overcome the current limitations of our solutions., Les logiciels dépendent de bibliothèques tierces pour réduire les coûts liés à leur développement et à leur maintenance. Elles proposent un ensemble de fonctionnalités robustes dont les développeurs peuvent tirer parti depuis une interface de programmation. Cependant, cette forte dépendance entre un logiciel et ses bibliothèques oblige les développeurs à reconsidérer leur rôle lorsque le logiciel évolue. Dans cette thèse, nous identifions plusieurs problématiques impliquant les bibliothèques tierces dans un contexte de maintenance logicielle. Plus particulièrement, une bibliothèque peut ne plus répondre aux besoins d’un logiciel et doit être remplacée par une nouvelle.Nous nommons cette opération une migration de bibliothèque.Nous soulevons dans ce contexte trois points qui caractérisent les difficultés rencontrées par les développeurs. Vers quelle bibliothèque migrer ? Comment appliquer la migration ? Avec l’aide de quels développeurs ? Cette thèse discute de solutions et apporte des contributions autour de ces problèmes. Nous présentons plusieurs approches et les évaluons lors de différents cas d’étude. L’analyse de l’évolution logicielle sera notre support de travail, dont la méthodologie est basée sur l’observation des changements de logiciels. Nous décrivons les limites actuelles de nos contribu-tions et ouvrons des perspectives futures pour enrichir l’état de l’art dans ce domaine

The Coq proof assistant mechanically checks the consistency of the logical reasoning in a proof. It can also be used to develop certified programs. Indeed, Coq uses internally a typed language derived from λ-calculus, the calculus of inductive constructions (CIC). This language can be directly used by a programmer, and a procedure — extraction — allows one to translate CIC programs into more widely used languages such as OCaml, Haskell or Scheme.Extraction is not a mere syntax change: the type system of CIC is very rich, but purely logical entities can appear inside programs, impacting their performance. Extraction erases these logical artefacts as well.In this thesis, we tackle certification of the extraction itself. We have proved its correction in the context of a full formalization of Coq in Coq. Even though this formalization is not exactly Coq, we worked on it with the concrete implementation of Coq in mind. We also propose a new way to certify extracted programs, in the concrete setting of the existing Coq system., L’assistant de preuve Coq permet de s’assurer mécaniquement de la correction de chaque étape de raisonnement dans une preuve. Ce système peut également servir au développement de programmes certifiés. En effet, Coq utilise en interne un langage typé dérivé du λ-calcul, le calcul des constructions inductives (CIC). Ce langage est directement utilisable pour programmer, et un mécanisme — l’extraction — permet de traduire les programmes CIC vers des langages à plus large audience tels qu’OCaml, Haskell ou Scheme.L’extraction n’est pas un simple changement de syntaxe : CIC dispose d’un système de types très riche, mais en contrepartie, des entités purement logiques peuvent apparaître dans les programmes et impacter leurs performances. L’extraction se charge également d’effacer ces parties logiques.Dans cette thèse, nous nous attaquons à la certification de l’extraction elle-même. Nous avons prouvé sa correction dans le cadre d’une formalisation entière de Coq en Coq. Cette formalisation ne correspond pas exactement au CIC implanté dans Coq, mais nous avons tout de même réalisé notre étude avec l’implantation concrète de Coq en tête. Nous proposons également une nouvelle méthode de certification des programmes extraits, dans le cadre concret du système Coq existant.

The goal of this thesis is to study the sum and the zero within two principal frameworks: type isomorphisms and the normalization of lambda-terms. Type isomorphisms have already been studied within the framework of the simply typed lambda-calculus with surjective pairing but without sums. To handle the case with sums and zero, I first restricted the study to the case of linear isomorphisms, within the framework of linear logic, which led to a remarkably simple characterization of these isomorphisms, obtained thanks to a syntactic method on proof-nets. The more general framework of intuitionistic logic corresponds to the open problem of characterizing isomorphisms in bi-cartesian closed categories. I contributed to this study by showing that there is no finite axiomatization of these isomorphisms. To achieve this, I used some results in number theory regarding Alfred Tarski's so-called ``high school algebra'' problem. The whole of this work brought about the problem of finding a canonical form to represent lambda-terms, with the aim of either denying the existence of an isomorphism by a case study on the form of the term, or checking their existence in the case of the very complex functions I was brought to handle. This analysis led us to give an ``extensional'' definition of normal form for the lambda-calculus with sums and zero, obtained by categorical methods using Grothendieck logical relations. Finally, I could obtain an ``intentional'' version of this result by using normalization by evaluation. By adapting the technique of type-directed partial evaluation, it is possible to produce a result in the new normal form, reducing considerably its size in the case of the type isomorphisms considered before.; Le but de cette thèse est d'étudier la somme et le zéro dans deux principaux cadres : les isomorphismes de types et la normalisation de lambda-termes. Les isomorphismes de type avaient déjà été étudiés dans le cadre du lambda-calcul simplement typé avec paires surjectives mais sans somme. Pour aborder le cas avec somme et zéro, j'ai commencé par restreindre l'étude au cas des isomorphismes linéaires, dans le cadre de la logique linéaire, ce qui a conduit à une caractérisation remarquablement simple de ces isomorphismes, obtenue grâce à une méthode syntaxique sur les réseaux de preuve. Le cadre plus général de la logique intuitionniste correspond au problème ouvert de la caractérisation des isomorphismes dans les catégories bi-cartésiennes fermées. J'ai pu apporter une contribution à cette étude en montrant qu'il n'y a pas d'axiomatisation finie de ces isomorphismes. Pour cela, j'ai tiré partie de travaux en théorie des nombres portant sur un problème énoncé par Alfred Tarski et connu sous le nom du « problème des égalités du lycée ». Pendant tout ce travail sur les isomorphismes de types, s'est posé le problème de trouver une forme canonique pour représenter les lambda-termes, que ce soit dans le but de nier l'existence d'un isomorphisme par une étude de cas sur la forme du terme, ou pour vérifier leur existence dans le cas des fonctions très complexes que j'étais amené à manipuler. Cette réflexion a abouti à poser une définition « extensionnelle » de forme normale pour le lambda-calcul avec somme et zéro, obtenue par des méthodes catégoriques grâce aux relations logiques de Grothendieck, apportant ainsi une nouvelle avancée dans l'étude de la question réputée difficile de la normalisation de ce lambda-calcul. Enfin je montrerai comment il est possible d'obtenir une version « intentionnelle » de ce résultat en utilisant la normalisation par évaluation. J'ai pu ainsi donner une adaptation de la technique d' évaluation partielle dirigée par les types pour qu'elle produise un résultat dans cette forme normale, ce qui en réduit considérablement la taille et diminue aussi beaucoup le temps de normalisation dans le cas des isomorphismes de types considérés auparavant.

The goal of this thesis is to study the sum and the zero within two principal frameworks: type isomorphisms and the normalization of lambda-terms. Type isomorphisms have already been studied within the framework of the simply typed lambda-calculus with surjective pairing but without sums. To handle the case with sums and zero, I first restricted the study to the case of linear isomorphisms, within the framework of linear logic, which led to a remarkably simple characterization of these isomorphisms, obtained thanks to a syntactic method on proof-nets. The more general framework of intuitionistic logic corresponds to the open problem of characterizing isomorphisms in bi-cartesian closed categories. I contributed to this study by showing that there is no finite axiomatization of these isomorphisms. To achieve this, I used some results in number theory regarding Alfred Tarski's so-called ``high school algebra'' problem. The whole of this work brought about the problem of finding a canonical form to represent lambda-terms, with the aim of either denying the existence of an isomorphism by a case study on the form of the term, or checking their existence in the case of the very complex functions I was brought to handle. This analysis led us to give an ``extensional'' definition of normal form for the lambda-calculus with sums and zero, obtained by categorical methods using Grothendieck logical relations. Finally, I could obtain an ``intentional'' version of this result by using normalization by evaluation. By adapting the technique of type-directed partial evaluation, it is possible to produce a result in the new normal form, reducing considerably its size in the case of the type isomorphisms considered before., Le but de cette thèse est d'étudier la somme et le zéro dans deux principaux cadres : les isomorphismes de types et la normalisation de lambda-termes. Les isomorphismes de type avaient déjà été étudiés dans le cadre du lambda-calcul simplement typé avec paires surjectives mais sans somme. Pour aborder le cas avec somme et zéro, j'ai commencé par restreindre l'étude au cas des isomorphismes linéaires, dans le cadre de la logique linéaire, ce qui a conduit à une caractérisation remarquablement simple de ces isomorphismes, obtenue grâce à une méthode syntaxique sur les réseaux de preuve. Le cadre plus général de la logique intuitionniste correspond au problème ouvert de la caractérisation des isomorphismes dans les catégories bi-cartésiennes fermées. J'ai pu apporter une contribution à cette étude en montrant qu'il n'y a pas d'axiomatisation finie de ces isomorphismes. Pour cela, j'ai tiré partie de travaux en théorie des nombres portant sur un problème énoncé par Alfred Tarski et connu sous le nom du « problème des égalités du lycée ». Pendant tout ce travail sur les isomorphismes de types, s'est posé le problème de trouver une forme canonique pour représenter les lambda-termes, que ce soit dans le but de nier l'existence d'un isomorphisme par une étude de cas sur la forme du terme, ou pour vérifier leur existence dans le cas des fonctions très complexes que j'étais amené à manipuler. Cette réflexion a abouti à poser une définition « extensionnelle » de forme normale pour le lambda-calcul avec somme et zéro, obtenue par des méthodes catégoriques grâce aux relations logiques de Grothendieck, apportant ainsi une nouvelle avancée dans l'étude de la question réputée difficile de la normalisation de ce lambda-calcul. Enfin je montrerai comment il est possible d'obtenir une version « intentionnelle » de ce résultat en utilisant la normalisation par évaluation. J'ai pu ainsi donner une adaptation de la technique d' évaluation partielle dirigée par les types pour qu'elle produise un résultat dans cette forme normale, ce qui en réduit considérablement la taille et diminue aussi beaucoup le temps de normalisation dans le cas des isomorphismes de types considérés auparavant.

Game theory had, in its origins, a vocation for social and economic sciences, with disparate applications, for example in the processing of medical data. It is perceived today as a very general paradigm of concepts and techniques, whose potential still remains to be discovered in computer science. In this thesis we study a particular branch, combinatorial game theory (with two players), in order to profit from it in the very active field of formal semantics of programming languages. Within a game, we can separate the syntactic aspect, inherent in the possible outcomes of matches, from the semantic aspect, inherent in the forecasts over the winning player and, possibly, inherent in a quantification of profit, in terms of a stake, like wealth or prestige. To model the concept of profit, the selected structure of evaluation should not necessarily be the structure of booleans (win or loose), or that of natural or relative numbers. It is enough for this structure to verify some properties, rather weak, guaranteeing the existence of a semantics, even when the play gives rise to infinite matches, as in the game of bisimulation between concurrent processes, or as in the game of logic programming. In this work, we study the semantic characterization of a logical language (with or without constraints) in terms of a game with two players. The effect of such an interpretation, beyond the intuitive model whose didactic value would deserve to be examined, makes it possible to reuse Alpha-Beta, one of the most celebrated algorithms in combinatorial game theory, as a resolution engine for logical languages. The recent and spectacular results obtained by chess programs (like the defeat of the world champion Kasparov against the IBM program Deep Blue) testify to a kind of artificial intelligence acquired by these programs that might be transposed and exploited in the resolution of logical languages. The resolution of existential conjunctive goals in a first-order theory of Horn clauses provides an interesting case. Indeed, the ability of Alpha-Beta to simplify calculation or, in other words, to prune the uninteresting paths, is not closely related to a particular type of game or profit, but to a well-chosen set of algebraic properties, satisfied by the game of logical programming. The correction of Alpha-Beta is formally proven for a very wide variety of structures. In this way, the computed values could be natural numbers, as in the case of chess, or substitutions or constraints, as in the case of logical languages., La théorie des jeux a développé, à ses débuts, une vocation pour les sciences sociales et économiques, avec des applications disparates, comme par exemple le traitement de données médicales. Elle apparaît aujourd'hui comme un paradigme de concepts et de techniques très général, dont le potentiel reste encore à exploiter en informatique. Dans cette thèse nous étudions une branche particulière, la théorie des jeux combinatoires (à deux joueurs), pour en tirer bénéfice dans le domaine, très actif, des sémantiques formelles des langages de programmation. D'un jeu, nous pouvons séparer l'aspect syntaxique, inhérent aux dénouements possibles des matchs, de l'aspect sémantique, inhérent aux prévisions sur le gagnant et la quantification de son gain (en termes d'un enjeu quelconque, tel que l'argent ou le préstige). Pour modeliser la notion de gain, la structure d'évaluation choisie ne doit pas forcément être celle des booléens (gagné ou perdu), ou celle des entiers naturels ou relatifs. Il suffit qu'elle vérifie des propriétés, assez faibles, garantissant l'existence d'une sémantique même lorsque le jeu donne lieu à des matchs infinis, comme dans le cas du jeu de la bisimulation entre processus concurrents, et du jeu de la programmation logique. Dans ce travail, nous étudions la caractérisation sémantique d'un langage logique (avec ou sans contrainte) en termes de jeu à deux joueurs. Au-delà du modèle intuitif des jeux, dont la valeur pédagogique mériterait d'être approfondie, une telle interprétation permet de réutiliser un des algorithmes les plus utilisés dans la théorie des jeux combinatoire, Alpha-Bêta, comme moteur de résolution pour les langages logiques. Les résultats récents et spectaculaires obtenus par les programmes d'échecs (souvenons-nous de la défaite du champion du monde Kasparov contre le programme Deep Blue d'IBM) témoignent d'une forme d'intelligence artificielle développée dans ces programmes qui peut être transposée et exploitée dans la résolution des langages logiques. La résolution d'interrogations existentielles conjonctives dans une théorie de clauses de Horn du premier ordre est en particulier concernée. En effet, la capacité d'Alpha-Bêta à simplifier le calcul ou, en d'autres termes, sa capacité à éliminer les coups inintéressants, n'est pas intimement liée à un type de jeu ou à un type de gain particuliers, mais demande juste des propriétés algébriques qui sont satisfaites dans le jeu de la programmation logique. La correction d'Alpha-Bêta est prouvée de façon formelle pour un éventail de structures très large. Les valeurs calculées pourront être aussi bien des entiers naturels, comme dans le cas du jeu d'échecs, que des substitutions ou des contraintes, comme dans le cas des langages logiques.