Теория типов - Type theory - Wikipedia

В математика, логика, и Информатика, а система типов это формальная система в котором каждый термин имеет «тип», который определяет его значение и операции, которые могут выполняться с ним. Теория типов академическое исследование систем типов.

Некоторые теории типов служат альтернативой теория множеств как основа математики. Две хорошо известные такие теории: Церковь Алонсо с типизированное λ-исчисление и Пер Мартин-Лёф с интуиционистская теория типов.

Теория типов была создана, чтобы избежать парадоксов в предыдущих основах, таких как наивная теория множеств, формальная логика и переписывать системы.

Теория типов тесно связана, а в некоторых случаях частично совпадает с ней. системы вычислительного типа, которые являются язык программирования функция, используемая для уменьшения ошибки.

История

Основная статья: История теории типов

Между 1902 и 1908 годами Бертран Рассел предложил различные "теории типа" в ответ на его открытие, что Готтлоб Фреге версия наивная теория множеств был поражен Парадокс Рассела. К 1908 году Рассел пришел к «разветвленной» теории типов вместе с «разветвленной» теорией типов.аксиома сводимости "оба из них занимали видное место в Уайтхед и Рассел с Principia Mathematica опубликовано между 1910 и 1913 годами. Они попытались разрешить парадокс Рассела, сначала создав иерархию типов, а затем назначив каждый конкретный математический (и, возможно, другой) объект типу. Сущности данного типа создаются исключительно из сущностей тех типов, которые находятся ниже в своей иерархии, что предотвращает присвоение сущности самой себе.

В 1920-е гг. Леон Чвистек и Фрэнк П. Рэмси предложил неразветвленную теорию типов, известную теперь как «теория простых типов» или теория простых типов, который разрушил иерархию типов в ранее разветвленной теории и как таковой не требовал аксиомы сводимости.

Обычно «теория типов» используется, когда эти типы используются с система перезаписи терминов. Самый известный ранний пример - Церковь Алонсо с просто типизированное лямбда-исчисление. Теория типов Чёрча^[1] помогла формальной системе избежать Парадокс Клини – Россера это повлияло на исходное нетипизированное лямбда-исчисление. Черч продемонстрировал, что он может служить основой математики, и был назван логика высшего порядка.

Некоторые другие теории включают: Пер Мартин-Лёф с интуиционистская теория типов, который был основой, используемой в некоторых областях конструктивная математика. Тьерри Кокванд с расчет конструкций и его производные являются основой, используемой Coq, Худой, и другие. Эта область является областью активных исследований, что продемонстрировано теория гомотопического типа.

Базовые концепты

Основная статья: Лямбда-куб

Современное представление систем типов в контексте теории типов стало систематизированным с помощью концептуальной основы, введенной Хенк Барендрегт^[2].

Тип, срок, значение

В системе теории типов срок противостоит тип. Например, 4, 2 + 2, и ${\displaystyle 2\cdot 2}$ все отдельные термины с типом нац для натуральных чисел. Традиционно за термином следует двоеточие и его тип, например 2: нат - это означает, что число 2 относится к типу нац. Помимо этого противопоставления и синтаксиса, мало что можно сказать о типах в этой общности, но часто они интерпретируются как своего рода набор (не обязательно наборы) значения что термин может оценивать. Обычно члены обозначают через е и типы по τ. Форма терминов и типов зависит от конкретной системы типов и уточняется некоторыми синтаксис и дополнительные ограничения правильная форма.

Среда набора, присвоение типа, оценка типа

Основная статья: Среда набора текста

Печатание обычно происходит в некоторых контекст или же среда обозначается символом ${\displaystyle \Gamma }$. Часто среда - это список пар ${\displaystyle e:\tau }$. Эту пару иногда называют назначение. Контекст завершает вышеуказанное противопоставление. Вместе они образуют суждение обозначенный ${\displaystyle \Gamma \vdash e:\tau }$.

Правила перезаписи, конвертация, редукция

Теории типов имеют явное вычисление, и это закодировано в правилах для переписывание термины. Они называются правила конвертации или, если правило работает только в одном направлении, снижение правило. Например, ${\displaystyle 2+2}$ и ${\displaystyle 4}$ синтаксически разные термины, но первое сводится ко второму. Это сокращение написано ${\displaystyle 2+2\twoheadrightarrow 4}$. Эти правила также устанавливают соответствующие эквивалентности между термином, написанным ${\displaystyle 2+2\equiv 4}$.

