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

Тьерри Кокан
Thierry Coquand
Место рождения:	Жальё (Франция, департамент Изер)
Страна:	Франция Франция
Научная сфера:	Основания математики, теоретическая информатика
Место работы:	Гётеборгский университет
Учёная степень:	PhD
Учёное звание:	Профессор
Альма-матер:	Высшая нормальная школа (Париж)
Научный руководитель:	Жерар Юэ
Известен как:	Разработчик исчисления конструкций, соорганизатор программы унивалетных оснований математики, исследователь бесточечной топологии
Награды и премии:	Исследовательская премия Общества Гёделя (2008)

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

Биография

Родился в Жальё (департамент Изер). В 1980 году окончил парижскую Высшую нормальную школу, в 1982 году сдал «математическую агрегацию» (фр. agrégation de mathématiques) — конкурсный экзамен на право преподавания математики в школах высшей ступени. В 1985 году защитил в INRIA докторскую диссертацию (PhD) по информатике под руководством Жерара Юэ (фр. Gérard Huet). В 1985—1989 годы был приглашённым исследователем INRIA, в 1989 году занимал должность директора по исследованиям (фр. directeur de recherche).

С 1990 года живёт и работает в Швеции: был приглашённым исследователем в Техническом университете Чалмерса, а с 1996 года — профессор Гётеборгского университета.

Научные работы

Во время работы в середине 1980-х годов с Жераром Юэ разработал исчисление конструкций (англ. calculus of constructions) — полиморфное λ-исчисление высшего порядка с зависимыми типами, занимающее высшую точку в λ-кубе Барендрегта и ставшее впоследствии основой программной системы автоматического доказательства 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).

В 2011 году избран членом Королевского общества наук и словесности Гётеборга (швед. Kungliga Vetenskaps- och Vitterhetssamhället i Göteborg).

Основные публикации

• 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, Gérard Huet The calculus of constructions (англ.) // Information and Computation. — 1988. — Vol. 76, no. 2—3. — P. 95—120. — ISSN [www.sigla.ru/table.jsp?f=8&t=3&v0=0890-5401&f=1003&t=1&v1=&f=4&t=2&v2=&f=21&t=3&v3=&f=1016&t=3&v4=&f=1016&t=3&v5=&bf=4&b=&d=0&ys=&ye=&lng=&ft=&mt=&dt=&vol=&pt=&iss=&ps=&pe=&tr=&tro=&cc=UNION&i=1&v=tagged&s=0&ss=0&st=0&i18n=ru&rlf=&psz=20&bs=20&ce=hJfuypee8JzzufeGmImYYIpZKRJeeOeeWGJIZRrRRrdmtdeee88NJJJJpeeefTJ3peKJJ3UWWPtzzzzzzzzzzzzzzzzzbzzvzzpy5zzjzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzztzzzzzzzbzzzzzzzzzzzzzzzzzzzzzzzzzzzvzzzzzzyeyTjkDnyHzTuueKZePz9decyzzLzzzL*.c8.NzrGJJvufeeeeeJheeyzjeeeeJh*peeeeKJJJJJJJJJJmjHvOJJJJJJJJJfeeeieeeeSJJJJJSJJJ3TeIJJJJ3..E.UEAcyhxD.eeeeeuzzzLJJJJ5.e8JJJheeeeeeeeeeeeyeeK3JJJJJJJJ*s7defeeeeeeeeeeeeeeeeeeeeeeeeeSJJJJJJJJZIJJzzz1..6LJJJJJJtJJZ4....EK*&debug=false 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 [www.sigla.ru/table.jsp?f=8&t=3&v0=0022-4812&f=1003&t=1&v1=&f=4&t=2&v2=&f=21&t=3&v3=&f=1016&t=3&v4=&f=1016&t=3&v5=&bf=4&b=&d=0&ys=&ye=&lng=&ft=&mt=&dt=&vol=&pt=&iss=&ps=&pe=&tr=&tro=&cc=UNION&i=1&v=tagged&s=0&ss=0&st=0&i18n=ru&rlf=&psz=20&bs=20&ce=hJfuypee8JzzufeGmImYYIpZKRJeeOeeWGJIZRrRRrdmtdeee88NJJJJpeeefTJ3peKJJ3UWWPtzzzzzzzzzzzzzzzzzbzzvzzpy5zzjzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzztzzzzzzzbzzzzzzzzzzzzzzzzzzzzzzzzzzzvzzzzzzyeyTjkDnyHzTuueKZePz9decyzzLzzzL*.c8.NzrGJJvufeeeeeJheeyzjeeeeJh*peeeeKJJJJJJJJJJmjHvOJJJJJJJJJfeeeieeeeSJJJJJSJJJ3TeIJJJJ3..E.UEAcyhxD.eeeeeuzzzLJJJJ5.e8JJJheeeeeeeeeeeeyeeK3JJJJJJJJ*s7defeeeeeeeeeeeeeeeeeeeeeeeeeSJJJJJJJJZIJJzzz1..6LJJJJJJtJJZ4....EK*&debug=false 0022-4812]. — DOI:10.2307/2275524..
• Thierry Coquand Sur un théorème de Kronecker concernant les variétés algébriques (фр.) // Comptes rendus hebdomadaires des séances de l’Académie des sciences. — Paris, 2004. — Vol. 338, n^o 4. — P. 291–294. — ISSN [www.sigla.ru/table.jsp?f=8&t=3&v0=0001-4036&f=1003&t=1&v1=&f=4&t=2&v2=&f=21&t=3&v3=&f=1016&t=3&v4=&f=1016&t=3&v5=&bf=4&b=&d=0&ys=&ye=&lng=&ft=&mt=&dt=&vol=&pt=&iss=&ps=&pe=&tr=&tro=&cc=UNION&i=1&v=tagged&s=0&ss=0&st=0&i18n=ru&rlf=&psz=20&bs=20&ce=hJfuypee8JzzufeGmImYYIpZKRJeeOeeWGJIZRrRRrdmtdeee88NJJJJpeeefTJ3peKJJ3UWWPtzzzzzzzzzzzzzzzzzbzzvzzpy5zzjzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzztzzzzzzzbzzzzzzzzzzzzzzzzzzzzzzzzzzzvzzzzzzyeyTjkDnyHzTuueKZePz9decyzzLzzzL*.c8.NzrGJJvufeeeeeJheeyzjeeeeJh*peeeeKJJJJJJJJJJmjHvOJJJJJJJJJfeeeieeeeSJJJJJSJJJ3TeIJJJJ3..E.UEAcyhxD.eeeeeuzzzLJJJJ5.e8JJJheeeeeeeeeeeeyeeK3JJJJJJJJ*s7defeeeeeeeeeeeeeeeeeeeeeeeeeSJJJJJJJJZIJJzzz1..6LJJJJJJtJJZ4....EK*&debug=false 0001-4036]. — DOI:10.1016/j.crma.2003.12.008.
• Theirry Coquand [plato.stanford.edu/entries/type-theory/ Type Theory] // Stanford Encyclopedia of Philosophy. — Stanford: Stanford University Publishing, 2010. — статья о теории типов в Стэнфордской философской энциклопедии.

