Jean-Yves Girard

aus Wikipedia, der freien Enzyklopädie
Zur Navigation springen Zur Suche springen
Jean-Yves Girard

Jean-Yves Girard (* 1947 in Lyon) ist ein französischer mathematischer Logiker.

Girard besuchte die École Normale Supérieure de Saint Cloud und wurde 1972 an der Universität Paris VII Denis Diderot bei Jean-Louis Krivine promoviert (Interprétaton fonctionelle et élimination des coupures de l'arithmétique d'ordre supérieure).[1] Er lehrte an der Universität Paris VII und an der Université de la Mediteranée Aix-Marseille.

Girard ist bekannt für Beiträge zur Beweistheorie mit Anwendungen in der Informatik. Er führte 1987 die Lineare Logik ein[2][3], eine neue Nichtklassische Logik, die auch in der Informatik vielfach Anwendung fand, und in diesem Zusammenhang 1989 Geometry of Interaction (GoI)[4]. 2001 begründete er Ludics aus der Analyse von Ableitungsregeln in Logiken.[5]

1971/2 führte er in seiner Dissertation eine getypte polymorphe Form des Lambda-Kalküls ein (wie unabhängig John C. Reynolds), System F.[6] Sie fand Anwendungen in der Theorie der Programmiersprachen (u. a. theoretische Grundlagen von ML).

Er ist Mitglied der Académie des sciences und der Academia Europaea (1995).[7]

Zu seinen Doktoranden zählen Yves Lafont, Laurent Regnier.

  • mit Yves Lafont, Paul Taylor: Proofs and Types, Cambridge University Press 1989
  • Proof theory and logic complexity, Neapel, Bibliopolis 1987
  • Herausgeber mit Yves Lafont, Laurent Regnier: Advances in linear logic, Cambridge University Press 1995

Einzelnachweise

[Bearbeiten | Quelltext bearbeiten]
  1. Mathematics Genealogy Project
  2. Girard Linear Logic, Theoretical Computer Science, Band 50, 1987, S. 1–102
  3. Linear Logic, Stanford Encyclopedia of Philosophy
  4. Girard Towards a geometry of interaction, Contemporary Mathematics, Band 92, 1989, S. 69
  5. Girard Locus solum: from the rules of logic to the logic of rules, in: Mathematical Structures in Computer Science, 11, 2001, 301–506
  6. Une Extension de l'Interprétation de Gödel à l'Analyse, et son Application à l'Élimination des Coupures dans l'Analyse et la Théorie des Types". Proceedings of the Second Scandinavian Logic Symposium. Amsterdam. 1971, S. 63–92
  7. Eintrag auf der Internetseite der Academia Europaea