Thierry Coquand

Thierry Coquand (born April 18, 1961 in Jallieu , Département Isère ) is a French mathematician and computer scientist.

Life

Coquand studied from 1980 at the Ecole Normale Superieure and graduated from the Agrégation in 1982 (best). In 1985 he received his doctorate from the University of Paris VII under Gérard Huet ( Une théorie des Constructions ). He was a postdoctoral fellow at Carnegie Mellon University (1985) and researched for INRIA from 1985 , where he became director of research in 1990. From 1990 he was visiting scientist and from 1991 research assistant at the Chalmers Institute of Technology and 1996 professor at the University of Gothenburg . He is the founder of the Calculus of Constructions (construction calculus, also calculus of inductive constructions CIC), a form of type theory that is used in the proof assistant Coq (the name of the language also stands for his initials). It also played an important role in the development of the univalent foundation of mathematics by Vladimir Voievodsky in the second half of the 2000s. In addition to mathematical logic, he deals with computer algebra.

In 2010 he received an Advanced Grant from the ERC. In 2011 he became a member of the Royal Society of Science in Gothenburg and the Academia Europaea . In 2007/08 he was a Junior Fellow at the Institut Universitaire de France and in 2011 he became a member of the Council of the Association for Symbolic Logic. In 2005 he was a Skolem Lecturer in Oslo and in 2001 he received the Wallmarska Prize from the Royal Swedish Academy of Sciences . For the development of Coq he received the 2013 ACM Software System Award with Gérard Huet , Christine Paulin-Mohring (Christine Paulin), Bruno Barras , Jean-Christophe Filliâtre , Hugo Herbelin , Chet Murthy , Yves Bertot , Pierre Castéran .

Fonts

with G. Huet: The calculus of constructions, Information and Computation, Vol. 76, 1988, pp. 95-120.
with G. Huet: The calculus of constructions, Technical Report 530. INRIA, Center de Rocquencourt, 1986, online
with Ch. Paulin-Mohring: Inductively defined types. Lecture Notes in Computer Science (LNCS) 417, COLOG-88.
Constructions: A higher order proof system for mechanizing mathematics, LNCS, Proceeding of Eurocal 1985.
Pattern matching with dependent types. Proceedings of the Workshop on Types for Proofs and Programs, 1992.
An analysis of Girard's paradox, LICS - ACM / IEEE Symposium on Logic in Computer Science 1986.
Metamathematical investigations of a calculus of constructions. In P. Odifreddi (Ed.), Logic and Computer Science. Academic Press, 1990.
A semantics of evidence for classical logic, Journal of Symbolic Logic, 1995.
An Analysis of Girard's paradox, LICS 1986.
with A. Spiwack: A proof of strong normalization using domain theory, Logical Method in Computer Science, Volume 3 (4), 2007
Sur un théoreme de Kronecker concernant les variétées algébriques, Compte Rendu Acad. Sci. Paris, Ser. 1, Volume 338, 2004, pp. 291-294
with H. Lombardi, C. Quitte: Generating non Noetherian Modules constructively, Manuscripta Math., Volume 115, 2004, pp. 513-520

Web links

Individual evidence

personal data
SURNAME	Coquand, Thierry
BRIEF DESCRIPTION	French mathematician and computer scientist
DATE OF BIRTH	April 18, 1961
PLACE OF BIRTH	Jallieu , Isère department

[1] Thierry Coquand in the Mathematics Genealogy Project (English)

[2] Membership directory: Thierry Coquand. Academia Europaea, accessed October 13, 2017 .