Меню Главная Случайная статья Настройки Кокан, Тьерри Материал из https://ru.wikipedia.org Тьерри Кокан (фр. Thierry Coquand; родился 18 апреля 1961 года) — французский математик, специалист по теории типов и автоматическому доказательству, создатель исчисления конструкций, соорганизатор программы создания унивалентных оснований математики. Профессор факультета информатики и инженерии Гётеборгского университета. Содержание 1 Биография 2 Научные работы 3 Организаторская деятельность 4 Награды и сообщества 5 Основные публикации 6 Примечания 7 Ссылки Биография Родился в Жальё (департамент Изер). В 1980 году окончил парижскую Высшую нормальную школу, в 1982 году сдал «математическую агрегацию» (фр. agrgation de mathmatiques) — конкурсный экзамен на право преподавания математики в школах высшей ступени. В 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 Gdel Society) за работу по пространствам метризаций (англ. space of valuations)[2]. В 2011 году избран членом Королевского общества наук и словесности Гётеборга (швед. Kungliga Vetenskaps- och Vitterhetssamhllet i Gteborg). Основные публикации Thierry Coquand. An analysis of Girard’s paradox (англ.) // Symposium on Logic in Computer Science (LICS’86), Cambridge, MA, 1986. — Cambridge, MA: IEEE, 1986. — P. 227—236. — анализ аналога парадокса Бурали-Форти для интуиционистской теории типов Мартин-Лёфа. Thierry Coquand, Grard Huet. The calculus of constructions (англ.) // Information and Computation[англ.]. — 1988. — Vol. 76, no. 2—3. — P. 95—120. — ISSN 0890-5401. — doi:10.1016/0890-5401(88)90005-3. — основная публикация по исчислению конструкций. Thierry Coquand. A semantics of evidence for classical logic (англ.) // Journal of Symbolic Logic[англ.]. — 1995. — Vol. 60, no. 1. — P. 325—337. — ISSN 0022-4812. — doi:10.2307/2275524.. Thierry Coquand. Sur un thorme de Kronecker concernant les varits algbriques (фр.) // Comptes rendus hebdomadaires des sances de l’Acadmie des sciences[фр.]. — Paris, 2004. — Vol. 338, no 4. — P. 291–294. — ISSN 0001-4036. — doi:10.1016/j.crma.2003.12.008. Theirry Coquand. Type Theory // Stanford Encyclopedia of Philosophy. — Stanford: Stanford University Publishing, 2010. — статья о теории типов в Стэнфордской философской энциклопедии. Примечания Deutsche Nationalbibliothek Record #122538900 // Gemeinsame Normdatei (нем.) — 2012—2016. sa Ekvall. Thierry Coquand has been awarded the Kurt Gdel Centenary Research Prize Fellowship (англ.) (недоступная ссылка — история). University of Gothenburg (6 апреля 2008). Дата обращения: 1 марта 2014. Ссылки Домашняя страница Тьерри Кокана (англ.). Дата обращения: 1 марта 2014.