Период, термин ${\displaystyle 2+1}$ сводится к ${\displaystyle 3}$. С ${\displaystyle 3}$ не подлежит дальнейшему сокращению, это называется нормальная форма. Различные системы типизированное лямбда-исчисление в том числе просто типизированное лямбда-исчисление, Жан-Ив Жирар Система F, и Тьерри Коквана расчет конструкций находятся сильно нормализующий. В таких системах успешная проверка типа подразумевает доказательство прекращения срока.

Тип правила

Основная статья: Тип правила

По типу суждений и эквивалентностей правила вывода может использоваться для описания того, как система типов присваивает тип синтаксическим конструкциям (терминам), как и в естественный вычет. Чтобы иметь смысл, правила преобразования и типов обычно тесно связаны, например, в по уменьшение предмета имущество, которое могло бы установить часть прочность системы типов.

Проблемы с решением

Система типов естественным образом связана с проблемы решения из проверка типа, типируемость, и тип проживания.^[3]

Проверка типа

Основная статья: Проверка типа

Проблема решения проверка типа (сокращенно ${\displaystyle \Gamma \vdash e:\tau ?}$) является:

Учитывая типовое окружение ${\displaystyle \Gamma }$, термин ${\displaystyle e}$, а тип ${\displaystyle \tau }$, решите, является ли срок ${\displaystyle e}$ можно присвоить тип ${\displaystyle \tau }$ в типовой среде ${\displaystyle \Gamma }$.

Разрешимость проверки типов означает, что безопасность типа любого заданного текста программы (исходного кода) можно проверить.

Типичность

Основная статья: Типичность

Проблема решения типичность (сокращенно ${\displaystyle \exists \Gamma ,\tau .\Gamma \vdash e:\tau ?}$) является:

Учитывая срок ${\displaystyle e}$, решите, существует ли среда типа ${\displaystyle \Gamma }$ и тип ${\displaystyle \tau }$ так что срок ${\displaystyle e}$ можно присвоить тип ${\displaystyle \tau }$ в типовой среде ${\displaystyle \Gamma }$.

Вариант типизации: типизируемость относительно. типовая среда (сокращенно ${\displaystyle \exists \tau .\Gamma \vdash e:\tau ?}$), для которого окружение типов является частью входных данных. Если данный термин не содержит внешних ссылок (таких как свободные переменные терма), то типируемость совпадает с типируемостью по отношению к. среда пустого типа.

Типичность тесно связана с вывод типа. В то время как типируемость (как проблема решения) касается существования типа для данного термина, вывод типа (как проблема вычисления) требует вычисления фактического типа.

Тип проживания

Основная статья: Тип проживания

Проблема решения тип проживания (сокращенно ${\displaystyle \exists e.\Gamma \vdash e:\tau ?}$) является:

Учитывая типовое окружение ${\displaystyle \Gamma }$ и тип ${\displaystyle \tau }$, решите, существует ли термин ${\displaystyle e}$ которому можно присвоить тип ${\displaystyle \tau }$ в типовой среде ${\displaystyle \Gamma }$.

Парадокс Жирара показывает, что заселение типов тесно связано с согласованностью системы типов с соответствием Карри – Ховарда. Чтобы быть здоровой, такая система должна иметь необитаемые типы.

Противопоставление терминов и типов также может рассматриваться как одно из выполнение и Технические характеристики. К программный синтез (вычислительный аналог) размещения типа (см. ниже) может использоваться для построения (всех или частей) программ из спецификации, представленной в форме информации о типе.^[4]

Интерпретации теории типов

Теория типов тесно связана со многими областями активных исследований. В частности, соответствие Карри – Ховарда обеспечивает глубокий изоморфизм между интуиционистской логикой, типизированным лямбда-исчислением и декартово закрытыми категориями.

Интуиционистская логика

Основная статья: Переписка Карри – Ховарда

Помимо представления о типах как о совокупности значений термина, теория типов предлагает вторую интерпретацию противопоставления термина и типов. Типы можно рассматривать как предложения и условия как доказательства. В этом способе чтения набора тип функции ${\displaystyle \alpha \rightarrow \beta }$ рассматривается как значение, т.е. как предложение, что ${\displaystyle \beta }$ следует из ${\displaystyle \alpha }$.

Теория категорий

Основная статья: Декартова закрытая категория

