Lambda cube

Initialement proposé par Henk Barendregt^[1], le ${\displaystyle \lambda }$-cube permet de visualiser les différentes dimensions pour lesquelles le calcul des constructions apporte une généralisation par rapport au lambda-calcul simplement typé où un terme ne peut dépendre que d'un autre terme. Chaque axe représente une nouvelle forme d'abstraction :

• Terme dépendant de type : le polymorphisme (d'où le Système F);
• Type dépendant de type : présence d'opérateurs de types ;
• Type dépendant de terme.

Cet article est une ébauche concernant la logique.