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