Thomas Hobbes est sans doute mieux connu comme philosophe politique que comme homme de science et ses longues querelles avec John Wallis en mathématiques et Robert Boyle en physique n’ont guère encouragé les historiens des sciences à prêter attention à son œuvre scientifique. Pourtant, Hobbes conçut la philosophie comme une science et se considérait comme le fondateur non seulement d’une science nouvelle : la philosophie civile, mais aussi de la science de l’optique - récemment renouvelée à la faveur de la découverte du télescope - et même des mathématiques. Mais à quoi Hobbes pense-t-il quand il parle de science ? Aux mathématiques qu’il admire tant ? A la philosophie naturelle de Galilée ? Ou à la médecine de Harvey ? En quel sens la philosophie civile est-elle une science et quel est le statut des mathématiques ? Telles sont les questions que nous abordons à partir d’une analyse du De Corpore et des dix premiers chapitres du De Homine traduits du latin. L’interprétation proposée ici consiste à réaffirmer l’unité du système des Éléments de la philosophie et à souligner la dimension matérialiste et réaliste de la science hobbesienne. Bien que Noel Malcolm ait définitivement établi que Hobbes n’est pas l’auteur du Short Tract on first principles, nous montrons que le tournant scientifique de Hobbes est profondément marqué par son intérêt pour l’optique qu’il renouvela sur la base d’une ontologie matérialiste et des principes du mécanisme hérités de Galilée. / Thomas Hobbes is perhaps best known as a political philosopher than as a scientist and his too long quarrels with John Wallis in mathematics and Robert Boyle in physics did little to encourage historians of science to pay attention to his scientific work. Yet Hobbes conceived of philosophy as a science and considered himself the founder not only of a new science: civil philosophy, but also the science of optics - recently renewed thanks to the discovery of the telescope - even mathematics. But what Hobbes has in mind when he talks about science? Mathematics he so admires? Galileo’s natural philosophy? Or Harvey’s medicine? In what sense civil philosophy is a science and what is the status of mathematics? These are the issues we discuss from an analysis of De Corpore and the first ten chapters of De Homine translated from Latin. The interpretation proposed here is to underline the unity of the system of the Elements of philosophy and emphasize the materialistic and realistic nature of Hobbesian science. Although Noel Malcolm has definitively established that Hobbes is not the author of Short Tract on First Principles, we show that Hobbes’s shift to science was deeply marked by his interest in the science of optics he renewed on the basis of a materialist ontology and principles inherited from Galilee mechanism.

Mes travaux de recherche portent sur la théorie de la démonstration, le lambda-calcul et l'informatique théorique, dans la ligne de la correspondance de Curry-Howard entre les preuves et les programmes.<br /><br />Dans ma thèse de doctorat, j'ai étudié les opérateurs de mise en mémoire pour les types de données. Ces notions, qui sont introduites par Krivine, permettent de programmer en appel par valeur tout en utilisant la stratégie de la réduction de tête pour exécuter les $\lambda$-termes. Pour cette étude, j'ai introduit avec David une extension du $\lambda$-calcul avec substitutions explicites appelée $\lambda$-calcul dirigé. Nous en avons déduit une nouvelle caractérisation des termes de mise en mémoire et obtenu des nombreux résultats très fins à leur sujet. En ce qui concerne le typage des opérateurs de mise en mémoire, Krivine a trouvé une formule du second ordre, utilisant la non-non traduction de Gödel de la logique classique dans la logique intuitionniste, qui caractérise ces opérateurs. Je me suis attaché à diverses généralisations du résultat de Krivine pour les types à quantificateur positif dans des extensions de la logique des prédicats du second ordre.<br /><br />J'ai poursuivi, après ma thèse, une activité de recherche sur l'extension de la correspondance de Curry-Howard à la logique classique, au moyen des instructions de contrôle. J'ai étudié des problèmes liés aux types de données dans deux de ces systèmes : le $\lambda \mu$-calcul de Parigot et le $\lambda C$-calcul de Krivine. J'ai donné des algorithmes très simples permettant de calculer la valeur d'un entier classique dans ces deux systèmes. J'ai également caractérisé les termes dont le type est l'une des règles de l'absurde. J'ai étendu le système de Parigot pour en obtenir une version non déterministe mais où les entiers se réduisent toujours en entiers de Church. Curieusement, ce système permet de programmer la fonction ``ou parallèle''.<br /><br />Je me suis intéressé aux systèmes numériques qui servent à représenter les entiers naturels au sein du $\lambda$-calcul. J'ai montré que pour un tel système, la possession d'un successeur, d'un prédécesseur et d'un test à zéro sont des propriétés indépendantes, puis qu'un système ayant ces trois fonctions possède toujours un opérateur de mise en mémoire. Dans un cadre typé, j'ai apporté une réponse négative à une conjecture de Tronci qui énonçait une réciproque du résultat précédent.<br /><br />La notion de mise en mémoire ne s'applique qu'à des types de données. Une définition syntaxique a été donné par Böhm et Berarducci, et Krivine a proposé une définition sémantique de ces types. J'ai obtenu avec Farkh des résultats reliant la syntaxe et la sémantique des types de données. Nous avons proposé également des définitions des types entrée et des types sortie pour lesquelles nous avons montré diverses propriétés syntaxiques et sémantiques.<br /><br />J'ai réussi à combiner la logique intuitionniste et la logique classique en une logique mixte. Dans cette logique, on distingue deux genres de variables du second ordre, suivant que l'on peut, ou non, leur appliquer le raisonnement par l'absurde. Ce cadre m'a permi de donner le type le plus général pour les opérateurs de mise en mémoire. Vu le rôle important que cette logique semble devoir jouer dans la théorie de ces opérateurs, j'en ai mené avec A. Nour une étude théorique approfondie. Le système de logique mixte propositionnelle auquelle nous avons abouti évoque les sytèmes $LC$ de Girard et $LK^{tq}$ de Danos, Joinet et Schellinx.<br /><br />Je me suis intéressé avec David à l'équivalence induite par l'égalité entre les arbres de Böhm infiniment $\eta$-expansés. Avec Raffalli, je me suis également intéressé à la sémantique de la logique du second ordre.

Les défis pour voir des robots opérant dans l'environnement de tous les jours des humains et sur une longue durée soulignent l'importance de leur adaptation aux changements qui peuvent être imprévisibles au moment de leur construction. C'est pourquoi, les robots doivent être capables d'apprendre continuellement dans des espaces infinis, non-stationnaires et de grande dimension. Il leur est impossible d'explorer tout son environnement pour apprendre pendant la durée limitée de sa vie. Pour être utile et acquérir des compétences, le robot doit au contraire être capable de savoir quelles parties échantillonner, et quels types de compétences il a intérêt à acquérir. Une manière de collecter des données est de décider par soi-même où explorer. Une autre manière est de se référer à un mentor. Nous appelons ces deux manières de collecter des données des modes d'échantillonnage. Le premier mode d'échantillonnage correspond à des algorithmes développés dans la littérature pour automatiquement pousser l'agent vers des parties intéressantes de l'environnement ou vers des types de compétences utiles. De tels algorithmes sont appelés des algorithmes de curiosité artificielle ou motivation intrinsèque. Le deuxième mode d'échantillonnage correspond au guidage social ou l'imitation, où un partenaire humain indique où explorer et où ne pas explorer. D'une étude des liens entre ces deux méthodes concurrentes, nous avons finalement construit une architecture algorithmique où les deux modes s'entremêlent en un structure hiérarchique, appelée Socially Guided Intrinsic Motivation (SGIM).