questions.tex

\documentclass[11pt,a4paper,oneside]{book}
\usepackage[utf8]{inputenc}
\usepackage[english,russian]{babel}
\usepackage[top=2cm,bottom=1cm,left=1cm,right=1cm]{geometry}

\begin{document}
\pagestyle{empty}

\begin{center}
\begin{Large}\scshape Программа курса <<Теория типов>>\end{Large}\\\vspace{0.1cm}
\textit{ИТМО, группы M3334-M3339 (year2016), осень 2018 г.}
\end{center}

\begin{enumerate}
\item Бестиповое лямбда-исчисление. Общие определения (альфа-эквивалентность, бета-редукция, 
бета-эк\-ви\-ва\-лент\-ность).
Параллельная бета-редукция. Теорема Чёрча-Россера.
\item Булевские значения, чёрчевские нумералы, упорядоченные пары.
\item Алгебраические типы: аналог в теории множеств, реализация в лямбда-исчислении. 
Нормальный и аппликативный порядок редукций, мемоизация.
\item \textbf{Y}-комбинатор. Парадокс Карри.
\item Просто типизированное лямбда-исчисление. Исчисление по Чёрчу и по Карри. Изоморфизм Карри-Ховарда.
\item Конъюнкция, дизъюнкция, ложь и соответствующие им конструкции в лямбда-исчислении.
\item Нетипизируемость \textbf{Y}-комбинатора. Слабая и сильная нормализация.
\item Задачи проверки типа, реконструкции (вывода) типа, обитаемости типа в просто типизированном лямбда-исчислении.
Их аналоги в интуиционистском исчислении высказываний.
\item Алгебраические термы. Задача унификации в алгебраических термах. Алгоритм унификации. Доказательство 
корректности алгоритма унификации. Наиболее общее решение задачи унификации.
\item Алгоритм нахождения типа в просто типизированном лямбда-исчислении. Наиболее общий тип, наиболее общая пара.
\item Комбинаторы. Базисы $SK$ и $BCKW$, выразимость в них любого замкнутого лямбда-терма.
Аналоги для комбинаторных исчислений в исчислении высказываний.
\item Логика второго порядка. Выразимость связок через импликацию и квантор всеобщности в интуиционистской логике 
2-го порядка (конъюнкция, дизъюнкция, ложь, отрицание, квантор существования).
\item Система F. Изоморфизм Карри-Ховарда для системы F. Упорядоченные пары и алгебраические типы.
\item Экзистенциальные типы. Конструкции \texttt{unpack} и \texttt{pack}.
\item Ранг типа. Частный случай типа. Типы и типовые схемы. \texttt{let}-полиморфизм.
\item Типовая система Хиндли-Милнера. Алгоритм W.
\item Типизация \textbf{Y}-комбинатора. Экви- и изорекурсивные типы, $\mu$-оператор, \texttt{roll} и \texttt{unroll}.
\item Зависимые типы: примеры в языках программирования, теоретико-множественный смысл, исчисление предикатов
и зависимые типы.
\item Обобщённые типовые системы. Типы, рода, сорта. Лямбда-куб.
\item Язык Идрис. Типизация \texttt{printf} с использованием зависимых типов.
\item Типы \texttt{Fin} и \texttt{Vect}. Операция индексации, доказуемо не выходящая за границы массива.
\item $\Sigma$ и $\Pi$ типы в языке Идрис. Примеры использования.
Переформулировка типов на языке обобщённых типовых систем.
Изоморфизм Карри-Ховарда и утверждения, соответствующие данным типам.
\item Равенство в Идрис. Доказательства в языке Идрис (на примере коммутативности сложения). 
Функция \texttt{replace} и конструкция \texttt{rewrite}.
\item Теорема Диаконеску. Типы и сетоиды.
\end{enumerate}

\end{document}