Глеб Красилич//Лямбда-исчисление и Соответствие Карри-Говарда

Дата и время: в 16:20 Докладчик: Глеб Красилич Название: Лямбда-исчисление и Соответствие Карри-Говарда Аннотация: В данном докладе мы попытаемся дать синтаксическое, дедуктивное введение в соответствие Карри -- Говарда для людей с мат. логическим бэкграундом. Я расскажу об основах обычного нетипизированного лямбда-исчисления, расскажу о том как мы можем снабдить наше исчисление системой типов, а также покажу как типизация связана с интуиционистской логикой. Это первый доклад в планируемой серии докладов. В последующих докладах планируется рассказать об основах гомотопической теории типов и формализации математики в системе Agda.