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