Русская Википедия:Кокан, Тьерри
Шаблон:Однофамильцы Шаблон:Учёный Тьерри Кокан (Шаблон:Lang-fr; родился 18 апреля 1961 года) — французский Шаблон:Математик, специалист по теории типов и автоматическому доказательству, создатель исчисления конструкций, соорганизатор программы создания унивалентных оснований математики. Профессор факультета информатики и инженерии Гётеборгского университета.
Биография
Родился в Жальё (департамент Изер). В 1980 году окончил парижскую Высшую нормальную школу, в 1982 году сдал Шаблон:Нп2 — конкурсный экзамен на право преподавания математики в школах высшей ступени. В 1985 году защитил в INRIA докторскую диссертацию (PhD) по информатике под руководством Жерара Юэ. В 1985—1989 годы был приглашённым исследователем INRIA, в 1989 году занимал должность директора по исследованиям (Шаблон:Lang-fr).
С 1990 года живёт и работает в Швеции: был приглашённым исследователем в Техническом университете Чалмерса, а с 1996 года — профессор Гётеборгского университета.
Научные работы
Во время работы в середине 1980-х годов с Жераром Юэ разработал исчисление конструкций — полиморфное λ-исчисление высшего порядка с зависимыми типами, занимающее высшую точку в λ-кубе Барендрегта и ставшее впоследствии основой программной системы автоматического доказательства Coq. (В названии «Coq» скрыты как акроним исчисления конструкций — CoC, так и первая часть фамилии Кокана.)
Основные публикации по теории типов и автоматическому доказательству. Серия трудов 1990-х — 2000-х годов посвящена Шаблон:Нп2 и конструктивной алгебре.
Организаторская деятельность
Член программного комитета XIV Международного конгресса по логике, методологии и философии (2011, Нанси).
Совместно с Владимиром Воеводским и Шаблон:Нп2 стал соорганизатором специальной исследовательской программы 2012—2013 академического года в Институте перспективных исследований, посвящённой унивалентным основаниям математики, в её рамках принял участие в совместном создании книги «Гомотопическая теория типов: унивалентные основания математики», в которой изложены основные результаты программы.
Член редакционных коллегий журналов Шаблон:Iw и Mathematical Structures in Computer Science (оба издаются Cambridge University Press). Рецензент книг по конструктивной алгебре и теории доказательств для издательств Springer-Verlag и Princeton University Press.
Награды и сообщества
В 2008 году стал лауреатом крупной исследовательской премии Шаблон:Нп2 за работу по пространствам метризаций (Шаблон:Lang-en)[1].
В 2011 году избран членом Шаблон:Нп2.
Основные публикации
- Шаблон:Статья — анализ аналога парадокса Бурали-Форти для интуиционистской теории типов Мартин-Лёфа.
- Шаблон:Статья — основная публикация по исчислению конструкций.
- Шаблон:Статья.
- Шаблон:Статья
- Шаблон:Статья — статья о теории типов в Стэнфордской философской энциклопедии.
Примечания
Ссылки