Thierry Coquand

Thierry Coquand (* 18. April 1961 in Jallieu, Département Isère) ist ein französischer Mathematiker und Informatiker.

Thierry Coquand, 2006

Leben

Coquand studierte ab 1980 an der Ecole Normale Superieure und absolvierte die Agrégation 1982 (als Bester). 1985 wurde er an der Universität Paris VII bei Gérard Huet promoviert (Une théorie des Constructions). Als Postdoktorand war er an der Carnegie Mellon University (1985) und forschte ab 1985 für das INRIA, an dem er 1990 Forschungsdirektor wurde. Ab 1990 war er Gastwissenschaftler und ab 1991 Forschungsassistent am Chalmers Institute of Technology und 1996 Professor an der Universität Göteborg. Er ist der Begründer des Calculus of Constructions (Konstruktionskalkül, auch Kalkül induktiver Konstruktionen CIC), einer Form der Typentheorie die im Beweisassistenten Coq verwendet wird (der Name der Sprache steht auch für seine Initialen). Es spielte auch in der Entwicklung der univalenten Grundlegung der Mathematik von Wladimir Wojewodski in der zweiten Hälfte der 2000er Jahre eine wichtige Rolle. Neben mathematischer Logik befasst er sich mit Computeralgebra.

2010 erhielt er einen Advanced Grant der ERC. 2011 wurde er Mitglied der Königlichen Gesellschaft der Wissenschaften in Göteborg und der Academia Europaea. 2007/08 war er Junior Fellow am Institut Universitaire de France und 2011 wurde er Mitglied im Rat der Association for Symbolic Logic. 2005 war er Skolem Lecturer in Oslo und 2001 erhielt er den Wallmarska Preis der Königlich Schwedischen Akademie der Wissenschaften. Für die Entwicklung von Coq erhielt er mit Gérard Huet, Christine Paulin-Mohring (Christine Paulin), Bruno Barras, Jean-Christophe Filliâtre, Hugo Herbelin, Chet Murthy, Yves Bertot, Pierre Castéran 2013 den ACM Software System Award. 2022 erhielt er einen weiteren Advanced Grant des ERC.

Schriften

• mit G. Huet: The calculus of constructions, Information and Computation, Bd. 76, 1988, S. 95–120.
• mit G. Huet: The calculus of constructions, Technical Report 530. INRIA, Centre de Rocquencourt, 1986, Online
• mit 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 (Hrsg.), 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.
• mit A. Spiwack: A proof of strong normalisation using domain theory, Logical Method in Computer Science, Band 3 (4), 2007
• Sur un théoreme de Kronecker concernant les variétées algébriques, Compte Rendu Acad. Sci. Paris, Ser. 1, Band 338, 2004, S. 291–294
• mit H. Lombardi, C. Quitte: Generating non Noetherian Modules constructively, Manuscripta Math., Band 115, 2004, S. 513–520

Weblinks

• Website am Chalmers Institute
• Curriculum Vitae for Thierry Coquand (PDF)
• Thierry Coquand in der Datenbank zbMATH