Programming with Dependent Types

2023/2024

Academic Year

RUS

Instruction in Russian

5

ECTS credits

Delivered at:

Department of Informatics

Course type:

Elective course

When:

4 year, 1, 2 module

Instructor

Moskvin, Denis

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

Аннотация

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

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

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

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

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

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

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

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

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

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

• 2023/2024 учебный год 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 (дата обращения: 27.08.2024).

Авторы

• Кузнецов Антон Михайлович
• Спицина Кристина Станиславовна