Лямбда-куб Хенка Барендрегта.
Слайды к докладу в PDF.
Мой перевод (с некоторыми, незначительными комментариями) первого раздела пятой главы замечательного обзора Хенка Барендрегта: Henk Barendregt, Lambda calculi with types, в Handbook of Logic in Computer Science. (Старая версия перевода.)