В внутренний язык декартовой закрытой категории просто типизированное лямбда-исчисление. Это представление может быть распространено на другие типизированные лямбда-исчисления. Некоторые декартовы замкнутые категории, топои, были предложены в качестве общей установки для математики вместо традиционной теории множеств.

Отличие от теории множеств

Существует множество различных теорий множеств и множество различных систем теории типов, поэтому все, что следует ниже, является обобщением.

• Теория множеств построена на логике. Требуется отдельная система вроде логика предикатов под ним. В теории типов такие понятия, как «и» и «или», могут быть закодированы как типы в самой теории типов.
• В теории множеств элемент не ограничен одним множеством. В теории типов термины (как правило) принадлежат только к одному типу. (Там, где будет использоваться подмножество, теория типов имеет тенденцию использовать функция предиката который возвращает истину, если термин входит в подмножество, и возвращает ложь, если значение нет. Объединение двух типов можно определить как новый тип, называемый тип суммы, который содержит новые термины.)
• Теория множеств обычно кодирует числа как множества. (0 - пустой набор, 1 - набор, содержащий пустой набор, и т.д. См. Теоретико-множественное определение натуральных чисел.) Теория типов может кодировать числа как функции, используя Церковная кодировка или более естественно как индуктивные типы. Индуктивные типы создают новые константы для функция преемника и ноль, очень похожий на Аксиомы Пеано.
• Теория типов имеет простую связь с конструктивной математикой через Толкование BHK. Это может быть связано с логикой Изоморфизм Карри – Ховарда. И некоторые теории типов тесно связаны с Теория категорий.

Дополнительные особенности

Зависимые типы

Основная статья: Зависимые типы

А зависимый тип - это тип, который зависит от термина или другого типа. Таким образом, тип, возвращаемый функцией, может зависеть от аргумента функции.

Например, список ${\displaystyle \mathrm {nat} }$s длины 4 может быть другого типа, чем список ${\displaystyle \mathrm {nat} }$s длины 5. В теории типов с зависимыми типами можно определить функцию, которая принимает параметр «n» и возвращает список, содержащий «n» нулей. Вызов функции с 4 приведет к появлению члена с другим типом, чем если бы функция вызывалась с 5.

Зависимые типы играют центральную роль в интуиционистская теория типов и в дизайне функциональные языки программирования подобно Идрис, АТС, Агда и Эпиграмма.

Типы равенства

Многие системы теории типов имеют тип, который представляет равенство типов и терминов. Этот тип отличается от конвертируемого и часто обозначается пропозициональное равенство.

В интуиционистской теории типов тип равенства (также называемый типом идентичности) известен как ${\displaystyle I}$ для идентичности. Есть тип ${\displaystyle I\ A\ a\ b}$ когда ${\displaystyle A}$ это тип и ${\displaystyle a}$ и ${\displaystyle b}$ оба термина типа ${\displaystyle A}$. Срок типа ${\displaystyle I\ A\ a\ b}$ интерпретируется как означающее, что ${\displaystyle a}$ равно ${\displaystyle b}$.

На практике можно построить тип ${\displaystyle I\ \mathrm {nat} \ 3\ 4}$ но такого термина не будет. В интуиционистской теории типов новые термины равенства начинаются с рефлексивности. Если ${\displaystyle 3}$ это термин типа ${\displaystyle \mathrm {nat} }$, то существует терм типа ${\displaystyle I\ \mathrm {nat} \ 3\ 3}$. Более сложные равенства могут быть созданы путем создания рефлексивного члена и последующего сокращения с одной стороны. Так что если ${\displaystyle 2+1}$ это термин типа ${\displaystyle \mathrm {nat} }$, то есть член типа ${\displaystyle I\ \mathrm {nat} \ (2+1)\ (2+1)}$ и, уменьшив, сгенерируйте член типа ${\displaystyle I\ \mathrm {nat} \ (2+1)\ 3}$. Таким образом, в этой системе тип равенства означает, что два значения одного и того же типа могут быть преобразованы редукциями.

Наличие типа для равенства важно, потому что им можно управлять внутри системы. Обычно нельзя сказать, что два термина являются нет равный; вместо этого, как в Интерпретация Брауэра – Гейтинга – Колмогорова, мы отображаем ${\displaystyle \neg (a=b)}$ к ${\displaystyle (a=b)\to \bot }$, куда ${\displaystyle \bot }$ это нижний тип не имеющий значений. Существует термин с типом ${\displaystyle (I\ \mathrm {nat} \ 3\ 4)\to \bot }$, но не одного типа ${\displaystyle (I\ \mathrm {nat} \ 3\ 3)\to \bot }$.

