Types 26

Материал из Wiki - Факультет компьютерных наук
Перейти к навигации Перейти к поиску

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

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

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

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

Ассистент: Илья Ткемаладзе aka @intttik.

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

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

Чат курса (Telegram)

[ Записи занятий]

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

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

Оценки

В отличие от предыдущих лет, ссылки на онлайн-трансляцию будут отличаться от занятия к занятию и публиковаться в канале курса.

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

  • Лекция 1, 7 сен 2026. Язык NatBool+Let и его денотационная семантика. Типы как носители смысла. Конспект.
  • Семинар 1, 14 сен 2026. TBA. [ Конспект]. [ Запись].
  • Лекция 2, 14 сен 2026. TBA. [ Конспект]. [ Запись].
  • Семинар 2, ??? 2026. TBA. [ Конспект]. [ Запись].
  • Лекция 3, 21 сен 2026. TBA. [ Конспект]. [ Запись].
  • Семинар 3, 21 сен 2026. TBA. [ Конспект]. [ Запись].
  • Лекция 4, 28 сен 2026. TBA. [ Конспект]. [ Запись].
  • Семинар 4, 28 сен 2026. TBA. [ Конспект]. [ Запись].
  • Лекция 5, 5 окт 2026. TBA. [ Конспект]. [ Запись].
  • Семинар 5, 5 окт 2026. TBA. [ Конспект]. [ Запись].
  • Лекция 6, 12 окт 2026. TBA. [ Конспект]. [ Запись].
  • Семинар 6, 12 окт 2026. TBA. [ Конспект]. [ Запись].
  • Лекция 7, 19 окт 2026. TBA. [ Конспект]. [ Запись].
  • Семинар 7, 19 окт 2026. TBA. [ Конспект]. [ Запись].
  • Лекция 8, 2 ноя 2026. TBA. [ Конспект]. [ Запись].
  • Семинар 8, 2 ноя 2026. TBA. [ Конспект]. [ Запись].
  • Лекция 9, 9 ноя 2026. TBA. [ Конспект]. [ Запись].
  • Семинар 9, 9 ноя 2026. TBA. [ Конспект]. [ Запись].
  • Лекция 10, 16 ноя 2026. TBA. [ Конспект]. [ Запись].
  • Семинар 10, 16 ноя 2026. TBA. [ Конспект]. [ Запись].
  • Лекция 11, 23 ноя 2026. TBA. [ Конспект]. [ Запись].
  • Семинар 11, 23 ноя 2026. TBA. [ Конспект]. [ Запись].
  • Лекция 12, 30 ноя 2026. TBA. [ Конспект]. [ Запись].
  • Семинар 12, 30 ноя 2026. TBA. [ Конспект]. [ Запись].
  • Лекция 13, 7 дек 2026. TBA. [ Конспект]. [ Запись].
  • Семинар 13, 7 дек 2026. TBA. [ Конспект]. [ Запись].
  • Лекция 14, 14 дек 2026. TBA. [ Конспект]. [ Запись].
  • Семинар 14, 14 дек 2026. TBA. [ Конспект]. [ Запись].

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

Теоретические домашние задания выкладываются на платформе Google Classroom по ссылке. Условие теоретических домашних заданий скомпилировано с помощью pdfLaTeX.

Практические домашние задания выкладываются на платформе TBA по [ ссылке].

  • ТДЗ-1 (теоретическое). Система IntBool+Let. Условие. Исходник. Дедлайн: 28 сентября в 23:59.
  • ДЗ-2 (TBA). TBA. [ TBA]. Дедлайн: TBA в 23:59.
  • ДЗ-3 (TBA). TBA. [ TBA]. Дедлайн: TBA в 23:59.
  • ДЗ-4 (TBA). TBA. [ TBA]. Дедлайн: TBA в 23:59.
  • ДЗ-5 (TBA). TBA. [ TBA]. Дедлайн: TBA в 23:59.
  • ДЗ-6 (TBA). TBA. [ TBA]. Дедлайн: TBA в 23:59.
  • ДЗ-7 (TBA). TBA. [ TBA]. Дедлайн: TBA в 23:59.
  • ДЗ-8 (TBA). TBA. [ TBA]. Дедлайн: TBA в 23:59.
  • ДЗ-9 (TBA). TBA. [ TBA]. Дедлайн: TBA в 23:59.
  • ДЗ-10 (TBA). TBA. [ TBA]. Дедлайн: TBA в 23:59.

Итоговая оценка за курс

Итог = Округление(0.4 * ТДЗ + 0.4 * ПДЗ + 0.2 * Э + Б),

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

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

Литература

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

  1. Benjamin C. Pierce, Types and Programming Languages
  2. Frank Pfenning, Lecture Notes on Bidirectional Type Checking
  3. Jean-Yves Girard, Proofs and Types
  4. Philip Wadler, Wen Kokke, Jeremy G. Siek, Programming Language Foundations in Agda

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

  1. Benjamin C. Pierce, Advanced Topics in Types and Programming Languages
  2. Lectures on the Curry-Howard Isomorphism
  3. The Twelf Project
  4. Programming Language and Theorem Prover – Lean
  5. The Granule Project
  6. Arend Theorem Prover
Источник — https://wiki.cs.hse.ru/index.php?title=Types_26&oldid=97342