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

Материал из Wiki - Факультет компьютерных наук
Перейти к: навигация, поиск
(→‎Лекции и семинары)
(→‎Лекции и семинары)
Строка 19: Строка 19:
 
== Лекции и семинары ==
 
== Лекции и семинары ==
  
−
* '''Лекция 1, 25 сен 2023'''. Организация курса; Формальные методы и теория типов; Язык IntBool.
+
* '''Лекция 1, 25 сен 2023'''. Организация курса; Формальные методы и теория типов; Язык IntBool. [https://disk.yandex.ru/d/zl7DgU7FmuJKLg/%D0%A2%D0%B8%D0%BF%D1%8B%20%D0%B2%20%D1%8F%D0%B7%D1%8B%D0%BA%D0%B0%D1%85%20%D0%BF%D1%80%D0%BE%D0%B3%D1%80%D0%B0%D0%BC%D0%BC%D0%B8%D1%80%D0%BE%D0%B2%D0%B0%D0%BD%D0%B8%D1%8F/%D0%9B%D0%B5%D0%BA%D1%86%D0%B8%D1%8F%2B%D0%A1%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80%202023-09-25T08-11-14Z.mp4 Запись].
−
* '''Семинар 1, 25 сен 2023'''. Денотационная и операционная семантики; Корректность системы типов языка IntBool.
+
* '''Семинар 1, 25 сен 2023'''. Денотационная и операционная семантики; Корректность системы типов языка IntBool. [https://disk.yandex.ru/d/zl7DgU7FmuJKLg/%D0%A2%D0%B8%D0%BF%D1%8B%20%D0%B2%20%D1%8F%D0%B7%D1%8B%D0%BA%D0%B0%D1%85%20%D0%BF%D1%80%D0%BE%D0%B3%D1%80%D0%B0%D0%BC%D0%BC%D0%B8%D1%80%D0%BE%D0%B2%D0%B0%D0%BD%D0%B8%D1%8F/%D0%9B%D0%B5%D0%BA%D1%86%D0%B8%D1%8F%2B%D0%A1%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80%202023-09-25T10-01-30Z.mp4 Запись].
−
* '''Лекция 2, 25 сен 2023'''. Preservation и progress теоремы; Лямбда-исчисление и его Тьюринг-полнота.
+
* '''Лекция 2, 25 сен 2023'''. Preservation и progress теоремы; Лямбда-исчисление и его Тьюринг-полнота. [https://disk.yandex.ru/d/zl7DgU7FmuJKLg/%D0%A2%D0%B8%D0%BF%D1%8B%20%D0%B2%20%D1%8F%D0%B7%D1%8B%D0%BA%D0%B0%D1%85%20%D0%BF%D1%80%D0%BE%D0%B3%D1%80%D0%B0%D0%BC%D0%BC%D0%B8%D1%80%D0%BE%D0%B2%D0%B0%D0%BD%D0%B8%D1%8F/%D0%9B%D0%B5%D0%BA%D1%86%D0%B8%D1%8F%2B%D0%A1%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80%202023-09-25T11-44-16Z.mp4 Запись].
−
* '''Семинар 2, 2 окт 2023'''. Операционная семантика лямбда-исчисления; STLC.
+
* '''Семинар 2, 2 окт 2023'''. Операционная семантика лямбда-исчисления; STLC. [https://disk.yandex.ru/d/zl7DgU7FmuJKLg/%D0%A2%D0%B8%D0%BF%D1%8B%20%D0%B2%20%D1%8F%D0%B7%D1%8B%D0%BA%D0%B0%D1%85%20%D0%BF%D1%80%D0%BE%D0%B3%D1%80%D0%B0%D0%BC%D0%BC%D0%B8%D1%80%D0%BE%D0%B2%D0%B0%D0%BD%D0%B8%D1%8F/%D0%9B%D0%B5%D0%BA%D1%86%D0%B8%D1%8F%2B%D0%A1%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80%202023-10-02T07-55-00Z.mp4 Запись].
−
* '''Лекция 3, 2 окт 2023'''. Теоретико-множественная семантика STLC; Алгебраические типы данных; Соответствие Карри-Говарда.
+
* '''Лекция 3, 2 окт 2023'''. Теоретико-множественная семантика STLC; Алгебраические типы данных; Соответствие Карри-Говарда. [https://disk.yandex.ru/d/zl7DgU7FmuJKLg/%D0%A2%D0%B8%D0%BF%D1%8B%20%D0%B2%20%D1%8F%D0%B7%D1%8B%D0%BA%D0%B0%D1%85%20%D0%BF%D1%80%D0%BE%D0%B3%D1%80%D0%B0%D0%BC%D0%BC%D0%B8%D1%80%D0%BE%D0%B2%D0%B0%D0%BD%D0%B8%D1%8F/%D0%9B%D0%B5%D0%BA%D1%86%D0%B8%D1%8F%2B%D0%A1%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80%202023-10-02T09-56-33Z.mp4 Запись].
−
* '''Семинар 3, 2 окт 2023'''. Доказательства в интуиционистской логике через CHC; Оператор fix и натуральные числа в STLC.
+
* '''Семинар 3, 2 окт 2023'''. Доказательства в интуиционистской логике через CHC; Оператор fix и натуральные числа в STLC. [https://disk.yandex.ru/d/zl7DgU7FmuJKLg/%D0%A2%D0%B8%D0%BF%D1%8B%20%D0%B2%20%D1%8F%D0%B7%D1%8B%D0%BA%D0%B0%D1%85%20%D0%BF%D1%80%D0%BE%D0%B3%D1%80%D0%B0%D0%BC%D0%BC%D0%B8%D1%80%D0%BE%D0%B2%D0%B0%D0%BD%D0%B8%D1%8F/%D0%9B%D0%B5%D0%BA%D1%86%D0%B8%D1%8F%2B%D0%A1%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80%202023-10-02T11-38-54Z.mp4 Запись].
−
* '''Лекция 4, 9 окт 2023'''. Оператор явной типизации; типизация параметров в STLC. Полиморфизм и System F; лямбда-куб.
+
* '''Лекция 4, 9 окт 2023'''. Оператор явной типизации; типизация параметров в STLC. Полиморфизм и System F; лямбда-куб. [https://disk.yandex.ru/d/zl7DgU7FmuJKLg/%D0%A2%D0%B8%D0%BF%D1%8B%20%D0%B2%20%D1%8F%D0%B7%D1%8B%D0%BA%D0%B0%D1%85%20%D0%BF%D1%80%D0%BE%D0%B3%D1%80%D0%B0%D0%BC%D0%BC%D0%B8%D1%80%D0%BE%D0%B2%D0%B0%D0%BD%D0%B8%D1%8F/%D0%9B%D0%B5%D0%BA%D1%86%D0%B8%D1%8F%2B%D0%A1%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80%202023-10-09T08-13-25Z.mp4 Запись].
−
* '''Семинар 4, 9 окт 2023'''. Система типов Хиндли-Милнера, часть 1.
+
* '''Семинар 4, 9 окт 2023'''. Система типов Хиндли-Милнера, часть 1. [https://disk.yandex.ru/d/zl7DgU7FmuJKLg/%D0%A2%D0%B8%D0%BF%D1%8B%20%D0%B2%20%D1%8F%D0%B7%D1%8B%D0%BA%D0%B0%D1%85%20%D0%BF%D1%80%D0%BE%D0%B3%D1%80%D0%B0%D0%BC%D0%BC%D0%B8%D1%80%D0%BE%D0%B2%D0%B0%D0%BD%D0%B8%D1%8F/%D0%9B%D0%B5%D0%BA%D1%86%D0%B8%D1%8F%2B%D0%A1%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80%202023-10-09T09-59-36Z.mp4 Запись].
−
* '''Лекция 5, 9 окт 2023'''. Система типов Хиндли-Милнера, часть 2.
+
* '''Лекция 5, 9 окт 2023'''. Система типов Хиндли-Милнера, часть 2. [https://disk.yandex.ru/d/zl7DgU7FmuJKLg/%D0%A2%D0%B8%D0%BF%D1%8B%20%D0%B2%20%D1%8F%D0%B7%D1%8B%D0%BA%D0%B0%D1%85%20%D0%BF%D1%80%D0%BE%D0%B3%D1%80%D0%B0%D0%BC%D0%BC%D0%B8%D1%80%D0%BE%D0%B2%D0%B0%D0%BD%D0%B8%D1%8F/%D0%9B%D0%B5%D0%BA%D1%86%D0%B8%D1%8F%2B%D0%A1%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80%202023-10-09T11-36-41Z.mp4 Запись].
  
 
== Домашние задания ==
 
== Домашние задания ==
  
 
== Итоговая оценка за курс ==
 
== Итоговая оценка за курс ==

Версия 11:03, 14 октября 2023

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

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

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

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

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

Чат курса (Telegram)

Основные пары (Zoom)

Дополнительные пары (Zoom)

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

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

  • Лекция 1, 25 сен 2023. Организация курса; Формальные методы и теория типов; Язык IntBool. Запись.
  • Семинар 1, 25 сен 2023. Денотационная и операционная семантики; Корректность системы типов языка IntBool. Запись.
  • Лекция 2, 25 сен 2023. Preservation и progress теоремы; Лямбда-исчисление и его Тьюринг-полнота. Запись.
  • Семинар 2, 2 окт 2023. Операционная семантика лямбда-исчисления; STLC. Запись.
  • Лекция 3, 2 окт 2023. Теоретико-множественная семантика STLC; Алгебраические типы данных; Соответствие Карри-Говарда. Запись.
  • Семинар 3, 2 окт 2023. Доказательства в интуиционистской логике через CHC; Оператор fix и натуральные числа в STLC. Запись.
  • Лекция 4, 9 окт 2023. Оператор явной типизации; типизация параметров в STLC. Полиморфизм и System F; лямбда-куб. Запись.
  • Семинар 4, 9 окт 2023. Система типов Хиндли-Милнера, часть 1. Запись.
  • Лекция 5, 9 окт 2023. Система типов Хиндли-Милнера, часть 2. Запись.

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

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

Источник — «http://wiki.cs.hse.ru/index.php?title=Types_23&oldid=80890»