Курсы Лекторы Материалы О проекте
Курсы Лекторы Материалы О проекте
Войти
Семинар 1. Введение в Isabelle. Лямбда-исчисление
Лекция из курса:
Формальная семантика и верификация программного обеспечения
Видео не может быть загружено из-за проблем с интернет-соединением или проблем на сервере. Или формат файла не поддерживается вашим браузером.
Семинар 1. Введение в Isabelle. Лямбда-исчисление
Видео закончится через
NaN:NaN
00:00
00:00
00:15
Следующая секция начнется через 04:18
Введение. Формальная верификация
04:18
Следующая секция начнется через 04:18
Формальное доказательство. Пример
10:58
Следующая секция начнется через 04:18
Интерактивное доказательство. Isabelle
16:13
Следующая секция начнется через 04:18
Работа с Isabelle (код)
42:10
Следующая секция начнется через 04:18
Лямбда-исчисление
47:24
Следующая секция начнется через 04:18
Бета-редукция
52:03
Следующая секция начнется через 04:18
Свободные и связанные переменные
54:42
Следующая секция начнется через 04:18
Нотация де Брауна. Альфа- и эта-конверсии. Равенство лямбда-термов
1:00:28
Следующая секция начнется через 04:18
Теорема Чёрча — Россера. Каррирование. Применение лямбда-исчисления. Нумералы Чёрча
1:05:56
Следующая секция начнется через 04:18
Неподвижные точки лямбда-терма. Рекурсия. Эмулятор машины Тьюринга. Парадокс Рассела
Свернуть таймкоды
00:00
00:00
Скорость
x 1.00
x 0.25
x 0.50
x 0.75
x 1.00
x 1.25
x 1.5
x 1.75
x 2.00
x 3.00
x 4.00
Качество
1080p
1080p
720p
480p
00:00
00:00
Скорость
x 1.00
x 0.25
x 0.50
x 0.75
x 1.00
x 1.25
x 1.5
x 1.75
x 2.00
x 3.00
x 4.00
Качество
1080p
1080p
720p
480p

Семинар 1. Введение в Isabelle. Лямбда-исчисление

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