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


#1

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


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

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


#3

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


#4

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


#5

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


#6

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

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


#7

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


#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 (бестиповое лямбда-исчисление: синтаксис, области видимости, свободные и связанные переменные).

#13

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

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

#14

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

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

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


#15

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


#16

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

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

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

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

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

#18

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

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


#19

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

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

#20

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

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