!!Thierry Coquand
!Short laudatio by Henk Barendregt 
\\
Thierry Coquand established in his PhD thesis in 1985 the Calculus of Constructions, a landmark in Type/Proof theory.
\\
He designed and co-implemented the Coq Proof Assistant, Coq, extended to the Calculus of Inductive Constructions by Coquand and Ch. Paulin-Mohring. It is the ultimate functional programming language, and a fundamental contribution to certified software.
\\ \\
Thierry Coquand is one of the main leaders of the Type Theory domain. He is also the European leader in the area of formal mathematics.
----

!Any further pages in alphabetic order of their title as created by you.\\

Just click at "Create new page", then type a short title and click OK, then add information on the empty page presented to you (including maybe a picture from your harddisk or a pdf-file by using the "Upload" Button) and finally click at "Save".\\
[{CategoryIndexPlugin category='User/Coquand_Thierry/OtherInformation'}]