Википедия
Лямбда-куб
Ля́мбда-куб (λ-куб) — наглядная классификация восьми типизированных лямбда-исчислений с явным приписыванием типов (систем, типизированных по Чёрчу ). Куб организован в соответствии с возможными зависимостями между типами и термами этого исчисления и формирует естественную структуру для исчисления конструкций . Идею λ-куба предложил в 1991 году нидерландский логик и математик Хенк Барендрегт .