=2

• Предисловие
• Введение
  • Типы в информатике
  • Для чего годятся типы
  • Системы типов и проектирование языков
  • Краткая история
  • Дополнительная литература
• Математический аппарат
  • Множества, отношения и функции
  • Упорядоченные множества
  • Последовательности
  • Индукция
  • Справочная литература

• Бестиповые арифметические выражения
  • Введение
  • Синтаксис
  • Индукция на термах
  • Семантические стили
  • Вычисление
  • Дополнительные замечания
• Реализация арифметических выражений на языке ML
  • Синтаксис
  • Вычисление
  • Что осталось за кадром
• Бестиповое лямбда-исчисление
  • Основы
  • Программирование на языке лямбда-исчисления
  • Формальности
  • Операционная семантика
  • Дополнительные замечания
• Представление термов без использованиия имен
  • Термы и контексты
  • Сдвиг и подстановка
  • Вычисление
• Реализация лямбда-исчисления на ML
  • Термы и контексты
  • Сдвиг и подстановка
  • Вычисление
  • Дополнительные замечания

• Типизированные арифметические выражения
  • Типы
  • Отношение типизации
  • Безопасность = продвижение + сохранение
• Простое типизированное лямбда-исчисление
  • Типы функций
  • Отношение типизации
  • Свойства типизации
  • Соответствие Карри-Ховарда
  • Стирание типов и типизируемость
  • Стиль Карри и стиль Чёрча
  • Дополнительные замечания
• Реализация простых типов на ML
  • Контексты
  • Термы и типы
  • Проверка типов
• Простые расширения
  • Базовые типы
  • Единичный тип
  • Производные формы: последовательное исполнение и связывания-пустышки
  • Приписывание типа
  • Связывания let
  • Пары
  • Кортежи
  • Записи
  • Типы-суммы
  • Варианты
  • Рекурсия общего вида
  • Списки
• Нормализация
  • Нормализация для простых типов
  • Дополнительные замечания
• Ссылки
  • Введение
  • Типизация
  • Вычисление
  • Типизация памяти
  • Безопасность
  • Дополнительные замечания
• Исключения
  • Порождение исключений
  • Обработка исключений
  • Исключения, сопровождаемые значениями

• Наследование
  • Включение
  • Отношение наследования
  • Свойства наследования и типизации
  • Типы Top и Bottom
  • Наследование и другие элементы языка
  • Семантика наследования, основанная на преобразованиях типов
  • Типы-пересечения и типы-объединения
  • Дополнительные замечания
• Метатеория наследования
  • Алгоритмическое отношение наследования
  • Алгоритмическое отношение типизации
  • Пересечения и объединения
  • Алгоритмическая типизация и тип Bot
• Реализация наследования на ML
  • Синтаксис
  • Наследование
  • Типизация
• Расширенный пример: императивные объекты
  • Что такое объектно-ориентированное программирование?
  • Объекты
  • Генераторы объектов
  • Наследование
  • Группировка переменных экземпляра
  • Простые классы
  • Добавление новых переменных экземпляра
  • Вызов методов надкласса
  • Классы с переменной self
  • Открытая рекурсия через self
  • Открытая рекурсия и порядок вычислений
  • Более эффективная реализация
  • Резюме
  • Дополнительные замечания
• Расширенный пример: Облегченная Java
  • Введение
  • Обзор
  • Именные и структурные системы типов
  • Определения
  • Свойства
  • Сравнение кодирования и объектов в виде элементарного понятия
  • Дополнительные замечания

• Рекурсивные типы
  • Примеры
  • Формальные определения
  • Наследование
  • Дополнительные замечания
• Метатеория рекурсивных типов
  • Индукция и коиндукция
  • Конечные и бесконечные типы
  • Наследование
  • Отступление о транзитивности
  • Проверка членства
  • Более эффективные алгоритмы
  • Регулярные деревья
  • µ-типы
  • Подсчет подвыражений
  • Отступление: экспоненциальный алгоритм
  • Наследование для изорекурсивных типов
  • Дополнительные замечания

• Реконструкция типов
  • Типовые переменные и подстановки
  • Две точки зрения на типовые переменные
  • Типизация на основе ограничений
  • Унификация
  • Главные типы
  • Неявные аннотации типов
  • Полиморфизм через let
  • Дополнительные замечания
• Универсальные типы
  • Мотивация
  • Разновидности полиморфизма
  • Система F
  • Примеры
  • Основные свойства
  • Стирание, типизируемость и реконструкция типов
  • Стирание и порядок вычислений
  • Фрагменты Системы F
  • Параметричность
  • Импредикативность
  • Дополнительные замечания
• Экзистенциальные типы
  • Мотивация
  • Абстракция данных при помощи экзистенциальных типов
  • Кодирование экзистенциальных типов
  • Дополнительные замечания
• Реализация Системы F на ML
  • Представление типов без использования имен
  • Сдвиг типов и подстановка
  • Термы
  • Вычисление
  • Типизация
• Ограниченная квантификация
  • Мотивация
  • Определения
  • Примеры
  • Безопасность
  • Ограниченные экзистенциальные типы
  • Дополнительные замечания
• Расширенный пример: еще раз императивные объекты
• Метатеория ограниченной квантификации
  • Выявление
  • Минимальная типизация
  • Наследование в Ядерной F_<:
  • Наследование в Полной F_<:
  • Неразрешимость Полной F_<:
  • Объединения и пересечения
  • Ограниченные кванторы существования
  • Ограниченная квантификация и тип Bot

• Операторы над типами и виды
  • Неформальное введение
  • Определения
• Полиморфизм высших порядков
  • Определения
  • Пример
  • Свойства исчисления
  • Фрагменты F_ω
  • Идем дальше: зависимые типы
• Наследование высших порядков
  • Интуитивные понятия
  • Определения
  • Свойства исчисления
  • Дополнительные замечания
• Расширенный пример: чисто функциональные объекты
  • Простые объекты
  • Наследование
  • Ограниченная квантификация
  • Типы интерфейсов
  • Отправка сообщений объектам
  • Простые классы
  • Полиморфные обновления
  • Добавление переменных экземпляра
  • Классы с переменной self
  • Дополнительные замечания

• Решения избранных упражнений
• Принятые обозначения
  • Имена метапеременных
  • Имена правил
  • Соглашения по именам и индексам
• Список литературы
• Index

This document was translated from L^AT_EX by H^EV^EA.