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

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

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

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

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

Страна:

Франция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: Katalog der 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.

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