Типы и языки программирования на русском

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

Данный текст представляет собой всестороннее введение как в системы типов в информатике, так и в базовую теорию языков программирования. Подход прагматичен и операционален; каждая новая концепция мотивируется примерами из программирования, а более теоретические разделы определяются потребностями реализаций. Каждая глава сопровождается многочисленными упражнениями и решениями, а также работающей реализацией, доступной через Интернет. Зависимости между главами явно обозначены, что позволяет читателям выбирать различные пути изучения материала.

Основные темы включают нетипизированное лямбда-исчисление, простые системы типов, реконструкцию типов, универсальный и экзистенциальный полиморфизм, подтипизацию, ограниченную квантификацию, рекурсивные типы, виды и операторы типов. Расширенные тематические исследования демонстрируют различные подходы к моделированию особенностей объектно-ориентированных языков.