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


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

Родился в Жальё (департамент Изер). В 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, Нанси).