Jean-Yves Girard

aus Wikipedia, der freien Enzyklopädie
Wechseln zu: Navigation, Suche

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

Girard besuchte die Ecole Normale Superieure de Saint Cloud und wurde 1972 an der Universität Paris VII Denis Diderot bei Jean-Louis Krivine promoviert (Interpretaton fonctionelle et elimination des coupures de l´arithmétique d´ordre superieure).[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 Academie des Sciences.

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

Schriften[Bearbeiten]

  • 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

Weblinks[Bearbeiten]

Einzelnachweise[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'Interpretation 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