Types 24 — различия между версиями

Материал из Wiki - Факультет компьютерных наук
Перейти к: навигация, поиск
(→‎Лекции и семинары)
(→‎Лекции и семинары)
Строка 31: Строка 31:
 
* '''Лекция 2, 9 сен 2024'''. Система типов NatBool+Let. Подстановка. Соглашение об именах. Preservation и progress теоремы. [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'''. Система типов NatBool+Let. Подстановка. Соглашение об именах. Preservation и progress теоремы. [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'''. Семантика с кучей. Эквивалентность семантик с подстановкой и с кучей. Корректность системы типов NatBool+Let. [https://disk.yandex.ru/d/WhHJyFeb9mDdkA/09.09%20%D1%81%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80.mp4 Запись].
 
* '''Семинар 2, 9 сен 2024'''. Семантика с кучей. Эквивалентность семантик с подстановкой и с кучей. Корректность системы типов NatBool+Let. [https://disk.yandex.ru/d/WhHJyFeb9mDdkA/09.09%20%D1%81%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80.mp4 Запись].
−
* '''Лекция 3, 16 сен 2024'''. Нетипизированное лямбда-исчисление. Стратегии редукции. Теорема Чёрча-Россера. [ Запись].
+
* '''Лекция 3, 16 сен 2024'''. Нетипизированное лямбда-исчисление. Стратегии редукции. Теорема Чёрча-Россера. [https://disk.yandex.ru/d/WhHJyFeb9mDdkA/%D0%9B%D0%B5%D0%BA%D1%86%D0%B8%D1%8F%202024-09-16T11-56-36Z.mp4 Запись].
−
* '''Семинар 3, 16 сен 2024'''. Кодирование Чёрча для типов данных: логические значения, пары, натуральные числа, списки. Комбинатор неподвижной точки. [ Запись].
+
* '''Семинар 3, 16 сен 2024'''. Кодирование Чёрча для типов данных: логические значения, пары, натуральные числа, списки. Комбинатор неподвижной точки. [https://disk.yandex.ru/d/WhHJyFeb9mDdkA/%D0%A1%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80%202024-09-16T15-02-10Z.mp4 Запись].
 
* '''Лекция 4, 23 сен 2024'''. Просто типизированное лямбда-исчисление. Доказательство слабой нормализуемости. [ Запись].
 
* '''Лекция 4, 23 сен 2024'''. Просто типизированное лямбда-исчисление. Доказательство слабой нормализуемости. [ Запись].
 
* '''Семинар 4, 23 сен 2024'''. Теоретико-множественная семантика STLC. Логическая семантика STLC. Пустой тип. [ Запись].
 
* '''Семинар 4, 23 сен 2024'''. Теоретико-множественная семантика STLC. Логическая семантика STLC. Пустой тип. [ Запись].

Версия 23:00, 26 сентября 2024

Типы в языках программирования

Осенний курс по выбору для студентов 3 и 4 курсов ПМИ ФКН ВШЭ.

Лектор: Павел Соколов aka @TurtlePU.

Семинарист: Илья Григорьев aka @ilyagribun.

Ассистент: Яна Ике aka @jijasan.

Полезные ссылки

Канал курса (Telegram)

Чат курса (Telegram)

Лекции (Zoom)

Семинары (Zoom)

Записи занятий (Я.Диск)

classroom для сдачи теоретических домашних заданий

Оценки

Лекции и семинары

  • Лекция 1, 2 сен 2024. Организация курса; Формальные методы и теория типов; Язык NatBool, его денотационная семантика и здравость системы типов относительно неё. Запись.
  • Семинар 1, 2 сен 2024. Операционные семантики; Эквивалентности семантик; Preservation и Progress теоремы; Корректность системы типов относительно операционной семантики. Запись.
  • Лекция 2, 9 сен 2024. Система типов NatBool+Let. Подстановка. Соглашение об именах. Preservation и progress теоремы. Запись.
  • Семинар 2, 9 сен 2024. Семантика с кучей. Эквивалентность семантик с подстановкой и с кучей. Корректность системы типов NatBool+Let. Запись.
  • Лекция 3, 16 сен 2024. Нетипизированное лямбда-исчисление. Стратегии редукции. Теорема Чёрча-Россера. Запись.
  • Семинар 3, 16 сен 2024. Кодирование Чёрча для типов данных: логические значения, пары, натуральные числа, списки. Комбинатор неподвижной точки. Запись.
  • Лекция 4, 23 сен 2024. Просто типизированное лямбда-исчисление. Доказательство слабой нормализуемости. [ Запись].
  • Семинар 4, 23 сен 2024. Теоретико-множественная семантика STLC. Логическая семантика STLC. Пустой тип. [ Запись].
  • Лекция 5, 30 сен 2024. TBA. [ Запись].
  • Семинар 5, 30 сен 2024. TBA. [ Запись].
  • Лекция 6, 7 окт 2024. TBA. [ Запись].
  • Семинар 6, 7 окт 2024. TBA. [ Запись].
  • Лекция 7, 14 окт 2024. TBA. [ Запись].
  • Семинар 7, 14 окт 2024. TBA. [ Запись].
  • Лекция 8, 21 окт 2024. TBA. [ Запись].
  • Семинар 8, 21 окт 2024. TBA. [ Запись].

Домашние задания

  • ТДЗ-1 (теоретическое). Система типов IntBool+Let. Условие. Исходник. Дедлайн: 26 сентября 2024 в 23:59.
  • ТДЗ-2 (теоретическое). Тьюринг-полнота нетипизированного лямбда-исчисления. Условие. Исходник. Дедлайн: 30 сентября 2024 в 23:59.
  • ТДЗ-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 * ПДЗ + Б),

где ТДЗ – средняя оценка за теоретические домашние задания, ПДЗ – за практические, а Б – сумма бонусных баллов, полученных за курс.

Округление арифметическое.

Литература

Основная литература

  1. Benjamin C. Pierce, Types and Programming Languages
  2. Frank Pfenning, Lecture Notes on Bidirectional Type Checking
  3. Jean-Yves Girard, Proofs and Types

Дополнительная литература

  1. Lectures on the Curry-Howard Isomorphism
  2. The Twelf Project
  3. Programming Language and Theorem Prover – Lean
  4. The Granule Project
Источник — «http://wiki.cs.hse.ru/index.php?title=Types_24&oldid=86761»