Глеб Красилич//Зависимые типы и автоматическая проверка доказательств (продолжение)

Дата и время: 27.01.2023 в 16:20

Докладчик: Глеб Красилич

Название: Зависимые типы и автоматическая проверка доказательств(продолжение)


Аннотация:
Данный доклад (а точнее серия из двух докладов) продолжает
тему доклада
"Лямбда-исчисление и Соответствие Карри-Говарда" от 23.09.2022
прошлый раз мы обсудили, как типизированное лямбда-исчисления связано
с логикой. Сейчас же мы рассмотрим Гомотопическую теорию типов (а
точнее ее "негомотопический" фрагмент, похожий на классическую теорию
типов Мартин-Лёфа): очень выразительное типизированное исчисление,
пригодное для формализации содержательной математики. Будут даны
основные определения, мотивировки, показано как мы можем формализовать
математические рассуждения пользуясь парадигмой "типы как
утверждения", и, пожалуй
самое главное, мы будем "программировать" математические
доказательства на языке Agda, используя его в качестве системы
автоматической проверки доказательств.