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.
My Menu
Saved Items

Refining the Barendregt Cube using Parameters

Fairouz KamareddineContact Information, Twan LaanContact Information and Rob NederpeltContact Information

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

Contact Information Fairouz Kamareddine
Email: fairouz@cee.hw.ac.uk

Contact Information Twan Laan
Email: twan.laan@wxs.nl

Contact Information Rob Nederpelt
Email: r.p.nederpelt@tue.nl
Fulltext Preview (Small, Large)
Image of the first page of the fulltext

References secured to subscribers.



Export this chapter
Export this chapter as RIS | Text
 
Remote Address: 38.107.191.108 • Server: mpweb02
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)