Исследовательская группа

Лаборатория языковых инструментов

Соответствие Карри-Говарда-Ламбека и однородные доказательства

September 9

Соответствие Карри-Говарда (формулы как типы, доказательства как программы) -- крайне популярное наблюдение о тесной связи оснований математики и информатики. Появившись в середине прошлого века, оно породило бум различных интерпретаций, применений и обобщений, который активно продолжается и сейчас. При этом расширение идет в двух направлениях: всё новые и новые логические и вычислительные системы связываются между собой, а также к соответствию добавляются новые измерения, удлинняя при этом название факта (так что для полноты картины сегодня стоило бы говорить о соответствии Карри-Говарда-Ламбека-Скотта-Тарского-Стоуна-Воеводского, но мы воздержимся от этого и ограничимся первыми тремя фамилиями)

В первой части доклада мы обсудим это знаменитое соответствие, в частности его теоретико-категориальную сторону. Во второй части мы рассмотрим одно конкретное его применение -- в области логического программирования -- и заодно познакомимся с понятием однородных доказательств (uniform proofs) -- теоретической основой логических языков программирования.


Докладчик: Дмитрий Розплохас

Материалы