Equivalences between Pure Type Systems and Systems of Illative Combinatory Logic

Notre Dame Journal of Formal Logic 46 (2):181-205 (2005)
Abstract
Pure Type Systems, PTSs, were introduced as a generalization of the type systems of Barendregt's lambda cube and were designed to provide a foundation for actual proof assistants which will verify proofs. Systems of illative combinatory logic or lambda calculus, ICLs, were introduced by Curry and Church as a foundation for logic and mathematics. In an earlier paper we considered two changes to the rules of the PTSs which made these rules more like ICL rules. This led to four kinds of PTSs. Most importantly PTSs are about statements of the form M:A, where M is a term and A a type. In ICLs there are no explicit types and the statements are terms. In this paper we show that for each of the four forms of PTS there is an equivalent form of ICL, sometimes if certain conditions hold
Keywords pure type systems   illative combinatory logic
Categories (categorize this paper)
Options
 Save to my reading list
Follow the author(s)
My bibliography
Export citation
Find it on Scholar
Edit this record
Mark as duplicate
Revision history Request removal from index
 
Download options
PhilPapers Archive


Upload a copy of this paper     Check publisher's policy on self-archival     Papers currently archived: 10,273
External links
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library
References found in this work BETA

No references found.

Citations of this work BETA

No citations found.

Similar books and articles
Tijn Borghuis (1998). Modal Pure Type Systems. Journal of Logic, Language and Information 7 (3):265-296.
M. W. Bunder (1970). A Paradox in Illative Combinatory Logic. Notre Dame Journal of Formal Logic 11 (4):467-470.
M. W. Bunder (1979). Scott's Models and Illative Combinatory Logic. Notre Dame Journal of Formal Logic 20 (3):609-612.
M. W. Bunder (1979). $\Lambda$-Elimination in Illative Combinatory Logic. Notre Dame Journal of Formal Logic 20 (3):628-630.
M. W. Bunder (1980). Significance and Illative Combinatory Logics. Notre Dame Journal of Formal Logic 21 (2):380-384.
Analytics

Monthly downloads

Added to index

2010-08-24

Total downloads

3 ( #267,324 of 1,096,265 )

Recent downloads (6 months)

1 ( #218,857 of 1,096,265 )

How can I increase my downloads?

My notes
Sign in to use this feature


Discussion
Start a new thread
Order:
There  are no threads in this forum
Nothing in this forum yet.