x 1.00
Семинар 1. Введение в Isabelle. Лямбда-исчисление
- 00:15Введение. Формальная верификация
- 04:18Формальное доказательство. Пример
- 10:58Интерактивное доказательство. Isabelle
- 16:13Работа с Isabelle (код)
- 42:10Лямбда-исчисление
- 47:24Бета-редукция
- 52:03Свободные и связанные переменные
- 54:42Нотация де Брауна. Альфа- и эта-конверсии. Равенство лямбда-термов
- 01:00:28Теорема Чёрча — Россера. Каррирование. Применение лямбда-исчисления. Нумералы Чёрча
- 01:05:56Неподвижные точки лямбда-терма. Рекурсия. Эмулятор машины Тьюринга. Парадокс Рассела