L. D. Beklemishev, S. L. Kuznetsov. Computational proof theory and lambda calculus

SEMINARS

L. D. Beklemishev, S. L. Kuznetsov. Computational proof theory and lambda calculus
September 30, 2019–May 12, 2020, Steklov Mathematical Institute, room 530, 8 Gubkina St., Moscow

Financial support. The course is supported by the Ministry of Science and Higher Education of the Russian Federation (the grant to the Steklov International Mathematical Center, agreement no. 075-15-2019-1614).

RSS: Forthcoming seminars

Lecturers
Beklemishev Lev Dmitrievich
Kuznetsov Stepan Lvovich

Organizations
Steklov Mathematical Institute of Russian Academy of Sciences, Moscow
Steklov International Mathematical Center

L. D. Beklemishev, S. L. Kuznetsov. Computational proof theory and lambda calculus, Steklov Mathematical Institute, room 530, 8 Gubkina St., Moscow, September 30, 2019–May 12, 2020

Lecture 21. Applications of functional interpretation. Interpretation by absence of counterexample. T system models L. D. Beklemishev May 12, 2020 16:30 Steklov Mathematical Institute, room 530, 8 Gubkina St., Moscow, online
Лекция 20. Гёделевская система Т. Интерпретация формальной арифметики в Т (продолжение) L. D. Beklemishev April 28, 2020 16:30 Steklov Mathematical Institute, room 530, 8 Gubkina St., Moscow
Лекция 19. Гёделевская система $Т$. Функциональная интерпретация интуиционистской арифметики в $Т$ L. D. Beklemishev April 21, 2020 Steklov Mathematical Institute, room 530, 8 Gubkina St., Moscow, online
Лекция 18. Интуиционистская арифметика L. D. Beklemishev April 14, 2020 16:30 Steklov Mathematical Institute, room 530, 8 Gubkina St., Moscow, online
Лекция 17. Примитивно рекурсивная арифметика L. D. Beklemishev April 7, 2020 Steklov Mathematical Institute, room 530, 8 Gubkina St., Moscow, online
Лекция 16. Негативная интерпретация классической логики в интуиционистской L. D. Beklemishev March 26, 2020 16:00 Steklov Mathematical Institute, room 530, 8 Gubkina St., Moscow
Лекция 15. Интуиционистское исчисление предикатов. Гильбертовский и генценовский формат. Теорема об устранении сечения. Дизъюнктивное и экзистенциальное свойства интуиционистской логики. L. D. Beklemishev March 23, 2020 16:30 Steklov Mathematical Institute, room 530, 8 Gubkina St., Moscow
Лекция 14. Полные частично упорядоченные множества. Модель Скотта $D_\infty$. S. L. Kuznetsov March 16, 2020 16:30 Steklov Mathematical Institute, room 530, 8 Gubkina St., Moscow
Лекция 13. Слабо экстенсиональные лямбда-алгебры. Модель Плоткина $\mathcal{P}\omega$. L. D. Beklemishev March 2, 2020 16:30 Steklov Mathematical Institute, room 530, 8 Gubkina St., Moscow
Лекция 12. Комбинаторные алгебры, лямбда-алгебры. L. D. Beklemishev February 17, 2020 16:30 Steklov Mathematical Institute, room 530, 8 Gubkina St., Moscow
Лекция 11. Модели лямбда-исчисления L. D. Beklemishev, S. L. Kuznetsov February 10, 2020 16:30 Steklov Mathematical Institute, room 530, 8 Gubkina St., Moscow
Лекция 10. Комбинаторная логика L. D. Beklemishev December 9, 2019 16:30 Steklov Mathematical Institute, room 530, 8 Gubkina St., Moscow
Лекция 9. Полнота типового лямбда-исчисления относительно теоретико-множественной семантики S. L. Kuznetsov December 2, 2019 16:30 Steklov Mathematical Institute, room 530, 8 Gubkina St., Moscow
Лекция 8. Теорема о сильной нормализуемости для типового лямбда-исчисления (окончание). Теоретико-множественная семантика типового лямбда-исчисления S. L. Kuznetsov November 25, 2019 16:30 Steklov Mathematical Institute, room 530, 8 Gubkina St., Moscow
Лекция 7. Алгоритм выведения наиболее общего типа в системе Карри (окончание). Теорема о сильной нормализуемости для типового лямбда-исчисления S. L. Kuznetsov November 18, 2019 16:30 Steklov Mathematical Institute, room 530, 8 Gubkina St., Moscow
Лекция 6. Алгоритм выведения наиболее общего типа в системе Карри S. L. Kuznetsov November 11, 2019 16:30 Steklov Mathematical Institute, room 530, 8 Gubkina St., Moscow
Лекция 5. Сохранение типа при бета-редукции. Интуиционистская логика высказываний, соответствие Карри - Говарда S. L. Kuznetsov October 28, 2019 16:30 Steklov Mathematical Institute, room 530, 8 Gubkina St., Moscow
Лекция 4. Свойство Чёрча - Россера (окончание). Типовое лямбда исчисление: типизации по Чёрчу и по Карри S. L. Kuznetsov October 21, 2019 16:30 Steklov Mathematical Institute, room 530, 8 Gubkina St., Moscow
Лекция 3. Представимость вычислимых функций в бестиповом лямбда-исчислении. Свойство Чёрча - Россера S. L. Kuznetsov October 14, 2019 Steklov Mathematical Institute, room 530, 8 Gubkina St., Moscow
Лекция 2. Теорема о неподвижной точке. Представимость примитивно-рекурсивных функций в бестиповом лямбда-исчислении S. L. Kuznetsov October 7, 2019 Steklov Mathematical Institute, room 530, 8 Gubkina St., Moscow
Лекция 1.Введение. Бестиповое лямбда-исчисление. Представление натуральных чисел в бестиповом лямбда-исчислении L. D. Beklemishev, S. L. Kuznetsov September 30, 2019 Steklov Mathematical Institute, room 530, 8 Gubkina St., Moscow