• A
  • A
  • A
  • АБВ
  • АБВ
  • АБВ
  • А
  • А
  • А
  • А
  • А
Обычная версия сайта

Программирование с зависимыми типами

2019/2020
Учебный год
RUS
Обучение ведется на русском языке
4
Кредиты
Статус:
Курс по выбору
Когда читается:
4-й курс, 3 модуль

Преподаватель

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

Аннотация

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

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

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

Результаты освоения дисциплины

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

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

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

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

  • неблокирующий Created with Sketch. Домашнее задание №1
  • неблокирующий Created with Sketch. Домашнее задание №2
  • неблокирующий Created with Sketch. Домашнее задание №3
  • блокирующий Created with Sketch. Устный экзамен
Промежуточная аттестация

Промежуточная аттестация

  • Промежуточная аттестация (3 модуль)
    0.16 * Домашнее задание №1 + 0.17 * Домашнее задание №2 + 0.17 * Домашнее задание №3 + 0.5 * Устный экзамен
Список литературы

Список литературы

Рекомендуемая основная литература

  • Тузовский А. Ф.-ОБЪЕКТНО-ОРИЕНТИРОВАННОЕ ПРОГРАММИРОВАНИЕ. Учебное пособие для прикладного бакалавриата-М.:Издательство Юрайт,2019-206-Университеты России-978-5-534-00849-4: -Текст электронный // ЭБС Юрайт - https://biblio-online.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