The cube is a way of presenting the fine structure of Coquand's Calculus of Constructions relating that system to a variety of other typed lambda calculi. This idea is due to Henk Barendregt, and is presented in his Introduction to Generalised Type Systems which is my principle source in preparing this material.

The eight systems at the vertices of the cube are obtained by extending the simply typed lambda calculus () at the origin of the cube along one or more of the axes of the cube. The cube has six faces.

Axes:

	Face Without	Axis	Face With
	Standard	(,*)	Non-standard	2
		(,)		w
		(*,)		P

Faces:

	(,*)
(*,)	(,)	(*,)	(,)
	(,*)

Vertices:

(,*) (,) (*,*)							(,*) (,) (*,*) (*,)
(,*)   (*,*)							(,*)   (*,*) (*,)
(,) (*,*)							(,) (*,*) (*,)
(*,*)							(*,*) (*,)

The Simply Typed Lambda Calculus

Coordinates

	P	w	2
(*,*)

Weak Lambda Omega Related to the system POLYREC studied by Renardel de Lafalette [1985].

Coordinates

	P	w	2
(*,*)		(,)

Polymorphic or Second Order, Typed Lambda Calculus

Coordinates

	P	w	2
(*,*)			(,*)

The System F

Coordinates

	P	w	2
(*,*)		(,)	(,*)

LF Also corresponds to one of the AUTOMATH systems.

Coordinates

	P	w	2
(*,*)	(*,)

Weak Lambda P omega

Coordinates

	P	w	2
(*,*)	(*,)	(,)

Lambda P2

Coordinates

	P	w	2
(*,*)	(*,)		(,*)

The Calculus of Constructions

Coordinates

	P	w	2
(*,*)	(*,)	(,)	(,*)

---

© created 1995/11/12 modified 1999/9/20