Refining the Barendregt cube using parameters

The Barendregt Cube (introduced in [3]) is a framework in which eight important typed ¿-calculi are described in a uniform way. Moreover, many type systems (like Automath [18], LF [11], ML [17], and system F [10]) can be related to one of these eight systems. Further- more, via the propositions-as-types principle, many logical systems can be described in the Barendregt Cube as well (see for instance [9]). However, there are important systems (including AUTOMATH, LF and ML) that cannot be adequately placed in the Barendregt Cube or in the larger framework of Pure Type Systems. In this paper we add a parameter mechanism to the systems of the Barendregt Cube. In doing so, we obtain a refinement of the Cube. In this refined Barendregt Cube, systems like Automath, LF, and ML can be described more naturally and accurately than in the original Cube.