Jean-Yves Girard

Jean -Yves Girard ( b. 1947 in Lyon ) is a French mathematical logician.

Girard attended the Ecole Normale Superieure de Saint Cloud and in 1972 at the University of Paris VII Denis Diderot, Jean -Louis Krivine doctorate ( Interpretaton fonctionelle et elimination of coupures de l' ordre d' arithmétique Superieure ). He taught at the University of Paris VII and at the Université de la Méditerranée Aix -Marseille.

Girard is known for his contributions to proof theory with applications in computer science. He led the 1987 Linear logic one, a new Non-classical logic, which in many cases was applied also in computer science, and in this connection in 1989 Geometry of Interaction ( GoI ). In 2001 he founded Ludics from the analysis of derivation rules in logics.

1971/2 he introduced in his thesis a typed polymorphic form of the lambda - calculus (such as independent John C. Reynolds ), System F. They found applications in the theory of programming languages ​​(including theoretical foundations of ML).

He is a member of the Academie des Sciences.

His doctoral include Yves Lafont, Laurent Regnier.

Writings

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