Теория типов в логике и основаниях математики.

Description

Титульный лист Введение Глава 1. Типы в исчислении предикатов и в лямбда-исчислении 1.1. Теория типов Б. Рассела и А. Уайтхеда 1.2. Лямбда-исчисление: чистое и типовое. Комбинаторная логика. Соответствие Карри-Говарда Глава 2. Теория категорий и типы 2.1. Базовые определения теории категорий 2.2. Декартово замкнутые категории 2.3. Пример декартово замкнутой категории 2.4. Категории над объектами и локально декартово замкнутые категории 2.5. n-категории 2.6. Декартово замкнутые категории и типовое лямбда-исчисление Глава 3. Теория типов П. Мартина-Лефа 3.1. Основные определения 3.2. Теоретико-категорная модель теории зависимых типов (экстенсиональный вариант) Глава 4. Гомотопическая интерпретация теории конструктивных типов 4.1. Базовые определения теории гомотопий 4.2. Фундаментальные и высшие группоиды 4.3. Типы как высшие группоиды 4.4. Семейства типов как расслоения, суммы и произведения 4.5. Высшие индуктивные типы 4.6. Гомотопические n-типы Заключение Список литературы