• A
  • A
  • A
  • ABC
  • ABC
  • ABC
  • А
  • А
  • А
  • А
  • А
Regular version of the site

Programming with Dependent Types

2019/2020
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
    «Отлично» (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