Видеозаписи по курсу «Теория языков программирования» 2015/16 (4 курс ФИИТ)

Поддержка учебных курсов ФИИТ, 4 курс
#3

По какой-то странной причине видео попало в категорию “Транспорт” на ютубе :car:

1 лайк
#4

Ясно, почему: после изучения этого курса в любую зарубежную магистратуру/аспирантуру возьмут без разговоров.

4 лайка
#5

Действительно, исправила, спасибо!

#6

Опубликованы видео лекции 5: часть 1, часть 2.

Первые две трети части 1 получились плохие :weary: Камера не сфокусировалась. Я добавила в эту часть небольшие текстовые вставки на случай, если доска совсем неразборчива.

#7

Видео весёлой конфетной лекции 6: часть 1, часть 2.

1 лайк
#8

Видео семинара 2:

  • часть 1 (бинарное дерево с элементом в корне, области видимости, хвостовая рекурсия);
  • часть 2 (реализация состояния для операционной семантики языка IMPe на SML, использование абстрактных типов для реализации синтаксиса IMPe).
#9

Видео лекции 7:

  • часть 1 (операционная семантика с малым шагом для IMPe: условный оператор, оператор цикла while, выполнение программы);
  • часть 2 (краткий обзор истории теории типов, роль типов в языках программирования).
#10

Видео лекции 8 (целиком):
терминатор и человечки в программах, статический и динамический этапы работы с программой, ошибки времени выполнения, система типов. Типы и правила типизации для языка SNB, единственность типа, свойство типобезопасности.

#11

Запись семинара 3:
отношение типизации и тайпчекер, недетерминированное отношение одношагового вычисления;
расширение языка SNB операторами для строк.

#12

Видео лекции 9:

  • часть 1 (разбор доказательств по индукции из контрольной; диалог «что такое тип?»; единственность типа терма, типизируемость подтермов);
  • часть 2 (доказательство типобезопасности языка SNB через теоремы о сохранении и продвижении).

Видео лекции 10:

  • часть 1 (второй способ доказательства теоремы о сохранении; коротко о Lex/Yacc для SML);
  • часть 2 (бестиповое лямбда-исчисление: синтаксис, области видимости, свободные и связанные переменные).
1 лайк
#13

Видео лекции 11:

  • часть 1 (синтаксическое равенство термов, альфа-конверсия и альфа-эквивалентность термов, функция переименования переменной в терме);
  • [часть 2] (https://www.youtube.com/watch?v=1X9FEGzT4vM&list=PL9zS4WrYQCg5hNEoeITwn99XCvaL1Lixy&index=27) (вычисление функций, бета-редукция, стратегии бета-редукции, операционная семантика лямбда-исчисления для стратегии вызова по значению).
2 лайка
#14

Видео семинара 4:

  • часть 1 (переименование связанных переменных, операционная семантика лямбда-исчисления для полной редукции, булевы константы Чёрча);
  • часть 2 (нумералы Чёрча, рекурсия).

В последней части семинара про рекурсию и Z-комбинатор я чушь какую-то написала, пытаясь показать, что Z-комбинатор действительно комбинатор неподвижной точки. Комментарии смотри здесь.

#15

2 posts were merged into an existing topic: (4 курс ФИИТ) Теория языков программирования

#16

Видео лекции 12:

  • часть 1 (оператор неподвижной точки для стратегии вызова по значению, экстенсиональность, эта-редукция; операция подстановки термов);
  • часть 2 (простое типизированное лямбда-исчисление: типы, термы, контекст типизации, правила вывода для отношения типизации).
1 лайк
(4 курс ФИИТ) Теория языков программирования
#17

Видео лекции 13:

  • часть 1 (типобезопасность: напоминание; лемма об инверсии отношения типизации; лемма о единственности типа термов; невозможность типизации комбинатора омега; лемма о канонических формах);
  • часть 2 (доказательство теоремы о продвижении для STLC).
1 лайк
#18

Видео семинара 5.

Правила типизации для типа Unit. Операционная семантика и правила типизации конструкции последовательного связывании. Последовательное связывание как синтаксический сахар.

1 лайк
#19

Видео лекции 14 (18.04.2016):

  • часть 1 (теорема о сохранении для простого типизированного лямбда-исчисления);
  • часть 2 (завершимость вычислений термов простого типизированного лямбда-исчисления).
1 лайк
#20

Видео лекции 15:

  • часть 1 (реконструкция типов, типовые переменные, подстановка типов);
  • часть 2 (композиция подстановок,более и менее конкретные подстановки);
1 лайк
#21

Видео последней в этом году лекции 16: правила типизации с ограничениями, обзор алгоритма вывода типов, алгоритм унификации ограничений Хиндли-Милнера, введение в полиморфное лямбда-исчисление.

#22

Видео бонусной лекции о соответствии Карри-Ховарда.