Вычислительная теория типов [1/5] - Роберт Харпер - OPLSS 2018

Летняя школа языков программирования в Орегоне Параллелизм и конкуренция 3-21 июля 2018 г. Университет Орегона https://www.cs.uoregon.edu/research/s... Название: Вычислительная теория типов [1/5] Докладчик: Роберт Харпер, Университет Карнеги-Меллона Дата: понедельник, 16 июля 2018 г., сессия 1 Темы: фундаментальная предпосылка конструктивизма теория типов как основа всей математики теория типов как язык программирования теория истины против теории формального доказательства детерминированная операциональная семантика абстрактный синтаксис с привязкой, областью видимости и заменой формы выражения формы суждений: значения и правила переходов производное понятие бинарные диаграммы решений типы как спецификации поведения программы суждения как формы выражения алгоритмы как средства коммуникации поведенческие против структурных выражений Типы и значения — это программы Семейства типов Семейства типов с индексацией по типам (также известные как зависимые типы) Гипотетические/общие суждения Функциональность: соблюдение равенства индексов Что такое равенство типов? Экви-удовлетворение Предварительный обзор многомерной/кубической теории типов Значения суждений, также известные как объяснения значений, или вычислительная семантика Равенство канонических типов, также известные как значения типов Лемма о расширении заголовка, также известная как обратное выполнение © 2018, Университет Орегона