Теория гомотопического типа отличается от интуиционистская теория типов в основном за счет обработки типа равенства.

Индуктивные типы

Основная статья: Индуктивный тип

Система теории типов требует для работы некоторых основных терминов и типов. Некоторые системы строят их из функций, используя Церковная кодировка. В других системах есть индуктивные типы: набор базовых типов и набор конструкторы типов которые генерируют типы с хорошими свойствами. Например, некоторые рекурсивные функции вызываемые индуктивные типы гарантированно завершаются.

Коиндуктивные типы представляют собой бесконечные типы данных, создаваемые функцией, которая генерирует следующий элемент (ы). Видеть Коиндукция и Corecursion.

Индукция-индукция это функция для объявления индуктивного типа и семейства типов, которое зависит от индуктивного типа.

Индукционная рекурсия позволяет использовать более широкий диапазон типов с хорошим поведением, позволяя определять тип и рекурсивные функции, работающие с ним, одновременно.

Типы вселенной

Типы были созданы для предотвращения парадоксов, таких как Парадокс Рассела. Однако мотивы, которые приводят к этим парадоксам - способность говорить обо всех типах людей - все еще существуют. Итак, у многих теорий типов есть «тип вселенной», который содержит все Другой типы (а не себя).

В системах, где вы, возможно, захотите что-то сказать о типах юниверсов, существует иерархия типов юниверсов, каждый из которых содержит тот, который находится ниже в иерархии. Иерархия определяется как бесконечная, но утверждения должны относиться только к конечному числу уровней юниверса.

Универсальные типы типов особенно сложны в теории типов. Первоначальное предложение интуиционистской теории типов пострадало от Парадокс Жирара.

Вычислительная составляющая

Многие системы теории типов, такие как просто типизированное лямбда-исчисление, интуиционистская теория типов, а расчет конструкций, также являются языками программирования. То есть, говорят, что они имеют «вычислительную составляющую». Вычисление - это сокращение терминов языка с помощью правила переписывания.

Система теории типов, имеющая хорошо отлаженный вычислительный компонент, также имеет простую связь с конструктивной математикой через Толкование BHK.

Неконструктивная математика в этих системах возможна путем добавления операторов к продолжениям, таких как вызов с текущим продолжением. Однако эти операторы имеют тенденцию нарушать желаемые свойства, такие как каноничность и параметричность.

Теории типов

Основной

• Просто типизированное лямбда-исчисление который является логика высшего порядка;
• интуиционистская теория типов;
• система F;
• LF часто используется для определения других теорий типов;
• расчет конструкций и его производные.

Незначительный

• Автомат;
• Теория типа ST;
• UTT (унифицированная теория зависимых типов Лаоса)
• некоторые формы комбинаторная логика;
• другие определены в лямбда-куб;
• другие под именем типизированное лямбда-исчисление;
• другие под именем система чистых типов.

Активный

• Теория гомотопического типа исследуется.

Практическое влияние

Языки программирования

Основная статья: Система типов

Существует обширное пересечение и взаимодействие между областями теории типов и систем типов. Системы типов - это функция языка программирования, предназначенная для выявления ошибок. Любой статический программный анализ, например алгоритмы проверки типов в семантический анализ фаза компилятор, имеет отношение к теории типов.

Ярким примером является Агда, язык программирования, который использует UTT (унифицированная теория зависимых типов Луо) для своей системы типов. Язык программирования ML был разработан для манипулирования теориями типов (см. LCF ), и их собственная система типов сильно повлияла на них.

Математические основы

Первый компьютерный помощник, названный Автомат, использовал теорию типов для кодирования математики на компьютере. Мартин-Лёф специально разработал интуиционистская теория типов закодировать все математика, чтобы служить новым основанием для математики. Продолжаются исследования математических основ с использованием теория гомотопического типа.

Математики, работающие в теория категорий уже испытывали трудности в работе с общепринятым фундаментом Теория множеств Цермело – Френкеля. Это привело к таким предложениям, как «Элементарная теория категорий множеств Лавера» (ETCS).^[5] Теория гомотопических типов продолжает эту линию, используя теорию типов. Исследователи изучают связи между зависимыми типами (особенно типом идентичности) и алгебраическая топология (конкретно гомотопия ).

Помощники доказательства

