Зиборов К.В.-Формальная семантика и верификация ПО- Семинар 1.Введение в Isabelle.Лямбда-исчисление

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