x 1.00
Скачать видео

Семинар 2. Лямбда-исчисление (продолжение). Доказательства в Isabelle

  1. 00:15Типизированное лямбда-исчисление. Синтаксис. Типизация по Чёрчу и по Карри
  2. 03:42Типизация по Карри. Полиморфизм и перегрузка. Сильная нормализация. Полнота по Тьюрингу
  3. 11:51Реализация в Isabelle (код)
  4. 27:31Термы и типы в Isabelle. Type Classes. Реализация в Isabelle (код)
  5. 37:27Схематические переменные. Унификация в Isabelle (теория и код)
  6. 43:55Доказательства в Isabelle. Proof state. Простейший метод. Правила интродукции. Правила элиминации. Примеры (теория и код)
  7. 01:16:09Безопасные и небезопасные правила
  8. 01:17:38Разбор упражнения (код)