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

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


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



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


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

09.09.2019, 17:15.

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