Types 26

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

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

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

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

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

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

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

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

Чат курса (Telegram)

Лекции (Яндекс.Телемост)

[ Семинары (Яндекс.Телемост)]

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

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

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

Оценки

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

  • Лекция 1, 7 сен 2026. Язык NatBool+Let и его денотационная семантика. Типы как носители смысла. Доска.
  • Семинар 1, 14 сен 2026. Операционная семантика NatBool+Let и свойство Чёрча-Россера. Доска. [ Запись].
  • Лекция 2, 15 сен 2026. TBA. [ Доска]. [ Запись].
  • Семинар 2, 21 сен 2026. TBA. [ Доска]. [ Запись].
  • Лекция 3, 21 сен 2026. TBA. [ Доска]. [ Запись].
  • Семинар 3, 22 сен 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=97591