Постновогодняя встреча сообщества функциональных программистов посвященная логическому программированию.
|
|
Антон Трунов "Что нам стоит терм построить: конструктивистская логика и функциональное программирование" Привет! Немного о себе для анонса. Область интересов: формальные методы, функциональное программирование, зависимые типы, автоматизированное доказательство теорем, теория языков программирования. |
Участвую в проекте по формальной верификации языка программирования смарт-контрактов криптовалюты Tezos.
Тезисы:
- Конструктивистская логика — это гуманно!
- Натуральная дедукция, изоморфизм Говарда-Кёрри: неужели успеем разобраться?
- Мифы о конструктивистской логике и их разоблачение
- Закон исключённого третьего и Проблема останова
- Двойное отрицание как монада
- Где используется конструктивистская логика?
Если будет получаться, то постараюсь сделать доклад более интерактивным. Возможно, попробую объяснять не при помощи слайдов, а открыть сессию Coq и доказывать некоторые вещи в "прямом эфире".
Официальный сайт события
https://spb-fp-meetup.timepad.ru/event/432028/