Введение

Часть 1. ТИПИЗИРОВАННОЕ λ-ИСЧИСЛЕНИЕ

• Упражнение 1. Типизированное λ-исчисление (по А. Чёрчу) (238мин.)
• • Теоретические сведения (159мин.)
  • Примеры решения некоторых типов упражнений (26мин.)
  • Упражнения для самостоятельного решения (53мин.)
  • Типизированное λ-исчисление (по А. Чёрчу) (20мин.)

Часть 2. АЛГОРИТМЫ УНИФИКАЦИИ

• Упражнение 2. Алгоритмы унификации в логическом программировании (172мин.)
• • Теоретические сведения (106мин.)
  • Примеры решения некоторых типов упражнений (26мин.)
  • Упражнения для самостоятельного решения (40мин.)
  • Алгоритмы унификации в логическом программировании (14мин.)
• Упражнение 3. Алгоритмы унификации в теории типов (251мин.)
• • Теоретические сведения (53мин.)
  • Примеры решения некоторых типов упражнений (53мин.)
  • Демонстрационный пример (40мин.)
  • Упражнения для самостоятельного решения (106мин.)
  • Алгоритмы унификации в теории типов (12мин.)

Часть 3. МОНОМОРФНЫЕ ТИПЫ (СИСТЕМА λ->)

• Упражнение 4. Мономорфные типы: система λ-> в стиле А. Чёрча (410мин.)
• • Теоретические сведения (291мин.)
  • Примеры решения некоторых типов упражнений (66мин.)
  • Упражнения для самостоятельного решения (40мин.)
  • Мономорфные типы: система λ-> в стиле А. Чёрча (20мин.)
• Упражнение 5. Мономорфные типы: система λ-> в стиле X. Карри (397мин.)
• • Теоретические сведения (79мин.)
  • Примеры решения некоторых типов упражнений (212мин.)
  • Упражнения для самостоятельного решения (93мин.)
  • Мономорфные типы: система λ-> в стиле X. Карри (16мин.)
• Упражнение 6. Мономорфные типы: изоморфизм Карри - Говарда, свойства системы λ-> (344мин.)
• • Теоретические сведения (212мин.)
  • Примеры решения некоторых типов упражнений (40мин.)
  • Упражнения для самостоятельного решения (79мин.)
  • Мономорфные типы: изоморфизм Карри - Говарда, свойства системы λ-> (12мин.)
• Упражнение 7. Элементы теории типов λ-> (для первокурсников) (185мин.)
• • Теоретические сведения (66мин.)
  • Примеры решения некоторых типов упражнений (26мин.)
  • Упражнения для самостоятельного решения (79мин.)
  • Элементы теории типов λ-> (для первокурсников) (12мин.)
• Упражнение 8. Мономорфные типы: алгоритм Хиндли - Милнера в системе λ-> в стиле X. Карри (172мин.)
• • Теоретические сведения (66мин.)
  • Примеры решения некоторых типов упражнений (40мин.)
  • Демонстрационный пример (26мин.)
  • Упражнения для самостоятельного решения (40мин.)
  • Мономорфные типы: алгоритм Хиндли - Милнера в системе λ-> в стиле X. Карри (12мин.)
• Упражнение 9. Проверка и синтез типа для функций в бесточечной форме записи (490мин.)
• • Теоретические сведения (357мин.)
  • Примеры решения некоторых типов упражнений (40мин.)
  • Демонстрационные примеры (40мин.)
  • Задачи для самостоятельного решения (40мин.)
  • Проверка и синтез типа для функций в бесточечной форме записи (12мин.)
• Упражнение 10. Расширения системы λ->: рекурсивные типы (система λµ), типы-пересечения (система λ) (251мин.)
• • Теоретические сведения (146мин.)
  • Упражнения для самостоятельного решения (93мин.)
  • Расширения системы λ->: рекурсивные типы (система λµ), типы-пересечения (система λ) (14мин.)
• Лабораторная работа 11. Программная модель вывода типов (в системе λ->) (79мин.)
• • Теоретические сведения (53мин.)
  • Задачи для самостоятельного решения (26мин.)
  • Программная модель вывода типов (в системе λ–>) (12мин.)

Часть 4. ПОЛИМОРФНЫЕ ТИПЫ (СИСТЕМА λ2)

• Упражнение 12. Полиморфные типы: система λ2 в стиле X. Карри (556мин.)
• • Теоретические сведения (384мин.)
  • Примеры решения некоторых типов упражнений (26мин.)
  • Работа с демонстрационными примерами (93мин.)
  • Упражнения для самостоятельного решения (40мин.)
  • Полиморфные типы: система λ2 в стиле X. Карри (14мин.)
• Упражнение 13. Полиморфные типы: решение задачи TSP для рекурсивных типов (304мин.)
• • Теоретические сведения (238мин.)
  • Примеры решения некоторых типов упражнений (13мин.)
  • Упражнения для самостоятельного решения (40мин.)
  • Полиморфные типы: решение задачи TSP для рекурсивных типов (12мин.)