Ссылки

• [www.cse.chalmers.se/~coquand/ Домашняя страница Тьерри Кокана] (англ.). Проверено 1 марта 2014.

Отрывок, характеризующий Кокан, Тьерри

«Князь Михаил Иларионович! – писал государь от 2 го октября в письме, полученном после Тарутинского сражения. – С 2 го сентября Москва в руках неприятельских. Последние ваши рапорты от 20 го; и в течение всего сего времени не только что ничего не предпринято для действия противу неприятеля и освобождения первопрестольной столицы, но даже, по последним рапортам вашим, вы еще отступили назад. Серпухов уже занят отрядом неприятельским, и Тула, с знаменитым и столь для армии необходимым своим заводом, в опасности. По рапортам от генерала Винцингероде вижу я, что неприятельский 10000 й корпус подвигается по Петербургской дороге. Другой, в нескольких тысячах, также подается к Дмитрову. Третий подвинулся вперед по Владимирской дороге. Четвертый, довольно значительный, стоит между Рузою и Можайском. Наполеон же сам по 25 е число находился в Москве. По всем сим сведениям, когда неприятель сильными отрядами раздробил свои силы, когда Наполеон еще в Москве сам, с своею гвардией, возможно ли, чтобы силы неприятельские, находящиеся перед вами, были значительны и не позволяли вам действовать наступательно? С вероятностию, напротив того, должно полагать, что он вас преследует отрядами или, по крайней мере, корпусом, гораздо слабее армии, вам вверенной. Казалось, что, пользуясь сими обстоятельствами, могли бы вы с выгодою атаковать неприятеля слабее вас и истребить оного или, по меньшей мере, заставя его отступить, сохранить в наших руках знатную часть губерний, ныне неприятелем занимаемых, и тем самым отвратить опасность от Тулы и прочих внутренних наших городов. На вашей ответственности останется, если неприятель в состоянии будет отрядить значительный корпус на Петербург для угрожания сей столице, в которой не могло остаться много войска, ибо с вверенною вам армиею, действуя с решительностию и деятельностию, вы имеете все средства отвратить сие новое несчастие. Вспомните, что вы еще обязаны ответом оскорбленному отечеству в потере Москвы. Вы имели опыты моей готовности вас награждать. Сия готовность не ослабнет во мне, но я и Россия вправе ожидать с вашей стороны всего усердия, твердости и успехов, которые ум ваш, воинские таланты ваши и храбрость войск, вами предводительствуемых, нам предвещают».
Но в то время как письмо это, доказывающее то, что существенное отношение сил уже отражалось и в Петербурге, было в дороге, Кутузов не мог уже удержать командуемую им армию от наступления, и сражение уже было дано.
2 го октября казак Шаповалов, находясь в разъезде, убил из ружья одного и подстрелил другого зайца. Гоняясь за подстреленным зайцем, Шаповалов забрел далеко в лес и наткнулся на левый фланг армии Мюрата, стоящий без всяких предосторожностей. Казак, смеясь, рассказал товарищам, как он чуть не попался французам. Хорунжий, услыхав этот рассказ, сообщил его командиру.
Казака призвали, расспросили; казачьи командиры хотели воспользоваться этим случаем, чтобы отбить лошадей, но один из начальников, знакомый с высшими чинами армии, сообщил этот факт штабному генералу. В последнее время в штабе армии положение было в высшей степени натянутое. Ермолов, за несколько дней перед этим, придя к Бенигсену, умолял его употребить свое влияние на главнокомандующего, для того чтобы сделано было наступление.
– Ежели бы я не знал вас, я подумал бы, что вы не хотите того, о чем вы просите. Стоит мне посоветовать одно, чтобы светлейший наверное сделал противоположное, – отвечал Бенигсен.
Известие казаков, подтвержденное посланными разъездами, доказало окончательную зрелость события. Натянутая струна соскочила, и зашипели часы, и заиграли куранты. Несмотря на всю свою мнимую власть, на свой ум, опытность, знание людей, Кутузов, приняв во внимание записку Бенигсена, посылавшего лично донесения государю, выражаемое всеми генералами одно и то же желание, предполагаемое им желание государя и сведение казаков, уже не мог удержать неизбежного движения и отдал приказание на то, что он считал бесполезным и вредным, – благословил совершившийся факт.


