JetBrains Research — наука, меняющая мир

Интуиционистская теория типов

Интуиционистская теория типов (также конструктивная теория типов или теория типов Мартина-Лёфа) является универсальной системой, которая призвана играть такую же роль для конструктивной математики, как теория множеств Цермело-Френкеля для классической математики. Она основана на принципе "высказывания как типы" и проясняет интерпретацию Брауэра-Гейтинга-Колмогорова интуиционистской логики. Она расширяет эту интерпретацию до более общего взгляда интуиционистской теории типов и, таким образом, дает общее представление не только о том, что такое конструктивное доказательство, но и о том, что такое конструктивный математический объект. Основная идея состоит в том, что математические понятия, такие как элементы, множества и функции, объясняются в терминах понятий из программирования, таких как структуры данных, типы данных и программы. На семинаре будет обсуждаться формальная система интуиционистской теории типов и её семантические основы.

Докладчик: Александр Мисонижник

11.03.2019, 17:15.

Место: ауд. 3248, мат-мех. факультет СПбГУ, Старый Петергоф, Университетский пр-т, д. 28