Лямбда-куб

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