Types 24 — различия между версиями
Материал из Wiki - Факультет компьютерных наук
TurtlePU (обсуждение | вклад) (→Полезные ссылки) |
TurtlePU (обсуждение | вклад) (→Лекции и семинары) |
||
| Строка 27: | Строка 27: | ||
== Лекции и семинары == | == Лекции и семинары == | ||
| − | * '''Лекция 1, 2 сен 2024'''. Организация курса; Формальные методы и теория типов; Язык NatBool, его денотационная семантика и здравость системы типов относительно неё. [ Запись]. | + | * '''Лекция 1, 2 сен 2024'''. Организация курса; Формальные методы и теория типов; Язык NatBool, его денотационная семантика и здравость системы типов относительно неё. [https://disk.yandex.ru/d/WhHJyFeb9mDdkA/02.09%20%D0%BB%D0%B5%D0%BA%D1%86%D0%B8%D1%8F.mp4 Запись]. |
| − | * '''Семинар 1, 2 сен 2024'''. Операционные семантики; Эквивалентности семантик; Preservation и Progress теоремы; Корректность системы типов относительно операционной семантики. [ Запись]. | + | * '''Семинар 1, 2 сен 2024'''. Операционные семантики; Эквивалентности семантик; Preservation и Progress теоремы; Корректность системы типов относительно операционной семантики. [https://disk.yandex.ru/d/WhHJyFeb9mDdkA/02.09%20%D1%81%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80.mp4 Запись]. |
| + | * '''Лекция 2, 9 сен 2024'''. [https://disk.yandex.ru/d/WhHJyFeb9mDdkA/09.09%20%D0%BB%D0%B5%D0%BA%D1%86%D0%B8%D1%8F.mp4 Запись]. | ||
| + | * '''Семинар 2, 9 сен 2024'''. [https://disk.yandex.ru/d/WhHJyFeb9mDdkA/09.09%20%D1%81%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80.mp4 Запись]. | ||
== Домашние задания == | == Домашние задания == | ||
Версия 13:42, 13 сентября 2024
Содержание
Типы в языках программирования
Осенний курс по выбору для студентов 3 и 4 курсов ПМИ ФКН ВШЭ.
Лектор: Павел Соколов aka @TurtlePU.
Семинарист: Илья Григорьев aka @ilyagribun.
Ассистент: Яна Ике aka @jijasan.
Полезные ссылки
classroom для сдачи теоретических домашних заданий
Лекции и семинары
- Лекция 1, 2 сен 2024. Организация курса; Формальные методы и теория типов; Язык NatBool, его денотационная семантика и здравость системы типов относительно неё. Запись.
- Семинар 1, 2 сен 2024. Операционные семантики; Эквивалентности семантик; Preservation и Progress теоремы; Корректность системы типов относительно операционной семантики. Запись.
- Лекция 2, 9 сен 2024. Запись.
- Семинар 2, 9 сен 2024. Запись.
Домашние задания
- ТДЗ-1 (теоретическое). TBA. Условие. Исходник. Дедлайн: 16 сентября 2024 в 23:59.
- ТДЗ-2 (теоретическое). TBA. [ Условие]. [ Исходник]. Дедлайн: TBA.
- ТДЗ-3 (теоретическое). TBA. [ Условие]. [ Исходник]. Дедлайн: TBA.
- ПДЗ-1 (практическое). TBA. [ Условие]. Дедлайн: TBA.
- ПДЗ-2 (практическое). TBA. [ Условие]. Дедлайн: TBA.
- БТДЗ (бонусное теоретическое). TBA. [ Условие]. [ Исходник]. Дедлайн: TBA.
- ПДЗ-3 (практическое). TBA. [ Условие]. Дедлайн: TBA.
- ПДЗ-4 (практическое). TBA. [ Условие]. Дедлайн: TBA.
- БПДЗ (бонусное практическое). TBA. [ Условие]. Дедлайн: TBA.
- ТДЗ-4 (теоретическое). TBA. [ Условие]. [ Исходник]. Дедлайн: TBA.
Условие теоретических домашних заданий скомпилировано с помощью pdfLaTeX.
Итоговая оценка за курс
Итог = Округление(0.4 * ТДЗ + 0.6 * ПДЗ + Б),
где ТДЗ – средняя оценка за теоретические домашние задания, ПДЗ – за практические, а Б – сумма бонусных баллов, полученных за курс.
Округление арифметическое.
Литература
Основная литература
- Benjamin C. Pierce, Types and Programming Languages
- Frank Pfenning, Lecture Notes on Bidirectional Type Checking
- Jean-Yves Girard, Proofs and Types
