Текущая (весна 2014) версия этого курса здесь

Теория типов:
аппликативные технологии

ФИВТ - факультет инноваций и высоких технологий, МФТИ

Предварительной подготовки не требуется.
Изложение носит замкнутый характер: Теория типов (осень 2006), Теория типов (весна 2009), Теория типов (весна 2010), Теория типов (весна 2011)  

Профессор: Вячеслав Эрнстович Вольфенгаген

Описание курса 
Программа курса
Что читать/Ссылки
Материал курса
Проекты по курсу
Студенты
Семинары
Помощь в изучении
Перечень вопросов

 
Аннотация

Излагаются основные идеи теории типов. Отражены два основных способа типизации выражений. Следуя первому, применявшемуся А. Черчем, ограничивается само определение выражения, когда всякое выражение наделяется его типом как частью его структуры. Во втором, применявшемся Х. Карри, строится язык, в который входят все бестиповые термы, а также применяется теория типов, в рамках которой имеются правила приписывания типов. В соответствии с правилами тип приписывается только некоторым из выражений, но не всем. Рассматривается более слабая теория типов, чем сильные полиморфные теории, применяющиеся в логике и программировании. Эта система лежит в основе всех прочих систем типов, а ее свойства играют самостоятельную роль. Пользуясь ею, рассматривается два метода назначения типов объектам: от типов к объектам и от объектов к типам. Вместе с тем рассматривается теория функций, функции в категории, некоторая теория типов и конструкция функтор-как-объект, что восходит к переменным множествам Ф. Ловера. Это позволяет установить связь с аппликативными вычислениями и показать связи бестиповых моделей вычислений с типовыми моделями вычислений, а также строить естественную формализацию систем высших порядков. В качестве приложения рассматривается строение простой теории типов и структуры концептов и ассоциированные модели объектов данных/метаданных. Дополнительно рассматриваются семейства моделей с соотнесениями для Web.

Модели вычислений оказываются базовым предметом, который необходим для приобретения навыков научной работы и развития интуиции для поиска новых принципов компьютинга. Следовательно, это продвинутый курс, освоив который можно работать над инновационными проектами в области програмирования, информационных технологий, включая Интернет/WWW, управление базами данных, информационные системы, информационный поиск и искусственный интеллект.

Для получения более широкого представления о курсе используйте ссылки слева, отмеченные как Описание и Что читать. Ссылки Материал курса и Студенты содержат презентации и сведения о выполняемых проектах.