Jean-Yves Girard (; born 1947) is a French
logician working in
proof theory
Proof theory is a major branchAccording to Wang (1981), pp. 3–4, proof theory is one of four domains mathematical logic, together with model theory, axiomatic set theory, and recursion theory. Barwise (1978) consists of four corresponding part ...
. He is the research director (
emeritus
''Emeritus'' (; female: ''emerita'') is an adjective used to designate a retired chair, professor, pastor, bishop, pope, director, president, prime minister, rabbi, emperor, or other person who has been "permitted to retain as an honorary title ...
) at the mathematical institute of the
University of Aix-Marseille
Aix-Marseille University (AMU; french: Aix-Marseille Université; formally incorporated as ''Université d'Aix-Marseille'') is a public research university located in the Provence region of southern France. It was founded in 1409 when Louis II of ...
, at
Luminy
Aix-Marseille University Faculty of Sciences is one of the faculties of Aix-Marseille University. The faculty is divided into seven departments across six campuses. With 8000 students and 1600 staff and faculty it is one of the largest science facu ...
.
Biography
Jean-Yves Girard is an alumnus of the
École normale supérieure de Saint-Cloud.
He made a name for himself in the 1970s with his proof of
strong normalization in a system of
second-order logic
In logic and mathematics, second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. Second-order logic is in turn extended by higher-order logic and type theory.
First-order logic quantifies on ...
called
System F
System F (also polymorphic lambda calculus or second-order lambda calculus) is a typed lambda calculus that introduces, to simply typed lambda calculus, a mechanism of universal quantification over types. System F formalizes parametric polymorph ...
. This result gave a new proof of
Takeuti's conjecture In mathematics, Takeuti's conjecture is the conjecture of Gaisi Takeuti that a sequent formalisation of second-order logic has cut-elimination (Takeuti 1953). It was settled positively:
* By Tait, using a semantic technique for proving cut-elimin ...
, which was proven a few years earlier by
William W. Tait, Motō Takahashi and
Dag Prawitz. For this purpose, he introduced the notion of "reducibility candidate" ("candidat de réducibilité"). He is also credited with the discovery of
Girard's paradox
In mathematical logic, System U and System U− are pure type systems, i.e. special forms of a typed lambda calculus with an arbitrary number of sorts, axioms and rules (or dependencies between the sorts). They were both proved inconsistent by Jea ...
,
linear logic
Linear logic is a substructural logic proposed by Jean-Yves Girard as a refinement of classical and intuitionistic logic, joining the dualities of the former with many of the constructive properties of the latter. Although the logic has also ...
, the
geometry of interaction,
ludics, and (satirically) the mustard watch.
He obtained the
CNRS Silver medal in 1983 and is a member of the
French Academy of Sciences
The French Academy of Sciences (French: ''Académie des sciences'') is a learned society, founded in 1666 by Louis XIV at the suggestion of Jean-Baptiste Colbert, to encourage and protect the spirit of French scientific research. It was at ...
.
Bibliography
*
*
*
* Jean-Yves Girard (2011). ''The Blind Spot: Lectures on Logic''
*
See also
*
Affine logic
References
External links
*
*
*
Journées Jean-Yves Girardweb site of 2007 conference in honour of Girard's 60th birthday
Living people
Proof theorists
French mathematicians
French logicians
ENS Fontenay-Saint-Cloud-Lyon alumni
Members of the French Academy of Sciences
1947 births
French National Centre for Scientific Research scientists
French philosophers
French male non-fiction writers
{{France-mathematician-stub