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

[juliet]

На страничке курса в Moodle в разделе Материалы висит ссылка на плейлист с видеолекциями. В котором уже опубликованы часть 1 и часть 2 лекции 3.

[juliet]

Видео сонной предпраздничной лекции 4 опубликовано: часть 1, часть 2.

[geo2a]

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

[bravit]

(4 курс ФИИТ) Теория языков программирования

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

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

[juliet]

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

[juliet]

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

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

[juliet]

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

[juliet]

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

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

[juliet]

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

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

[juliet]

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

[juliet]

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

[juliet]

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

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

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

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

[juliet]

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

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

[juliet]

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

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

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

[juliet]

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

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

[juliet]

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

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

[juliet]

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

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

[juliet]

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

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

[juliet]

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

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