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

Материал из Wiki - Факультет компьютерных наук
Перейти к: навигация, поиск
(→‎Лекции и семинары)
(→‎Домашние задания)
Строка 48: Строка 48:
 
* ТДЗ-1 (теоретическое). Система типов IntBool+Let. [https://drive.google.com/file/d/1e5iTyjbkPKIABjm4tQHwdzMoW1OVYoma/view?usp=drive_link Условие]. [https://drive.google.com/file/d/1gkqzoSl_h1E2pDWnNn3kDfkN76AeWf8n/view?usp=drive_link Исходник]. Дедлайн: '''26 сентября 2024 в 23:59'''.
 
* ТДЗ-1 (теоретическое). Система типов IntBool+Let. [https://drive.google.com/file/d/1e5iTyjbkPKIABjm4tQHwdzMoW1OVYoma/view?usp=drive_link Условие]. [https://drive.google.com/file/d/1gkqzoSl_h1E2pDWnNn3kDfkN76AeWf8n/view?usp=drive_link Исходник]. Дедлайн: '''26 сентября 2024 в 23:59'''.
 
* ТДЗ-2 (теоретическое). Тьюринг-полнота нетипизированного лямбда-исчисления. [https://drive.google.com/file/d/13SsC9fjrJwqGT4d5wqcL7zMdwbbaW43_/view?usp=drive_link Условие]. [https://drive.google.com/file/d/1mlBWX8HIrGEsP40NCK1Q9mbqhw9LvLIr/view?usp=drive_link Исходник]. Дедлайн: '''30 сентября 2024 в 23:59'''.
 
* ТДЗ-2 (теоретическое). Тьюринг-полнота нетипизированного лямбда-исчисления. [https://drive.google.com/file/d/13SsC9fjrJwqGT4d5wqcL7zMdwbbaW43_/view?usp=drive_link Условие]. [https://drive.google.com/file/d/1mlBWX8HIrGEsP40NCK1Q9mbqhw9LvLIr/view?usp=drive_link Исходник]. Дедлайн: '''30 сентября 2024 в 23:59'''.
−
* ТДЗ-3 (теоретическое). TBA. [ Условие]. [ Исходник]. Дедлайн: '''TBA'''.
+
* ТДЗ-3 (теоретическое). Алгебраические типы данных и соответствие Карри-Говарда. [https://drive.google.com/file/d/1lloVL7bqNmihxQOfCBp-7U7u3mzQTXNR/view?usp=sharing Условие]. [https://drive.google.com/file/d/1wLlLtCkHWNQ9OOLB4kkJHTWj2C-8Ktn9/view?usp=sharing Исходник]. Дедлайн: '''18 октября 2024 в 23:59'''.
 
* ПДЗ-1 (практическое). TBA. [ Условие]. Дедлайн: '''TBA'''.
 
* ПДЗ-1 (практическое). TBA. [ Условие]. Дедлайн: '''TBA'''.
 
* ПДЗ-2 (практическое). TBA. [ Условие]. Дедлайн: '''TBA'''.
 
* ПДЗ-2 (практическое). TBA. [ Условие]. Дедлайн: '''TBA'''.

Версия 23:02, 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 (теоретическое). Алгебраические типы данных и соответствие Карри-Говарда. Условие. Исходник. Дедлайн: 18 октября 2024 в 23:59.
  • ПДЗ-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=86762»