 | Тема этой статьи может не соответствовать общему руководству Википедии о известности . ( февраль 2015 г. ) (Узнайте, как и когда удалить этот шаблон сообщения ) |
Томас Streicher (1958 года рождения) является немецкий математик , который является профессором математики в Техническом университете Дармштадта . Он получил докторскую степень в 1988 году из Университета Пассау с советником Манфред Брой .
Работа [ править ]
Его научные интересы включают в себя категорическое логики , теории домена и теории типа Мартин-LOF .
В совместной работе с Мартином Хофманном он построил модель интенсиональной теории типов Мартина-Лёфа, в которой типы идентичности интерпретируются как группоиды . Это была первая модель с нетривиальными типами идентичности, т.е. отличными от множеств . На основе этой работы [1] были изучены другие модели с нетривиальными типами тождества, включая теорию гомотопических типов, которая была предложена в качестве основы математики в исследовательской программе Владимира Воеводского Univalent Foundations of Mathematics .
Вместе с Мартином Хофманном он получил награду LICS Test-of-Time в 2014 году за статью «Группоидная модель опровергает уникальность доказательств идентичности».
Библиография [ править ]
- Т. Штрейхер (1991), Семантика теории типов: результаты правильности, полноты и независимости , Birkhäuser Boston. ISBN 3764335947
- М. Хофманн и Т. Штрейхер (1996), Группоидная интерпретация теории типов , в Самбине, Джованни (ред.) И др., Двадцать пять лет конструктивной теории типов. Материалы конгресса, Венеция, Италия, 19–21 октября 1995 г.
- T. Streicher (2006), Теоретико-предметные основы функционального программирования , World Scientific Pub Co Inc., ISBN 9812701427
Ссылки [ править ]
- ^ Awodey, Steve (2010). «Теория типов и гомотопия». arXiv : 1010,1810 . CS1 maint: обескураженный параметр ( ссылка )
Внешние ссылки [ править ]
- Официальный веб - сайт в Technische Universität Дармштадта
- Томас Штрейхер на проекте « Математическая генеалогия»
