Введение в теорию языков программирования

От переводчиков
Что называют теорией языков программирования?
Благодарности
Глава 1. Термы и отношения
1.1.Индуктивные определения
1.1.1. Теорема о неподвижной точке
1.1.2. Индуктивные определения
1.1.3. Структурная индукция
1.1.4. Рефлексивно-транзитивное замыкание
отношения
1.2.Языки
1.2.1. Языки без переменных
1.2.2. Переменные
1.2.3. Многосортные языки
1.2.4. Свободные и связанные переменные
1.2.5. Подстановка
1.3.Три способа задания семантики языка
1.3.1. Денотационная семантика
1.3.2. Операционная семантика с большим шагом
1.3.3. Операционная семантика с малым шагом
1.3.4. Незавершающиеся вычисления
Глава 2. Язык PCF
2.1. Функциональный язык PCF
2.1.1. Программы как функции
2.1.2. Функции как объекты первого класса
2.1.3. Функции с несколькими аргументами
2.1.4. Без присваиваний
2.1.5. Рекурсивные определения
2.1.6. Определения
2.1.7. Язык PCF
2.2.Операционная семантика с малым шагом
2.2.1. Правила
2.2.2. Числа
2.2.3. Эквивалентность (congruence)
2.2.4. Пример
2.2.5. Нередуцируемые замкнутые термы
2.2.6. Незавершающиеся вычисления
2.2.7. Слияние (confuence)
2.3.Стратегии редукции
2.3.1. Понятие стратегии
2.3.2. Слабая редукция
2.3.3. Вызов по имени
2.3.4. Вызов по значению
2.3.5. Немного лени не помешает
2.4.Операционная семантика с большим шагом
2.4.1. Вызов по имени
2.4.2. Вызов по значению
2.5.Вычисление PCF-программ
Глава 3. От вычисления к интерпретации
3.1. Вызов по имени
3.2. Вызов по значению
3.3. Оптимизация: индексы де Брауна
3.4. Построение функций с помощью неподвижных
точек
3.4.1. Первая версия: рекурсивные замыкания
3.4.2. Вторая версия: рациональные значения
Глава 4. Компиляция
4.1. Интерпретатор, написанный на языке без
функций
4.2. От интерпретации к компиляции
4.3. Абстрактная машина для PCF
4.3.1. Окружение
4.3.2. Замыкания
4.3.3. Конструкции PCF
4.3.4. Использование индексов де Брауна
4.3.5. Операционная семантика с малым шагом
4.4.Компиляция PCF
Глава 5. PCF с типами
5.1.Типы
5.1.1. PCF с типами
5.1.2. Отношение типизации
5.2.Отсутствие ошибок во время выполнения
5.2.1. Использование операционной семантики с
малым шагом
5.2.2. Использование операционной семантики с
большим шагом
5.3.Денотационная семантика для PCF с типами
5.3.1. Тривиальная семантика
5.3.2. Завершаемость
5.3.3. Отношение порядка Скотта
5.3.4. Семантика неподвижной точки
Глава 6. Вывод типов
6.1.Вывод мономорфных типов
6.1.1. Присвоение типов нетипизированным
термам
6.1.2. Алгоритм Хиндли
6.1.3. Алгоритм Хиндли с немедленным
разрешением
6.2.Полиморфизм
6.2.1. PCF с полиморфными типами
6.2.2. Алгоритм Дамаса-Милнера
Глава 7. Ссылки и присваивание
7.1. Расширение PCF
7.2. Семантика PCF со ссылками
Глава 8. Записи и объекты
8.1.Записи
8.1.1. Помеченные поля
8.1.2. Расширение PCF записями
8.2.Объекты
8.2.1. Методы и функциональные поля
8.2.2. Что значит "Self"?
8.2.3. Объекты и ссылки
Послесловие
Библиография
Предметный указатель