Accueil🇫🇷Chercher

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 est médaille d'argent du CNRS en 1983, correspondant de l'Académie des sciences depuis 1994, membre de l'Académie européenne depuis 1995.

Biographie

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 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 conjecture de Takeuti (en), établie peu auparavant, par William W. Tait (en), 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 « ludique (en) » et la « géométrie de l'interaction (en) » . Il a écrit de nombreux livres et articles de vulgarisation, dont des articles dans Pour la Science et Sciences et Avenir.

Son cours de logique (Le Point Aveugle, 2006 et 2007) donne un éclairage nouveau sur l’état actuel de la discipline, ainsi qu'il donne à voir ses dernières avancées, à la lumière de l'opposition entre essence et existence. Des notes issues de ses cours avaient auparavant été traduites et mises en forme par Y. Lafont et P. Taylor (Proofs and Types, 1989).

Bibliographie

  • J.-Y. Girard, Le Point Aveugle, Cours de Logique, ed. Hermann, Paris, collection « Visions des Sciences »:
    • Tome 1 : Vers la Perfection, 280 pp., . Cours de thĂ©orie de la dĂ©monstration s'ouvre sur une rĂ©flexion sur l'Ă©tat actuel de la logique (essentialisme et existentialisme, thĂ©orème d'incomplĂ©tude de Gödel, calcul des sĂ©quents), poursuit sur la correspondance de Curry-Howard (système F, interprĂ©tation catĂ©gorique) puis motive et dĂ©crit la logique linĂ©aire (espaces cohĂ©rents, système LL, rĂ©seaux de preuves).
    • Tome 2 : Vers l'imperfection, 288 pp., . Le cours continue en exposant l' « hypothèse de la polarisation » (les « desseins », la « ludique » et les systèmes LC et LLP), puis dĂ©crit les systèmes expĂ©rimentaux LLL et ELL et les « espaces cohĂ©rents quantiques », et enfin s'achève sur la « gĂ©omĂ©trie de l'interaction » .

Articles grand public

  • Le thĂ©orème de Gödel ou une soirĂ©e avec M. Homais, Sciences et Avenir,
  • L'idĂ©e d'incomplĂ©tude, Science et Avenir 121, .
  • La logique linĂ©aire, Pour la Science, 150, p. 74-85, .
  • Une thĂ©orie gĂ©omĂ©trique des ordinaux, Pour la Science, , reprise dans « Les mathĂ©matiques aujourd'hui », Belin, 1986, p. 97-108.

Article connexe

Liens externes

Cet article est issu de wikipedia. Text licence: CC BY-SA 4.0, Des conditions supplémentaires peuvent s’appliquer aux fichiers multimédias.