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). 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, eine neue Nichtklassische Logik, die auch in der Informatik vielfach Anwendung fand, und in diesem Zusammenhang 1989 Geometry of Interaction (GoI). 2001 begründete er Ludics aus der Analyse von Ableitungsregeln in Logiken. 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. 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). Zu seinen Doktoranden zählen Yves Lafont, Laurent Regnier.