Бакалавриат
2019/2020
Типы в языках программирования
Лучший по критерию «Полезность курса для расширения кругозора и разностороннего развития»
Лучший по критерию «Новизна полученных знаний»
Статус:
Курс по выбору (Прикладная математика и информатика)
Направление:
01.03.02. Прикладная математика и информатика
Кто читает:
Департамент информатики
Когда читается:
3-й курс, 3 модуль
Формат изучения:
без онлайн-курса
Преподаватели:
Москвин Денис Николаевич
Язык:
русский
Кредиты:
4
Контактные часы:
44
Программа дисциплины
Аннотация
Является дисциплиной по выбору.Данная дисциплина направлена на овладение навыками понимания и выведения систем типов различных языков программирования. В результате освоения дисциплины студент должен: знать способы описания типов в языках программирования; уметь выводить типы для конкретного языка; владеть математическим аппаратом и инструментальными средствами, используемым в описании систем типов.
Цель освоения дисциплины
- Целями освоения дисциплины «Типы в языках программирования» являются формирование у студентов теоретических знаний и практических навыков понимания и выведения систем типов различных языков программирования.
Планируемые результаты обучения
- Знает понятие простого типизированного лямбда- исчисления. Применяет теоремы о продвижении и сохранении типа для решения поставленных задач. Владеет навыками вычисления населенности различных систем типов.
- Знает устройство систем типов языков программирования и общие подходы к проектированию таких систем. Формализует синтаксис, операционную семантику и отношение типизации для вычислительной системы в виде набора правил. Владеет навыками доказательства сохранения полезных свойств при безопасных расширениях типов.
- Владеет понятием полиморфные типы. Знает переменные типа и подстановки; реконструкция типов; Let- полиморфизм. Знает универсальные типы и экзистенциальные типы.
- Знает основные алгоритмы применяемые в области типов в языках программирования. Реализует алгоритмы на языке Haskell. Владеет навыками реализации алгоритмов вывода типов для различных систем.
Содержание учебной дисциплины
- Простые типы
- Подтипы и рекурсивные типы
- Полиморфные типы
- Системы типов высших порядков
Элементы контроля
- Домашнее задание 1
- Домашнее задание 2
- Домашнее задание 3
- Домашнее задание 4
- Устный экзаменЭкзамен проводится на платформе Zoom. Экзамен проводится в устной форме (опрос по материалам курса). По просьбе преподавателя студент должен быть готов выполнить некоторые задания в письменном виде, после чего сфотографировать и выслать на почту преподавателю. К экзамену необходимо подключиться согласно расписанию, высланному преподавателем на корпоративные почты студентов накануне экзамена. Компьютер студента должен удовлетворять требованиям: наличие рабочей камеры и микрофона, поддержка платформы Zoom. Для участия в экзамене студент обязан: выбрать себе имя в Zoom совпадающее с его именем и фамилией, явиться на экзамен согласно точному расписанию, при ответе включить камеру и микрофон. Во время экзамена студентам запрещается выключать камеру. Ипользование конспектов или других справочных материалов допускается только с разрешения преподавателя. Кратковременным нарушением связи во время экзамена считается нарушение связи менее 5 минут. Долговременным нарушением связи во время экзамена считается нарушение 5 минут и более. При долговременном нарушении связи возможность продолжения студентом участие в экзамене определяется преподавателем. Процедура пересдачи подразумевает использование усложненных заданий
Промежуточная аттестация
- Промежуточная аттестация (3 модуль)0.125 * Домашнее задание 1 + 0.125 * Домашнее задание 2 + 0.125 * Домашнее задание 3 + 0.125 * Домашнее задание 4 + 0.5 * Устный экзамен
Список литературы
Рекомендуемая основная литература
- Sørensen, M. H., & Urzyczyn, P. (2006). Lectures on the Curry-Howard Isomorphism (Vol. 1st ed). Amsterdam: Elsevier Science. Retrieved from http://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=edsebk&AN=196231
Рекомендуемая дополнительная литература
- Pierce, B. C. (2005). Advanced Topics in Types and Programming Languages. Cambridge, Mass: The MIT Press. Retrieved from http://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=edsebk&AN=138471