Refining the Barendregt cube using parameters

F. Kamareddine, T.D.L. Laan, R.P. Nederpelt

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

7 Citations (Scopus)


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.
Original languageEnglish
Title of host publicationFunctional and logic programming : proceedings 5th international symposium, FLOPS 2001, Tokyo, Japan, March 7-9, 2001
EditorsH. Kuchen, K. Ueda
Place of PublicationBerlin
ISBN (Print)3-540-41639-7
Publication statusPublished - 2001

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


Dive into the research topics of 'Refining the Barendregt cube using parameters'. Together they form a unique fingerprint.

Cite this