Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
|
 |
Refining the Barendregt Cube using Parameters
| |
|
Refining the Barendregt Cube using Parameters
Fairouz Kamareddine6 , Twan Laan7 and Rob Nederpelt8 
| (6) |
Computing and Electrical Engineering, Heriot-Watt Univ., Riccarton, Edinburgh, EH14 4AS, Scotland |
| (7) |
Molenstraat 208, 5701, KL Helmond, the Netherlands |
| (8) |
Mathematics and Computing Science, Eindhoven Univ. of Technology, P.O.Box 513, 5600 MB Eindhoven, the Netherlands |
Abstract
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.
This work has been partially supported by EPSRC grant numbers GR/L36963 and GR/L15685, by a Royal Society ESEP grant and by
the British council and the Dutch research council NWO.
Kamareddine is grateful to Eindhoven University of Technology for its hospitality and support during the preparation of this
article.
Fulltext Preview (Small, Large)
 References secured to subscribers.
|
|
|
|
|
|