Types 26

Материал из Wiki - Факультет компьютерных наук
Версия от 06:07, 7 сентября 2026; TurtlePU (обсуждение | вклад) (Новая страница: «== Типы в языках программирования == Осенний курс по выбору для студентов 3 и 4 курсов ПМИ ФКН ВШЭ. '''Лектор''': Павел Соколов aka [https://t.me/TurtlePU @TurtlePU]. '''Семинарист''': Илья Григорьев aka [https://t.me/ilyagribun @ilyagribun]. '''Ассистент''': Илья Ткемаладзе aka [https://t.me/intttik @intttik]. == П...»)
(разн.) ← Предыдущая версия | Текущая версия (разн.) | Следующая версия → (разн.)
Перейти к навигации Перейти к поиску

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

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

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

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

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

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

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

Чат курса (Telegram)

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

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

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

[ Оценки]

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

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

  • Лекция 1, 7 сен 2026. TBA. [ Конспект]. [ Запись].
  • Семинар 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. [ Конспект]. [ Запись].

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

  • Домашние задания будут как теоретические, так и практические. Планируется бонусное теоретическое и бонусное практическое домашние задания.

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

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

Итог = Округление(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=97264