Лямбда-куб

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