Книга "Основы языков программирования" написана для студентов старших курсов и аспирантов. В ней используется серия типизированных лямбда-исчислений для изучения аксиоматической, операциональной и денотационной семантики последовательностных языков программирования. По ходу книги происходит постепенное достраивание лямбда-исчисления всё более сложными системами типов.
Отличительной чертой данной книги по сравнению с другими работами по данной теме является то, что в ней содержится материал по универсальной алгебре и алгебраическим типам данных, императивным языкам и Флойд-хоаровской логике, а в последних главах рассматриваются полиморфные типы, модули, подтипы и объектно-ориентированные понятия, а также вывод типов. Книга предназначена прежде всего для изучающих математику, но благодаря включению соответствующих вопросов и примеров материал книги доступен и студентам, специализирующимся по системам программного обеспечения, теории вычислительных систем или математической логике.
Книга может использоваться в качестве справочника специалистами, занимающимися языками программирования, проверкой и аттестацией компьютерных программ и программированием, в том числе теми, кто работает с программными модулями или занимается объектно-ориентированным программированием.

Предисловие редактора перевода
Предисловие

ГЛАВА 1. Введение
1.1. Модель языков программирования
1.2. λ-обозначения
1.3. Уравнения, редукция и семантики
1.4. Типы и системы типов
1.5. Обозначения и математические соглашения
1.6. Введение в теорию множеств
1.7. Синтаксис и семантика
1.8. Индукция

ГЛАВА 2. Язык ПВФ
2.1. Введение
2.2. Синтаксис ПВФ
2.3. ПВФ-программы и их семантики
2.4. ПВФ-редукция и символьная интерпретация
2.5. Примеры ПВФ. Выразительная мощь и ограничения
2.6. Вариации и расширения ПВФ

ГЛАВА 3. Универсальные алгебры и алгебраические типы данных
3.1. Введение
3.2. Предварительный обзор алгебраических спецификаций
3.3. Алгебры, сигнатуры и термы
3.4. Уравнения, корректность и полнота
3.5. Гомоморфизмы и инициальная алгебра
3.6. Алгебраические типы данных
3.7. Системы переписывания термов

ГЛАВА 4. Строго типизированное λ-исчисление
4.1. Введение
4.2. Типы
4.3. Термы
4.4. Формальные системы
4.5. Модели Хенкина, корректность и полнота

ГЛАВА 5. Модели типизированного λ-исчисления
5.1. Введение
5.2. Модели Скотта и неподвижные точки
5.3. Индукция по неподвижным точкам
5.4. Вычислительная корректность и полная абстракция
5.5. Теоретико-рекурсивные модели
5.6. Отношения частичной эквивалентности и рекурсия

ГЛАВА 6. Императивные программы
6.1. Введение
6.2. while-программы
6.3. Операционная семантика
6.4. Денотационная семантика
6.5. Пред- и постусловия для while-программ
6.6. Семантика дополнительных программных конструктов

ГЛАВА 7. Категории и рекурсивные типы
7.1. Введение
7.2. Декартово замкнутые категории
7.3. Ламбда-модели Крипке и категории функторов
7.4. Модели областей рекурсивных типов

ГЛАВА 8. Логические отношения
8.1. Введение в логические отношения
8.2. Логические отношения на аппликативных структурах
8.3. Результаты теории доказательств
8.4. Частичные сюръективности и особые модели
8.5. Независимость от представления
8.6. Обобщения логических отношений

ГЛАВА 9. Полиморфизм и модульность
9.1. Введение
9.2. Предикативное полиморфное исчисление
9.3. Импредикативный полиморфизм
9.4. Абстрактные типы данных и объемные типы
9.5. Обобщенные произведения, суммы и программные модули

ГЛАВА 10. Подтипы и связанные с ними понятия
10.1. Введение
10.2. Строго типизированное λ-исчисление с подтипами
10.3. Записи
10.4. Семантические модели для подтипов
10.5. Рекурсивные типы и модель объектов через записи
10.6. Полиморфизм с ограничениями на подтипы

ГЛАВА 11. Вывод типов
11.1. Введение
11.2. Вывод типов для λ→ с типовыми переменными
11.3. Вывод типов с полиморфными объявлениями

Литература
Предметный указатель