|
Содержание
Предисловие редактора перевода Предисловие ГЛАВА 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. Вывод типов с полиморфными объявлениями Литература Предметный указатель |