Кокан, Тьерри

Родился 18 апреля 1961 года в Жальё (департамент Изер).

В 1980 году окончил парижскую Высшую нормальную школу.

В 1982 году получил право преподавания математики в высших учебных заведениях.

С 1985 по 1989 год — приглашённый исследователь Национального института исследований в информатике и автоматике, в 1989 году — директор по исследованиям (фр. directeur de recherche).

В 1990 году перебрался в Швецию. Являлся приглашённым исследователем в Техническом университете Чалмерса, с 1996 года — профессор Гётеборгского университета.

В 2011 году избран членом Королевского общества наук и словесности Гётеборга.

Член редакционных коллегий журналов Journal of Functional Programming и Mathematical Structures in Computer Science (издательство Cambridge University Press). Рецензент книг по конструктивной алгебре и теории доказательств для издательств Springer-Verlag и Princeton University Press.

Доктор философии по информатике. В 1985 году защитил диссертацию в INRIA под руководством Жерара Юэ.

Совместно с Жераром Юэ разработал исчисление конструкций — полиморфное λ-исчисление высшего порядка с зависимыми типами, занимающее высшую точку в λ-кубе Барендрегта и ставшее впоследствии основой программной системы автоматического доказательства Coq. (В названии «Coq» скрыты как акроним исчисления конструкций — CoC, так и первая часть фамилии Кокана.)

Основные публикации посвящены теории типов и автоматическому доказательству. Серия трудов 1990-х — 2000-х годов посвящена бесточечной топологии и конструктивной алгебре.

Член программного комитета XIV Международного конгресса по логике, методологии и философии (2011, Нанси).

Совместно с Владимиром Воеводским и Стивом Ауди стал соорганизатором специальной исследовательской программы 2012—2013 академического года в Институте перспективных исследований, посвящённой унивалентным основаниям математики, в её рамках принял участие в совместном создании книги «Гомотопическая теория типов: унивалентные основания математики», в которой изложены основные результаты программы.

• Thierry Coquand. An analysis of Girard’s paradox (англ.) // Symposium on Logic in Computer Science (LICS’86), Cambridge, MA, 1986. — Cambridge, MA: IEEE, 1986. — P. 227—236. — анализ аналога парадокса Бурали-Форти для интуиционистской теории типов Мартин-Лёфа.
• Thierry Coquand, Gérard Huet. The calculus of constructions (англ.) // Information and Computation. — 1988. — Vol. 76, no. 2—3. — P. 95—120. — ISSN 0890-5401. — doi:10.1016/0890-5401(88)90005-3. — основная публикация по исчислению конструкций.
• Thierry Coquand. A semantics of evidence for classical logic (англ.) // Journal of Symbolic Logic. — 1995. — Vol. 60, no. 1. — P. 325—337. — ISSN 0022-4812. — doi:10.2307/2275524..
• Thierry Coquand. Sur un théorème de Kronecker concernant les variétés algébriques (фр.) // Comptes rendus hebdomadaires des séances de l’Académie des sciences. — Paris, 2004. — Vol. 338, n^o 4. — P. 291–294. — ISSN 0001-4036. — doi:10.1016/j.crma.2003.12.008.
• Theirry Coquand. Type Theory // Stanford Encyclopedia of Philosophy. — Stanford: Stanford University Publishing, 2010. — статья о теории типов в Стэнфордской философской энциклопедии.

• Премия Общества Гёделя за работу по пространствам метризаций (2008)^[2];
• Премия Ассоциации вычислительной техники (2013).