Jean-Yves Girard

Jean-Yves Girard, né en 1947 à Lyon, est un logicien et mathématicien contemporain, directeur de recherche au CNRS (émérite) au département de logique de la programmation de l'institut de mathématiques de Luminy (devenu l'Institut de Mathématiques de Marseille depuis le ). Il a reçu la médaille d'argent du CNRS en 1983. Depuis 1994, il est correspondant de l'Académie des sciences, et membre de l'Académie européenne depuis 1995. Jean-Yves Girard est un ancien élève de l'École normale d'instituteurs de Lyon (1962) et de l'École normale supérieure de Saint-Cloud (sciences) (1966). Il obtient une licence de mathématiques en 1967, une maîtrise en 1968 et est agrégé de mathématiques en 1969. En 1970, il obtient un DEA de logique à Paris VII sous la direction de Jean-Louis Krivine. Sa recherche personnelle, notamment sur le système F, le mène au CNRS en mars 1971 où il soutient sa thèse d'Etat en juin 1972, avec Georg Kreisel comme rapporteur et Jean-Louis Krivine en directeur de thèse. Il grimpe les échelons au sein du CNRS, étant promu chargé de recherches en 1973, maître de recherches en 1981, puis directeur de recherche en 1990. Pendant ce temps, il travaille à l'Université Paris VII dans l'Équipe de Logique Mathématique jusqu'en 1992. Par la suite, il rejoint Marseille, où il dirige l'équipe de Logique de la Programmation de l'Institut de Mathématiques de Luminy avant de prendre progressivement sa retraite. En 1983, il reçoit la Médaille d’Argent du CNRS. Il s'est fait connaître au début des années 1970, en démontrant la normalisation des preuves de la logique du second ordre et de la théorie des types. Ce résultat renforce la , établie peu auparavant, par , Moto-o Takahashi et Dag Prawitz. C'est dans le cadre de cette démonstration qu'il introduit les candidats de réductibilité ("Girard's idea") et le système F, système de preuves en logique du second ordre. On lui doit, également, les dilatateurs dans la théorie des ordinaux, l'étude de la logique et , la logique linéaire et ses réseaux de preuves, la « » et la « » .

À propos de ce résultat

Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Concepts associés (7)

Jean-Yves Girard

Logique linéaire

vignette|Arbre de résolution linéaire En logique mathématique et plus précisément en théorie de la démonstration, la logique linéaire est un système formel inventé par le logicien Jean-Yves Girard en 1987. Du point de vue logique, la logique linéaire décompose et analyse les logiques classique et intuitionniste. Du point de vue calculatoire, elle est un système de type pour le lambda-calcul permettant de spécifier certains usages des ressources. La logique classique n'étudie pas les aspects les plus élémentaires du raisonnement.

Geometry of interaction

The Geometry of Interaction (GoI) was introduced by Jean-Yves Girard shortly after his work on linear logic. In linear logic, proofs can be seen as various kinds of networks as opposed to the flat tree structures of sequent calculus. To distinguish the real proof nets from all the possible networks, Girard devised a criterion involving trips in the network. Trips can in fact be seen as some kind of operator acting on the proof.