Введение

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

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

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

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

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

• Упражнение 4. Мономорфные типы: система λ-> в стиле А. Чёрча (406мин.)
• • Теоретические сведения (288мин.)
  • Примеры решения некоторых типов упражнений (66мин.)
  • Упражнения для самостоятельного решения (39мин.)
  • Мономорфные типы: система λ-> в стиле А. Чёрча (20мин.)
• Упражнение 5. Мономорфные типы: система λ-> в стиле X. Карри (393мин.)
• • Теоретические сведения (79мин.)
  • Примеры решения некоторых типов упражнений (210мин.)
  • Упражнения для самостоятельного решения (92мин.)
  • Мономорфные типы: система λ-> в стиле X. Карри (16мин.)
• Упражнение 6. Мономорфные типы: изоморфизм Карри - Говарда, свойства системы λ-> (341мин.)
• • Теоретические сведения (210мин.)
  • Примеры решения некоторых типов упражнений (39мин.)
  • Упражнения для самостоятельного решения (79мин.)
  • Мономорфные типы: изоморфизм Карри - Говарда, свойства системы λ-> (12мин.)
• Упражнение 7. Элементы теории типов λ-> (для первокурсников) (184мин.)
• • Теоретические сведения (66мин.)
  • Примеры решения некоторых типов упражнений (26мин.)
  • Упражнения для самостоятельного решения (79мин.)
  • Элементы теории типов λ-> (для первокурсников) (12мин.)
• Упражнение 8. Мономорфные типы: алгоритм Хиндли - Милнера в системе λ-> в стиле X. Карри (170мин.)
• • Теоретические сведения (66мин.)
  • Примеры решения некоторых типов упражнений (39мин.)
  • Демонстрационный пример (26мин.)
  • Упражнения для самостоятельного решения (39мин.)
  • Мономорфные типы: алгоритм Хиндли - Милнера в системе λ-> в стиле X. Карри (12мин.)
• Упражнение 9. Проверка и синтез типа для функций в бесточечной форме записи (485мин.)
• • Теоретические сведения (354мин.)
  • Примеры решения некоторых типов упражнений (39мин.)
  • Демонстрационные примеры (39мин.)
  • Задачи для самостоятельного решения (39мин.)
  • Проверка и синтез типа для функций в бесточечной форме записи (12мин.)
• Упражнение 10. Расширения системы λ->: рекурсивные типы (система λµ), типы-пересечения (система λ) (249мин.)
• • Теоретические сведения (144мин.)
  • Упражнения для самостоятельного решения (92мин.)
  • Расширения системы λ->: рекурсивные типы (система λµ), типы-пересечения (система λ) (14мин.)
• Лабораторная работа 11. Программная модель вывода типов (в системе λ->) (79мин.)
• • Теоретические сведения (52мин.)
  • Задачи для самостоятельного решения (26мин.)
  • Программная модель вывода типов (в системе λ–>) (12мин.)

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

• Упражнение 12. Полиморфные типы: система λ2 в стиле X. Карри (551мин.)
• • Теоретические сведения (380мин.)
  • Примеры решения некоторых типов упражнений (26мин.)
  • Работа с демонстрационными примерами (92мин.)
  • Упражнения для самостоятельного решения (39мин.)
  • Полиморфные типы: система λ2 в стиле X. Карри (14мин.)
• Упражнение 13. Полиморфные типы: решение задачи TSP для рекурсивных типов (302мин.)
• • Теоретические сведения (236мин.)
  • Примеры решения некоторых типов упражнений (13мин.)
  • Упражнения для самостоятельного решения (39мин.)
  • Полиморфные типы: решение задачи TSP для рекурсивных типов (12мин.)
• Упражнение 14. Полиморфные типы: система λ2 в стиле А. Чёрча (302мин.)
• • Теоретические сведения (144мин.)
  • Примеры решения некоторых типов упражнений (66мин.)
  • Упражнения для самостоятельного решения (79мин.)
  • Полиморфные типы: система λ2 в стиле А. Чёрча (12мин.)
