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

Бакалавриат 2024/2025

Статус: Курс по выбору (Прикладная математика и информатика)

Направление: 01.03.02. Прикладная математика и информатика

Кто читает: Департамент информатики

Где читается: Санкт-Петербургская школа физико-математических и компьютерных наук

Когда читается: 4-й курс, 1, 2 модуль

Формат изучения: без онлайн-курса

Охват аудитории: для своего кампуса

Преподаватели: Москвин Денис Николаевич

Язык: русский

Кредиты: 5

Полная версия программы учебной дисциплины Задать вопрос

Аннотация

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

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

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

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

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

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

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

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

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

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

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

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

Авторы

Кузнецов Антон Михайлович
Юдаева Оксана Юрьевна

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