Томас Штрайхер

Томас Штрайхер (род. 1958) — австрийский математик, профессор математики в Техническом университете Дармштадта . Он получил докторскую степень в 1988 году в Университете Пассау под руководством Манфреда Броя .

Работа

Его исследовательские интересы включают категориальную логику , теорию предметных областей и теорию типов Мартина-Лёфа .

В совместной работе с Мартином Хофманном он построил модель интенсиональной теории типов Мартина-Лёфа , в которой тождественные типы интерпретируются как группоиды . Это была первая модель с нетривиальными типами тождеств, т.е. отличными от множеств . На основе этой работы изучались и другие модели с нетривиальными тождественными типами, в том числе теория гомотопических типов , которая была предложена в качестве основы математики в Владимира Воеводского исследовательской программе «Унивалентные основы математики» .

Вместе с Мартином Хофманном он получил премию LICS Test-of-Time Award 2014 за статью: Модель группоида опровергает уникальность доказательств идентичности .

Библиография

• Т. Штрайхер (1991), Семантика теории типов: результаты корректности, полноты и независимости , Birkhäuser Boston. ISBN   3764335947
• М. Хофманн и Т. Штрейхер (1996), Группоидная интерпретация теории типов , в книге Самбин, Джованни (редактор) и др., Двадцать пять лет конструктивной теории типов. Материалы конгресса, Венеция, Италия, 19–21 октября 1995 г.
• Т. Штрейхер (2006), Теоретико-предметные основы функционального программирования , World Scientific Pub Co Inc. ISBN   9812701427

Внешние ссылки

• Официальный сайт Технического университета Дармштадта
• Томас Штрайхер в проекте «Математическая генеалогия»