David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Ezio Di Nucci
Jack Alan Reynolds
Learn more about PhilPapers
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)|
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
Wil Dekkers, Martin Bunder & Henk Barendregt (1998). Completeness of the Propositions-as-Types Interpretation of Intuitionistic Logic Into Illative Combinatory Logic. Journal of Symbolic Logic 63 (3):869-890.
Henk Barendregt, Martin Bunder & Wil Dekkers (1993). Systems of Illative Combinatory Logic Complete for First-Order Propositional and Predicate Calculus. Journal of Symbolic Logic 58 (3):769-788.
Martin Bunder & Wil Dekkers (2001). Pure Type Systems with More Liberal Rules. Journal of Symbolic Logic 66 (4):1561-1580.
M. W. Bunder (1979). On the Equivalence of Systems of Rules and Systems of Axioms in Illative Combinatory Logic. Notre Dame Journal of Formal Logic 20 (3):603-608.
M. W. Bunder (1988). Arithmetic Based on the Church Numerals in Illative Combinatory Logic. Studia Logica 47 (2):129 - 143.
M. W. Bunder (1983). A Weak Absolute Consistency Proof for Some Systems of Illative Combinatory Logic. Journal of Symbolic Logic 48 (3):771-776.
Tijn Borghuis (1998). Modal Pure Type Systems. Journal of Logic, Language and Information 7 (3):265-296.
J. Roger Hindley (1972). Introduction to Combinatory Logic. Cambridge [Eng.]University Press.
M. W. Bunder (1977). Consistency Notions in Illative Combinatory Logic. Journal of Symbolic Logic 42 (4):527-529.
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 (1982). Illative Combinatory Logic Without Equality as a Primitive Predicate. Notre Dame Journal of Formal Logic 23 (1):62-70.
M. W. Bunder (1980). Significance and Illative Combinatory Logics. Notre Dame Journal of Formal Logic 21 (2):380-384.
J. W. Klop (1980). Combinatory Reduction Systems. Mathematisch Centrum.
Added to index2010-08-24
Total downloads178 ( #19,326 of 1,796,189 )
Recent downloads (6 months)66 ( #8,620 of 1,796,189 )
How can I increase my downloads?