Курсы Лекторы Материалы О проекте
Курсы Лекторы Материалы О проекте
Войти
Семинар 2. Лямбда-исчисление (продолжение). Доказательства в Isabelle
Лекция из курса:
Формальная семантика и верификация программного обеспечения
Видео не может быть загружено из-за проблем с интернет-соединением или проблем на сервере. Или формат файла не поддерживается вашим браузером.
Семинар 2. Лямбда-исчисление (продолжение). Доказательства в Isabelle
Видео закончится через
NaN:NaN
00:00
00:00
00:15
Следующая секция начнется через 03:42
Типизированное лямбда-исчисление. Синтаксис. Типизация по Чёрчу и по Карри
03:42
Следующая секция начнется через 03:42
Типизация по Карри. Полиморфизм и перегрузка. Сильная нормализация. Полнота по Тьюрингу
11:51
Следующая секция начнется через 03:42
Реализация в Isabelle (код)
27:31
Следующая секция начнется через 03:42
Термы и типы в Isabelle. Type Classes. Реализация в Isabelle (код)
37:27
Следующая секция начнется через 03:42
Схематические переменные. Унификация в Isabelle (теория и код)
43:55
Следующая секция начнется через 03:42
Доказательства в Isabelle. Proof state. Простейший метод. Правила интродукции. Правила элиминации. Примеры (теория и код)
1:16:09
Следующая секция начнется через 03:42
Безопасные и небезопасные правила
1:17:38
Следующая секция начнется через 03:42
Разбор упражнения (код)
Свернуть таймкоды
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

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

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