Теория типов и альтернативные основания математики

Теория типов — сравнительно молодая область на стыке математической логики, теории категорий и компьютерных наук. Появившись как один из вариантов разрешения парадоксов наивной теории множеств, системы типов нашли неожиданное применение в языках программирования как средство легковесной верификации как пользовательского кода, так и программных оптимизаций. Кроме этого, системы типов естественным образом обеспечивают конструктивный и, более того, синтетический подход к математике (синтетическая (дифференциальная) геометрия, синтетическая топология, синтетическая теория гомотопий и т.д.) В особенности, гомотопическая теория типов (HoTT) претендует на статус альтернативного основания (конструктивной) математики.
В рамках данного доклада будет изложена история становления теории типов как самостоятельной дисциплины с изложением основных математических результатов, начиная с Principia Mathematica Бертрана Рассела и заканчивая сегодняшними наиболее активными направлениями исследований.