Кокан, Тьерри
французский учёный в области информатики и логики Из Википедии, свободной энциклопедии
французский учёный в области информатики и логики Из Википедии, свободной энциклопедии
Тьерри Кокан (фр. Thierry Coquand; родился 18 апреля 1961 года) — французский математик, специалист по теории типов и автоматическому доказательству, создатель исчисления конструкций, соорганизатор программы создания унивалентных оснований математики. Профессор факультета информатики и инженерии Гётеборгского университета.
| Тьерри Кокан | |
|---|---|
| фр. Thierry Coquand | |
.jpg) | |
| Дата рождения | 18 апреля 1961[1] (63 года) |
| Место рождения | Жальё (Франция, департамент Изер) |
| Страна |
 Франция |
| Род деятельности | математик, специалист в области информатики, инженер |
| Научная сфера | Основания математики, теоретическая информатика |
| Место работы | Гётеборгский университет |
| Альма-матер | Высшая нормальная школа (Париж) |
| Учёная степень | PhD |
| Учёное звание | Профессор |
| Научный руководитель | Жерар Юэ |
| Известен как | Разработчик исчисления конструкций, соорганизатор программы унивалетных оснований математики, исследователь бесточечной топологии |
| Награды и премии | Исследовательская премия Общества Гёделя (2008) |
 Медиафайлы на Викискладе | |
Родился в Жальё (департамент Изер). В 1980 году окончил парижскую Высшую нормальную школу, в 1982 году сдал «математическую агрегацию» (фр. agrégation de mathématiques) — конкурсный экзамен на право преподавания математики в школах высшей ступени. В 1985 году защитил в INRIA докторскую диссертацию (PhD) по информатике под руководством Жерара Юэ. В 1985—1989 годы был приглашённым исследователем INRIA, в 1989 году занимал должность директора по исследованиям (фр. directeur de recherche).
С 1990 года живёт и работает в Швеции: был приглашённым исследователем в Техническом университете Чалмерса, а с 1996 года — профессор Гётеборгского университета.
Во время работы в середине 1980-х годов с Жераром Юэ разработал исчисление конструкций — полиморфное λ-исчисление высшего порядка с зависимыми типами, занимающее высшую точку в λ-кубе Барендрегта и ставшее впоследствии основой программной системы автоматического доказательства Coq. (В названии «Coq» скрыты как акроним исчисления конструкций — CoC, так и первая часть фамилии Кокана.)
Основные публикации по теории типов и автоматическому доказательству. Серия трудов 1990-х — 2000-х годов посвящена бесточечной топологии (англ. pointless topology) и конструктивной алгебре.
Член программного комитета XIV Международного конгресса по логике, методологии и философии (2011, Нанси).
Совместно с Владимиром Воеводским и Стивом Ауди (англ. Steve Awodey) стал соорганизатором специальной исследовательской программы 2012—2013 академического года в Институте перспективных исследований, посвящённой унивалентным основаниям математики, в её рамках принял участие в совместном создании книги «Гомотопическая теория типов: унивалентные основания математики», в которой изложены основные результаты программы.
Член редакционных коллегий журналов Journal of Functional Programming[англ.] и 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).
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.
