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

Материал из Википедии — свободной энциклопедии
Перейти к: навигация, поиск
Тьерри Кокан
Thierry Coquand
Thierry Coquand.jpg
Дата рождения:

18 апреля 1961({{padleft:1961|4|0}}-{{padleft:4|2|0}}-{{padleft:18|2|0}})[1] (53 года)

Место рождения:

Жальё (Франция, департамент Изер)

Страна:

ФранцияFlag of France.svg Франция

Научная сфера:

Основания математики, теоретическая информатика

Место работы:

Гётеборгский университет

Учёная степень:

PhD

Учёное звание:

Профессор

Альма-матер:

Высшая нормальная школа (Париж)

Научный руководитель:

Жерар Юэ[fr]

Известен как:

Разработчик исчисления конструкций, соорганизатор программы унивалетных оснований математики, исследователь бесточечной топологии

Награды и премии


Исследовательская премия Общества Гёделя (2008)

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

Биография[править | править вики-текст]

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

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

Научные работы[править | править вики-текст]

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

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

Организаторская деятельность[править | править вики-текст]

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

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

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

Награды и сообщества[править | править вики-текст]

В 2008 году стал лауреатом крупной исследовательской премии Общества Гёделя (англ. Kurt Gödel Society) за работу по пространствам метризаций (англ. space of valuations)[2].

В 2011 году избран членом Королевского общества наук и словесности Гётеборга (швед. Kungliga Vetenskaps- och Vitterhetssamhället i Göteborg).

Основные публикации[править | править вики-текст]

Примечания[править | править вики-текст]

  1. Record #122538900 // Gemeinsame NormdateiLeipzig: Deutschen Nationalbibliothek, 2012—2014. Проверено 14 мая 2014.
  2. Åsa Ekvall. Thierry Coquand has been awarded the Kurt Gödel Centenary Research Prize Fellowship (англ.). University of Gothenburg (6 April 2008). Проверено 1 марта 2014.

Ссылки[править | править вики-текст]