Бакалавриат
2019/2020
Программирование с зависимыми типами
Лучший по критерию «Полезность курса для расширения кругозора и разностороннего развития»
Лучший по критерию «Новизна полученных знаний»
Статус:
Курс по выбору (Прикладная математика и информатика)
Направление:
01.03.02. Прикладная математика и информатика
Кто читает:
Департамент информатики
Когда читается:
4-й курс, 3 модуль
Формат изучения:
без онлайн-курса
Преподаватели:
Москвин Денис Николаевич
Язык:
русский
Кредиты:
4
Контактные часы:
66
Программа дисциплины
Аннотация
Целью освоения дисциплины «Программирование с зависимыми типами» является формирование у студентов теоретических знаний и практических навыков по основам создания программ на языках с зависимыми типами. Курс посвящён различным аспектам программирования на языке Agda, таким как типы как сущности первого класса и функции на типах; зависимые типы и зависимое сопоставление с образцом; приёмы доказательства равенств, разрешимости и тотальности; выражение отношений средствами зависимых типов; вычисление эффектов. В результате освоения дисциплины студент должен: − Знать приёмы доказательства равенств, разрешимости и тотальности; − Уметь выражать отношения средствами зависимых типов; − Иметь навыки (приобрести опыт) применения математического и аппарата функций на типах
Цель освоения дисциплины
- формирование у студентов теоретических знаний и практических навыков по основам создания программ на языках с зависимыми типами
Планируемые результаты обучения
- Знает базовые конструкции теории типов и языка agda. Умеет применять индуктивные и коиндуктивные конструкции для решения поставленных задач. Использует теорию типов языки с зависимыми типами для решения поставленных задач
- Знает области применения зависимых типов; особенности программирования с зависимыми типами. Записывает спецификации программ на языке agda; доказывает свойства программ и иные утверждения на языке agda. Доказывает свойства программ и иные утверждения на языке agda.
Содержание учебной дисциплины
- Базовые конструкции теории типов и языка agda
- Индуктивные и коиндуктивные конструкции
- Равенство в теории типов
Элементы контроля
- Домашнее задание №1«Отлично» (8-10) Решено задач на 20 или более баллов «Хорошо» (6-7) Решено задач на 14-19 баллов «Удовлетворительно» (4-5) Решено задач на 9-13 баллов «Неудовлетворительно» (0-3) Решено задач на менее чем 9 баллов
- Домашнее задание №2
- Домашнее задание №3
- Устный экзаменЭкзамен проводится на платформе Zoom. Экзамен проводится в устной форме (опрос по материалам курса). По просьбе преподавателя студент должен быть готов выполнить некоторые задания в письменном виде, после чего сфотографировать и выслать на почту преподавателю. К экзамену необходимо подключиться согласно расписанию, высланному преподавателем на корпоративные почты студентов накануне экзамена. Компьютер студента должен удовлетворять требованиям: наличие рабочей камеры и микрофона, поддержка платформы Zoom. Для участия в экзамене студент обязан: выбрать себе имя в Zoom совпадающее с его именем и фамилией, явиться на экзамен согласно точному расписанию, при ответе включить камеру и микрофон. Во время экзамена студентам запрещается выключать камеру. Ипользование конспектов или других справочных материалов допускается только с разрешения преподавателя. Кратковременным нарушением связи во время экзамена считается нарушение связи менее 5 минут. Долговременным нарушением связи во время экзамена считается нарушение 5 минут и более. При долговременном нарушении связи возможность продолжения студентом участие в экзамене определяется преподавателем. Процедура пересдачи подразумевает использование усложненных заданий
Промежуточная аттестация
- Промежуточная аттестация (3 модуль)0.16 * Домашнее задание №1 + 0.17 * Домашнее задание №2 + 0.17 * Домашнее задание №3 + 0.5 * Устный экзамен
Список литературы
Рекомендуемая основная литература
- Тузовский А. Ф. - ОБЪЕКТНО-ОРИЕНТИРОВАННОЕ ПРОГРАММИРОВАНИЕ. Учебное пособие для прикладного бакалавриата - М.:Издательство Юрайт - 2019 - 206с. - ISBN: 978-5-534-00849-4 - Текст электронный // ЭБС ЮРАЙТ - URL: https://urait.ru/book/obektno-orientirovannoe-programmirovanie-434045
Рекомендуемая дополнительная литература
- Introduction to Milestones in Interactive Theorem Proving. (2018). Journal of Automated Reasoning, 61(1–4), 1–8. https://doi.org/10.1007/s10817-018-9465-5