• A
  • A
  • A
  • АБВ
  • АБВ
  • АБВ
  • А
  • А
  • А
  • А
  • А
Обычная версия сайта
02
Июль

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

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

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

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

Аннотация

Является дисциплиной по выбору. Курс посвящён различным аспектам программирования на языке Agda, таким как: типы как сущности первого класса и функции на типах; зависимые типы и зависимое сопоставление с образцом; приёмы доказательства равенств, разрешимости и тотальности; выражение отношений средствами зависимых типов; вычисление эффектов. Для освоения дисциплины студентам необходимы знания, полученные в результате изучения дисциплин «Функциональное программирование», «Типы в языках программирования».
Цель освоения дисциплины

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

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

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

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

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

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

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

  • неблокирующий Домашнее задание №1
    Домашнее задание №1 выдается студентам в одном варианте и состоит из 12 задач. Каждой задаче присвоен свой балл. Срок выполнения домашнего задания - 1 неделя. Форма представления обучающимися домашнего задания - представленные в письменном виде решения задач.
  • неблокирующий Домашнее задание №2
    Домашнее задание №2 выдается студентам в одном варианте и состоит из 13 задач. Каждой задаче присвоен свой балл. Срок выполнения домашнего задания - 1 неделя. Форма представления обучающимися домашнего задания - представленные в письменном виде решения задач.
  • неблокирующий Домашнее задание №3
    Домашнее задание №3 выдается студентам в одном варианте и состоит из 20 задач. Каждой задаче присвоен свой балл. Срок выполнения домашнего задания - 1 неделя. Форма представления обучающимися домашнего задания - представленные в письменном виде решения задач.
  • блокирующий Устный экзамен
    Устный экзамен проводится в форме ответов на вопросы экзаменационного билета. Экзаменационный билет содержит два вопроса из перечня вопросов к экзамену. На подготовку ответа выделяется 2,5 часа.
Промежуточная аттестация

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

  • 2022/2023 учебный год 2 модуль
    Преподаватель учитывает оценку за текущий контроль (домашние задания). Онакопленная = (Од/з1 + Од/з2 + Од/з3) / 3 Результирующая оценка за дисциплину рассчитывается следующим образом: ОРезультирующая = 0,5Онакопленная + 0,5Оэкзамен
Список литературы

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

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

  • Pierce, B. C. (2002). 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=70966

Рекомендуемая дополнительная литература

  • Тузовский, А. Ф.  Объектно-ориентированное программирование : учебное пособие для вузов / А. Ф. Тузовский. — Москва : Издательство Юрайт, 2021. — 206 с. — (Высшее образование). — ISBN 978-5-534-00849-4. — Текст : электронный // Образовательная платформа Юрайт [сайт]. — URL: https://urait.ru/bcode/470223 (дата обращения: 28.08.2023).