Зиборов К.В. - Формальная семантика и верификация ПО - Семинар 2. Доказательства в Isabelle

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