Тьерри Кокан ( фр. Thierry Coquand ; родился 18 апреля 1961 года ) — французский математик , специалист по теории типов и автоматическому доказательству , создатель исчисления конструкций , соорганизатор программы создания унивалентных оснований математики . Профессор факультета информатики и инженерии Гётеборгского университета .

Биография

Родился в Жальё ( департамент Изер ). В 1980 году окончил парижскую Высшую нормальную школу , в 1982 году сдал ( фр. ) — конкурсный экзамен на право преподавания математики в школах высшей ступени. В 1985 году защитил в INRIA докторскую диссертацию ( PhD ) по информатике под руководством Жерара Юэ . В 1985—1989 годы был приглашённым исследователем INRIA, в 1989 году занимал должность директора по исследованиям ( фр. directeur de recherche ).

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

Научные работы

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

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

Организаторская деятельность

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

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

Член редакционных коллегий журналов и (оба издаются Cambridge University Press ). Рецензент книг по конструктивной алгебре и теории доказательств для издательств Springer-Verlag и Princeton University Press .

Награды и сообщества

В 2008 году стал лауреатом крупной исследовательской премии ( англ. ) за работу по пространствам метризаций ( англ. space of valuations ) .

В 2011 году избран членом ( швед. ).

Основные публикации

• 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 (англ.) // . — 1988. — Vol. 76 , no. 2—3 . — P. 95—120 . — ISSN . — doi : . — основная публикация по исчислению конструкций.
• Thierry Coquand. A semantics of evidence for classical logic (англ.) // . — 1995. — Vol. 60 , no. 1 . — P. 325—337 . — ISSN . — doi : . .
• Thierry Coquand. Sur un théorème de Kronecker concernant les variétés algébriques (фр.) // . — Paris, 2004. — Vol. 338 , n ^o 4 . — P. 291–294 . — ISSN . — doi : .
• Theirry Coquand. // Stanford Encyclopedia of Philosophy . — Stanford : Stanford University Publishing, 2010. — статья о теории типов в Стэнфордской философской энциклопедии .

Примечания

Ссылки

• (англ.) . Дата обращения: 1 марта 2014.