Чистая система типов (система обобщенных типов) — форма типизированного лямбда-исчисления, допускающая произвольное количество сортов переменных и зависимостей между ними. Разработана независимо Стефано Берарди (1988) и Яном Терловым (1989).
Чистую систему типов можно рассматривать как обобщение лямбда-куба, подразумевая, что каждой из его вершин соответствует экземпляр чистой системы типов с двумя сортами переменных (подобный взгляд высказывал автор идеи лямбда-куба Барендрегт).
Примечания
Категория:Теория типов Категория:Лямбда-исчисление Категория:Теория доказательств