Equivalences between Pure Type Systems and Systems of Illative Combinatory Logic

Notre Dame Journal of Formal Logic 46 (2):181-205 (2005)
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)
DOI 10.1305/ndjfl/1117755149
 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: 24,463
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.

Add more references

Citations of this work BETA

No citations found.

Add more citations

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.

Monthly downloads

Added to index


Total downloads

179 ( #22,991 of 1,925,510 )

Recent downloads (6 months)

1 ( #418,235 of 1,925,510 )

How can I increase my downloads?

My notes
Sign in to use this feature

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