TY - GEN

T1 - Refining the Barendregt cube using parameters

AU - Kamareddine, F.

AU - Laan, T.D.L.

AU - Nederpelt, R.P.

PY - 2001

Y1 - 2001

N2 - 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.

AB - 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.

U2 - 10.1007/3-540-44716-4_24

DO - 10.1007/3-540-44716-4_24

M3 - Conference contribution

SN - 3-540-41639-7

T3 - Lecture Notes in Computer Science

SP - 375

EP - 389

BT - Functional and logic programming : proceedings 5th international symposium, FLOPS 2001, Tokyo, Japan, March 7-9, 2001

A2 - Kuchen, H.

A2 - Ueda, K.

PB - Springer

CY - Berlin

ER -