• Упражнение 15. Система λ2 в стиле А. Чёрча: логические связки и квантор , логические операции, упорядоченные пары, нумералы, списки (354мин.)
• • Теоретические сведения (262мин.)
  • Примеры решения некоторых типов упражнений (26мин.)
  • Упражнения для самостоятельного решения (52мин.)
  • Система λ2 в стиле А. Чёрча: логические связки и квантор , логические операции, упорядоченные пары, нумералы, списки (14мин.)
• Упражнение 16. Система λ2 в стиле А. Чёрча: метод синтаксически ориентированного конструирования (144мин.)
• • Теоретические сведения (118мин.)
  • Упражнения для самостоятельного решения (26мин.)
  • Система λ2 в стиле А. Чёрча: метод синтаксически ориентированного конструирования (12мин.)

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

• Упражнение 17. Операторы на типах. Кайнды конструкторов типов (288мин.)
• • Теоретические сведения (184мин.)
  • Примеры решения некоторых типов упражнений (66мин.)
  • Упражнения для самостоятельного решения (26мин.)
  • Операторы на типах. Кайнды конструкторов типов (14мин.)
• Упражнение 18. Система типов λω с операторами на типах (184мин.)
• • Теоретические сведения (105мин.)
  • Примеры решения некоторых типов упражнений (26мин.)
  • Упражнения для самостоятельного решения (52мин.)
  • Система типов λω с операторами на типах (12мин.)
• Упражнение 19. Система типов λP с зависимыми типами (275мин.)
• • Теоретические сведения (184мин.)
  • Примеры решения некоторых типов упражнений (39мин.)
  • Упражнения для самостоятельного решения (52мин.)
  • Система типов λP с зависимыми типами (12мин.)
• Упражнение 20. λ-куб Барендрегта (328мин.)
• • Теоретические сведения (210мин.)
  • Примеры решения некоторых типов упражнений (13мин.)
  • Упражнения для самостоятельного решения (92мин.)
  • λ-куб Барендрегта (14мин.)
• Упражнение 21. Логические системы λ-куба. Прямое погружение логических систем в λ-куб (210мин.)
• • Теоретические сведения (118мин.)
  • Примеры решения некоторых типов упражнений (26мин.)
  • Упражнения для самостоятельного решения (52мин.)
  • Логические системы λ-куба. Прямое погружение логических систем в λ-куб (14мин.)

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

• Упражнение 1L. Интуиционистские пропозициональные логики (354мин.)
• • Теоретические сведения (249мин.)
  • Примеры решения некоторых типов упражнений (13мин.)
  • Задачи для самостоятельного решения (79мин.)
  • Интуиционистские пропозициональные логики (16мин.)
• Упражнение 2L. Интуиционистские пропозициональные логики: минимальное позитивное исчисление Prop (236мин.)
• • Теоретические сведения (105мин.)
  • Примеры решения некоторых типов упражнений (39мин.)
  • Задачи для самостоятельного решения (79мин.)
  • Интуиционистские пропозициональные логики: минимальное позитивное исчисление Prop (12мин.)
• Упражнение 3L. Интуиционистские пропозициональные логики: секвенциальное исчисление Н. Н. Воробьёва - Дж. Худельмайера без правила сокращения (354мин.)
• • Теоретические сведения (118мин.)
  • Примеры решения некоторых типов упражнений (118мин.)
  • Упражнения для самостоятельного решения (105мин.)
  • Интуиционистские пропозициональные логики: секвенциальное исчисление Н. Н. Воробьёва - Дж. Худельмайера без правила сокращения (12мин.)
• Упражнение 4L. Интуиционистские пропозициональные логики: логика второго порядка Рrор2 (184мин.)
• • Теоретические сведения (105мин.)
  • Примеры решения некоторых типов упражнений (26мин.)
  • Задачи для самостоятельного решения (52мин.)
  • Интуиционистские пропозициональные логики: логика второго порядка Рrор2 (16мин.)
• Упражнение 5L. Интуиционистская предикатная логика: минимальная логика Pred (249мин.)
• • Теоретические сведения (157мин.)
  • Примеры решения некоторых типов упражнений (13мин.)
  • Упражнения для самостоятельного решения (79мин.)
  • Интуиционистская предикатная логика: минимальная логика Pred (12мин.)

Литература

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

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

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

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

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

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