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

Материал из Wiki - Факультет компьютерных наук
Перейти к: навигация, поиск
(Типы в языках программирования)
(Домашние задания)
Строка 32: Строка 32:
 
== Домашние задания ==
 
== Домашние задания ==
  
* ТДЗ-1 (теоретическое). TBA. [ Условие]. [ Исходник]. Дедлайн: '''TBA'''.
+
* ТДЗ-1 (теоретическое). TBA. [https://drive.google.com/file/d/1KGMBvMlFyfby220n2ITO0yjWcaMRL4Yx/view?usp=drivesdk Условие]. [https://drive.google.com/file/d/1KR1O9FGDCwTDwJoQj2gk6Jqyq8MUs46d/view?usp=drivesdk Исходник]. Дедлайн: '''16 сентября 2024 в 23:59'''.
 
* ТДЗ-2 (теоретическое). TBA. [ Условие]. [ Исходник]. Дедлайн: '''TBA'''.
 
* ТДЗ-2 (теоретическое). TBA. [ Условие]. [ Исходник]. Дедлайн: '''TBA'''.
 
* ТДЗ-3 (теоретическое). TBA. [ Условие]. [ Исходник]. Дедлайн: '''TBA'''.
 
* ТДЗ-3 (теоретическое). TBA. [ Условие]. [ Исходник]. Дедлайн: '''TBA'''.

Версия 19:33, 9 сентября 2024

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

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

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

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

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

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

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

Чат курса (Telegram)

Лекции (Zoom)

Семинары (Zoom)

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

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

[ Оценки]

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

  • Лекция 1, 2 сен 2024. Организация курса; Формальные методы и теория типов; Язык NatBool, его денотационная семантика и здравость системы типов относительно неё. [ Запись].
  • Семинар 1, 2 сен 2024. Операционные семантики; Эквивалентности семантик; Preservation и Progress теоремы; Корректность системы типов относительно операционной семантики. [ Запись].

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

  • ТДЗ-1 (теоретическое). TBA. Условие. Исходник. Дедлайн: 16 сентября 2024 в 23:59.
  • ТДЗ-2 (теоретическое). TBA. [ Условие]. [ Исходник]. Дедлайн: TBA.
  • ТДЗ-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