Jean-Yves Girard
Pour les articles homonymes, voir Girard.
| Directeur de recherche au CNRS |
|---|
| Naissance | |
|---|---|
| Pseudonyme |
Yann-Joachim Ringard |
| Nationalité | |
| Formation | |
| Activités |
| A travaillé pour | |
|---|---|
| Membre de | |
| Maître | |
| Directeur de thèse | |
| Sites web | |
| Distinctions |
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.
Biographie
[modifier | modifier le code]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 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.
En 1990, il écrit sous le pseudonyme Yann-Joachim Ringard un pamphlet satirique contre la sémantique de Kripke: Les montres à moutarde, une approche intégrée au temps et à la nourriture[1].
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).
L'influence de Jean-Yves Girard et de la logique linéaire couvre maintenant plusieurs domaines, tels que la logique, les mathématiques (pour la question des fondements), l'informatique (pour la gestion de ressources), la linguistique (Multiplicative Linear Logic et calcul de Lambek (en)) et la philosophie.
Bibliographie
[modifier | modifier le code]- 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 » .
- J.-Y. Girard, P. Taylor, Y. Lafont, Proofs and Types, Cambridge University Press, 1989
- Ernest Nagel, James R. Newman, Kurt Gödel et Jean-Yves Girard, Le théorème de Gödel, Éditions du Seuil, [détail de l’édition]
- J.-Y. Girard, Le fantôme de la transparence, Éditions Allia, .
Articles grand public
[modifier | modifier le code]- 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.
Références
[modifier | modifier le code]- Yann-Joachim Ringard, « Les montres à moutarde : une approche intégrée au temps et à la nourriture »
[PDF],
Articles connexes
[modifier | modifier le code]Liens externes
[modifier | modifier le code]- Ressources relatives à la recherche :
- Page personnelle de Jean-Yves Girard
- Mathématicien français du XXe siècle
- Mathématicien français du XXIe siècle
- Logicien français
- Membre de l'Académie des sciences (France)
- Théorie des types
- Personnalité en théorie de la démonstration
- Naissance à Lyon
- Directeur de recherche au CNRS
- Élève de l'École normale supérieure de Saint-Cloud
- Naissance en 1947
- Lauréat de la médaille d'argent du CNRS
- Lauréat du prix Poncelet