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

Дата и время: 20.01.2023 в 16:20 Докладчик: Глеб Красилич Название: Зависимые типы и автоматическая проверка доказательств Литература: Homotopy Type Theory: Univalent Foundations of Mathematics (https://homotopytypetheory.org/book/). Appendix A1 и A2 содержит выписанные правила вывода гомотопической теории типов и комментарии к ним. Аннотация: Данный доклад (а точнее серия из двух докладов) продолжает тему доклада "Лямбда-исчисление и Соответствие Карри-Говарда" от 23.09.2022 (https://youtube.com/watch?v=vEXdBZB7eG4&si=EnSIkaIECMiOmarE). В прошлый раз мы обсудили, как типизированное лямбда-исчисления связано с логикой. Сейчас же мы рассмотрим Гомотопическую теорию типов (а точнее ее "негомотопический" фрагмент, похожий на классическую теорию типов Мартин-Лёфа): очень выразительное типизированное исчисление, пригодное для формализации содержательной математики. Будут даны основные определения, мотивировки, показано как мы можем формализовать математические рассуждения пользуясь парадигмой "типы как утверждения", и, пожалуй самое главное, мы будем "программировать" математические доказательства на языке Agda, используя его в качестве системы автоматической проверки доказательств.