Programming with Dependent Types

2020/2021

Academic Year

RUS

Instruction in Russian

4

ECTS credits

Delivered at:

Department of Informatics

Course type:

Elective course

When:

4 year, 3 module

Instructor

Исаев Валерий Иванович

Программа дисциплины

Аннотация

Целью освоения дисциплины «Программирование с зависимыми типами» является формирование у студентов теоретических знаний и практических навыков по основам создания программ на языках с зависимыми типами. Курс посвящён различным аспектам программирования на языке Agda, таким как типы как сущности первого класса и функции на типах; зависимые типы и зависимое сопоставление с образцом; приёмы доказательства равенств, разрешимости и тотальности; выражение отношений средствами зависимых типов; вычисление эффектов. В результате освоения дисциплины студент должен: − Знать приёмы доказательства равенств, разрешимости и тотальности; − Уметь выражать отношения средствами зависимых типов; − Иметь навыки (приобрести опыт) применения математического и аппарата функций на типах

Цель освоения дисциплины

• формирование у студентов теоретических знаний и практических навыков по основам создания программ на языках с зависимыми типами

Планируемые результаты обучения

• Знает базовые конструкции теории типов и языка agda. Умеет применять индуктивные и коиндуктивные конструкции для решения поставленных задач. Использует теорию типов языки с зависимыми типами для решения поставленных задач
• Знает области применения зависимых типов; особенности программирования с зависимыми типами. Записывает спецификации программ на языке agda; доказывает свойства программ и иные утверждения на языке agda. Доказывает свойства программ и иные утверждения на языке agda.

Содержание учебной дисциплины

• Базовые конструкции теории типов и языка agda
• Индуктивные и коиндуктивные конструкции
• Равенство в теории типов

Элементы контроля

• Домашнее задание 1
• Домашнее задание 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