Основная статья: Помощник доказательства

Большая часть текущих исследований теории типов проводится пруфы, интерактивный помощники доказательства, и автоматические средства доказательства теорем. Большинство этих систем используют теорию типов в качестве математической основы для кодирования доказательств, что неудивительно, учитывая тесную связь между теорией типов и языками программирования:

• LF используется Двенадцать, часто для определения других теорий типа;
• многие теории типов, которые подпадают под логика высшего порядка используются Семейство испытателей HOL и ПВС;
• теория вычислительного типа используется NuPRL;
• расчет конструкций и его производные используются Coq, Матита, и Худой;
• UTT (Единая теория зависимых типов Луо) используется Агда который является одновременно языком программирования и помощником по проверке

Многие теории типов поддерживаются КОНСТРУКТОР ЛЕГО и Изабель. Изабель также поддерживает основы помимо теорий типов, таких как ZFC. Мицар является примером системы доказательств, которая поддерживает только теорию множеств.

Лингвистика

Теория типов также широко используется в формальные теории семантики из естественные языки, особенно Грамматика Монтегю и его потомки. Особенно, категориальные грамматики и предгрупповые грамматики широко использовать конструкторы типов для определения типов (имя существительное, глаголи др.) слов.

Самая обычная конструкция принимает основные типы ${\displaystyle e}$ и ${\displaystyle t}$ для частных лиц и истинные ценности соответственно, и рекурсивно определяет набор типов следующим образом:

• если ${\displaystyle a}$ и ${\displaystyle b}$ типы, значит, тоже ${\displaystyle \langle a,b\rangle }$;
• ничего, кроме основных типов, и то, что можно построить из них с помощью предыдущего предложения, является типами.

Сложный тип ${\displaystyle \langle a,b\rangle }$ это тип функции от сущностей типа ${\displaystyle a}$ объектам типа ${\displaystyle b}$. Таким образом, есть такие типы, как ${\displaystyle \langle e,t\rangle }$ которые интерпретируются как элементы набора функций от сущностей до истинностных значений, т.е. индикаторные функции наборов сущностей. Выражение типа ${\displaystyle \langle \langle e,t\rangle ,t\rangle }$ - это функция от наборов сущностей к истинностным значениям, то есть (индикаторная функция) набора наборов. Этот последний тип обычно считается типом квантификаторы естественного языка, подобно все или же никто (Монтегю 1973, Barwise и Купер 1981).

Социальные науки

Грегори Бейтсон ввел теорию логических типов в общественные науки; его представления о двойной переплет и логические уровни основаны на теории типов Рассела.

Отношение к теории категорий

Хотя первоначальная мотивация теория категорий был далек от фундаментализма, оказалось, что эти две области имеют глубокую связь. В качестве Джон Лейн Белл пишет: "На самом деле категории могут самих себя рассматриваться как типовые теории определенного вида; один только этот факт указывает на то, что теория типов гораздо более тесно связана с теорией категорий, чем с теорией множеств ». Короче говоря, категорию можно рассматривать как теорию типов, рассматривая ее объекты как типы (или сорта), т. е.« грубо говоря , категорию можно рассматривать как теорию типов, лишенную синтаксиса ». Таким образом, следует ряд важных результатов:^[6]

• декартовы закрытые категории соответствуют типизированному λ-исчислению (Ламбек, 1970);
• C-моноиды (категории с продуктами и экспонентами и один нетерминальный объект) соответствуют нетипизированному λ-исчислению (независимо наблюдаемому Ламбеком и Дана Скотт около 1980 г.);
• локально декартовы закрытые категории соответствуют Теории типа Мартина-Лёфа (Сили, 1984).

Взаимодействие, известное как категориальная логика, с тех пор является предметом активных исследований; см., например, монографию Джейкобса (1999).

Смотрите также

• Тип данных для конкретных типов данных в программировании
• Теория предметной области
• Тип (теория модели)
• Система типов для более практического обсуждения систем типов для языков программирования
• Универсальные основы

Примечания

