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.

Schriften

• 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

• Homepage
• Literatur von und über Jean-Yves Girard im SUDOC-Katalog (Verbund französischer Universitätsbibliotheken)

Einzelnachweise

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