Тьерри Кокан

**Тьерри Кокан** (француз телендә: Thierry Coquand; 1961 елның 18 апрелендә туган) — француз математигы, типлар теориясе һәм автоматик исбатлау буенча белгеч, конструкцияләр исәпләве барлыкка китерүчесе, математиканың унивалент нигезләре барлыкка китерү программасының бергә оештыручыларының берсе. Гётеборг университетының информатика һәм инженерия факультетының профессоры.

## Тәрҗемәи хәле
Жальёда (Изер департаменты) туган. 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-енче ел хезмәтләр сериясе нотасыз топологиягә (en. 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 елда метризацияләр пространстволары (ингл. space of valuations) буенча эше өчен Гёдель Җәмгыятенең (ингл. Kurt Gödel Society) эре тикшеренүче премиясенең лауреаты булган..
2011 елда Гётеборгның король фәннәр һәм нәфис сүз җәмгыятенең (швед. Kungliga Vetenskaps- och Vitterhetssamhället i Göteborg) әгъзасы булып сайланган булган.

## Төп публикацияләре
*  — анализ аналога парадокса Бурали-Форти для интуиционистской теории типов Мартин-Лёфа.
*  — основная публикация по исчислению конструкций.
* .
* 
*  — статья о теории типов в Стэнфордской философской энциклопедии.

## Искәрмәләр

## Сылтамалар
* 
Төркем:Әлифба буенча шәхесләр
Төркем:Математиклар