1. Церковь, Алонсо (1940). «Формулировка простой теории типов». Журнал символической логики. 5 (2): 56–68. Дои:10.2307/2266170. JSTOR  2266170.
2. Барендрегт, Хенк (1991). «Введение в системы обобщенных типов». Журнал функционального программирования. 1 (2): 125–154. Дои:10,1017 / с0956796800020025. HDL:2066/17240. ISSN  0956-7968.
3. Хенк Барендрегт; Вил Деккерс; Ричард Статман (20 июня 2013 г.). Лямбда-исчисление с типами. Издательство Кембриджского университета. п. 66. ISBN  978-0-521-76614-2.
4. Heineman, Джордж Т .; Бессай, Ян; Дуддер, Борис; Rehof, Якоб (2016). «Долгий и извилистый путь к модульному синтезу». Использование формальных методов, верификации и валидации: основные методы. ISoLA 2016. Конспект лекций по информатике. 9952. Springer. С. 303–317. Дои:10.1007/978-3-319-47166-2_21.
5. ETCS в nLab
6. Белл, Джон Л. (2012). «Типы, наборы и категории» (PDF). В Канамори, Акихиро (ред.). Наборы и расширения в двадцатом веке. Справочник по истории логики. 6. Эльзевир. ISBN  978-0-08-093066-4.

Рекомендации

• Фермер, Уильям М. (2008). «Семь достоинств простой теории типов». Журнал прикладной логики. 6 (3): 267–286. Дои:10.1016 / j.jal.2007.11.001.

дальнейшее чтение

• Aarts, C .; Backhouse, R .; Hoogendijk, P .; Voermans, E .; ван дер Вуде, Дж. (декабрь 1992 г.). «Реляционная теория типов данных». Technische Universiteit Eindhoven.
• Эндрюс Б., Питер (2002). Введение в математическую логику и теорию типов: к истине через доказательство (2-е изд.). Kluwer. ISBN  978-1-4020-0763-7.
• Джейкобс, Барт (1999). Категориальная логика и теория типов. Исследования по логике и основам математики. 141. Эльзевир. ISBN  978-0-444-50170-7. Подробно описывает теорию типов, включая расширения полиморфных и зависимых типов. Дает категориальная семантика.
• Карделли, Лука (1996). «Типовые системы». У Такера, Аллена Б. (ред.). Справочник по информатике и инженерии. CRC Press. С. 2208–36. ISBN  9780849329098.
• Коллинз, Джордан Э. (2012). История теории типов: развитие после второго издания «Principia Mathematica». Lambert Academic Publishing. HDL:11375/12315. ISBN  978-3-8473-2963-3. Предоставляет исторический обзор развития теории типов с акцентом на упадок теории как основы математики в течение четырех десятилетий после публикации второго издания «Principia Mathematica».
• Констебль, Роберт Л. (2012) [2002]. «Наивная теория вычислительного типа» (PDF). In Schwichtenberg, H .; Steinbruggen, R. (ред.). Доказательства и надежность системы. Серия "Наука НАТО" II. 62. Springer. С. 213–259. ISBN  9789401004138. Задуманный как аналог теории типов Пол Халмос s (1960) Наивная теория множеств
• Кокванд, Тьерри (2018) [2006]. "Теория типов". Стэнфордская энциклопедия философии.
• Томпсон, Саймон (1991). Теория типов и функциональное программирование. Аддисон-Уэсли. ISBN  0-201-41667-0.
• Хиндли, Дж. Роджер (2008) [1995]. Основная теория простых типов. Издательство Кембриджского университета. ISBN  978-0-521-05422-5. Хорошее введение в простую теорию типов для компьютерных ученых; Однако описанная система не совсем соответствует СТТ Черча. Обзор книги
• Kamareddine, Fairouz D .; Лаан, Тван; Недерпелт, Роб П. (2004). Современный взгляд на теорию типов: от истоков до наших дней. Springer. ISBN  1-4020-2334-0.
• Феррейрос, Хосе; Домингес, Хосе Феррейрос (2007). «X. Логика и теория типов в межвоенный период». Лабиринт мысли: история теории множеств и ее роль в современной математике (2-е изд.). Springer. ISBN  978-3-7643-8349-7.
• Лаан, Т.Д.Л. (1997). Эволюция теории типов в логике и математике (PDF) (Кандидат наук). Эйндховенский технологический университет. Дои:10.6100 / IR498552. ISBN  90-386-0531-5.

внешняя ссылка

• Роберт Л. Констебль (ред.). «Вычислительная теория типов». Scholarpedia.
• Форум ТИПЫ - модерируемый форум по электронной почте, посвященный теории типов в информатике, действующий с 1987 года.
• Книга Нупрл: "Введение в теорию типов. "
• Типы Конспект лекций по проекту летних школ 2005–2008 гг.
  • В 2005 летняя школа имеет вводные лекции