• Упражнение 14. Полиморфные типы: система λ2 в стиле А. Чёрча (304мин.)
• • Теоретические сведения (146мин.)
  • Примеры решения некоторых типов упражнений (66мин.)
  • Упражнения для самостоятельного решения (79мин.)
  • Полиморфные типы: система λ2 в стиле А. Чёрча (12мин.)
• Упражнение 15. Система λ2 в стиле А. Чёрча: логические связки и квантор , логические операции, упорядоченные пары, нумералы, списки (357мин.)
• • Теоретические сведения (265мин.)
  • Примеры решения некоторых типов упражнений (26мин.)
  • Упражнения для самостоятельного решения (53мин.)
  • Система λ2 в стиле А. Чёрча: логические связки и квантор , логические операции, упорядоченные пары, нумералы, списки (14мин.)
• Упражнение 16. Система λ2 в стиле А. Чёрча: метод синтаксически ориентированного конструирования (146мин.)
• • Теоретические сведения (119мин.)
  • Упражнения для самостоятельного решения (26мин.)
  • Система λ2 в стиле А. Чёрча: метод синтаксически ориентированного конструирования (12мин.)

Часть 5. λ-КУБ БАРЕНДРЕГТА

• Упражнение 17. Операторы на типах. Кайнды конструкторов типов (291мин.)
• • Теоретические сведения (185мин.)
  • Примеры решения некоторых типов упражнений (66мин.)
  • Упражнения для самостоятельного решения (26мин.)
  • Операторы на типах. Кайнды конструкторов типов (14мин.)
• Упражнение 18. Система типов λω с операторами на типах (185мин.)
• • Теоретические сведения (106мин.)
  • Примеры решения некоторых типов упражнений (26мин.)
  • Упражнения для самостоятельного решения (53мин.)
  • Система типов λω с операторами на типах (12мин.)
• Упражнение 19. Система типов λP с зависимыми типами (278мин.)
• • Теоретические сведения (185мин.)
  • Примеры решения некоторых типов упражнений (40мин.)
  • Упражнения для самостоятельного решения (53мин.)
  • Система типов λP с зависимыми типами (12мин.)
• Упражнение 20. λ-куб Барендрегта (331мин.)
• • Теоретические сведения (212мин.)
  • Примеры решения некоторых типов упражнений (13мин.)
  • Упражнения для самостоятельного решения (93мин.)
  • λ-куб Барендрегта (14мин.)
• Упражнение 21. Логические системы λ-куба. Прямое погружение логических систем в λ-куб (212мин.)
• • Теоретические сведения (119мин.)
  • Примеры решения некоторых типов упражнений (26мин.)
  • Упражнения для самостоятельного решения (53мин.)
  • Логические системы λ-куба. Прямое погружение логических систем в λ-куб (14мин.)

Часть 6. ИНТУИЦИОНИСТСКИЕ ЛОГИЧЕСКИЕ ИСЧИСЛЕНИЯ

• Упражнение 1L. Интуиционистские пропозициональные логики (357мин.)
• • Теоретические сведения (251мин.)
  • Примеры решения некоторых типов упражнений (13мин.)
  • Задачи для самостоятельного решения (79мин.)
  • Интуиционистские пропозициональные логики (16мин.)
• Упражнение 2L. Интуиционистские пропозициональные логики: минимальное позитивное исчисление Prop (238мин.)
• • Теоретические сведения (106мин.)
  • Примеры решения некоторых типов упражнений (40мин.)
  • Задачи для самостоятельного решения (79мин.)
  • Интуиционистские пропозициональные логики: минимальное позитивное исчисление Prop (12мин.)
• Упражнение 3L. Интуиционистские пропозициональные логики: секвенциальное исчисление Н. Н. Воробьёва - Дж. Худельмайера без правила сокращения (357мин.)
• • Теоретические сведения (119мин.)
  • Примеры решения некоторых типов упражнений (119мин.)
  • Упражнения для самостоятельного решения (106мин.)
  • Интуиционистские пропозициональные логики: секвенциальное исчисление Н. Н. Воробьёва - Дж. Худельмайера без правила сокращения (12мин.)
• Упражнение 4L. Интуиционистские пропозициональные логики: логика второго порядка Рrор2 (185мин.)
• • Теоретические сведения (106мин.)
  • Примеры решения некоторых типов упражнений (26мин.)
  • Задачи для самостоятельного решения (53мин.)
  • Интуиционистские пропозициональные логики: логика второго порядка Рrор2 (16мин.)
• Упражнение 5L. Интуиционистская предикатная логика: минимальная логика Pred (251мин.)
• • Теоретические сведения (159мин.)
  • Примеры решения некоторых типов упражнений (13мин.)
  • Упражнения для самостоятельного решения (79мин.)
  • Интуиционистская предикатная логика: минимальная логика Pred (12мин.)

Литература

Новые издания по дисциплине "Программирование" и смежным дисциплинам

Приложение 1. Программа синтеза типа λ-терма в системе λ-> по двухэтапному алгоритму Хиндли - Милн

Приложение 2. Транслятор математической формы записи λ-терма в системе λ-> в запись с конструктора

Приложение 3. Программа синтеза типа λ-терма и кайнда типа в системах λ-куба Барендрегта

Завершение курса

• Тест:  Итоговое тестирование (40мин.)