Записка, поданная Бенигсеном о необходимости наступления, и сведения казаков о незакрытом левом фланге французов были только последние признаки необходимости отдать приказание о наступлении, и наступление было назначено на 5 е октября.
4 го октября утром Кутузов подписал диспозицию. Толь прочел ее Ермолову, предлагая ему заняться дальнейшими распоряжениями.
– Хорошо, хорошо, мне теперь некогда, – сказал Ермолов и вышел из избы. Диспозиция, составленная Толем, была очень хорошая. Так же, как и в аустерлицкой диспозиции, было написано, хотя и не по немецки:
«Die erste Colonne marschiert [Первая колонна идет (нем.) ] туда то и туда то, die zweite Colonne marschiert [вторая колонна идет (нем.) ] туда то и туда то» и т. д. И все эти колонны на бумаге приходили в назначенное время в свое место и уничтожали неприятеля. Все было, как и во всех диспозициях, прекрасно придумано, и, как и по всем диспозициям, ни одна колонна не пришла в свое время и на свое место.
Когда диспозиция была готова в должном количестве экземпляров, был призван офицер и послан к Ермолову, чтобы передать ему бумаги для исполнения. Молодой кавалергардский офицер, ординарец Кутузова, довольный важностью данного ему поручения, отправился на квартиру Ермолова.
– Уехали, – отвечал денщик Ермолова. Кавалергардский офицер пошел к генералу, у которого часто бывал Ермолов.
– Нет, и генерала нет.
Кавалергардский офицер, сев верхом, поехал к другому.
– Нет, уехали.
«Как бы мне не отвечать за промедление! Вот досада!» – думал офицер. Он объездил весь лагерь. Кто говорил, что видели, как Ермолов проехал с другими генералами куда то, кто говорил, что он, верно, опять дома. Офицер, не обедая, искал до шести часов вечера. Нигде Ермолова не было и никто не знал, где он был. Офицер наскоро перекусил у товарища и поехал опять в авангард к Милорадовичу. Милорадовича не было тоже дома, но тут ему сказали, что Милорадович на балу у генерала Кикина, что, должно быть, и Ермолов там.