Switch to: References

Add citations

You must login to add citations.
  1. Equivalences between Pure Type Systems and Systems of Illative Combinatory Logic.M. W. Bunder & W. J. M. Dekkers - 2005 - Notre Dame Journal of Formal Logic 46 (2):181-205.
    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 (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  • Bunder’s paradox.Michael Caie - 2020 - Review of Symbolic Logic 13 (4):829-844.
    Systems ofillative logicare logical calculi formulated in the untypedλ-calculus supplemented with certain logical constants.1In this short paper, I consider a paradox that arises in illative logic. I note two prima facie attractive ways of resolving the paradox. The first is well known to be consistent, and I briefly outline a now standard construction used by Scott and Aczel that establishes this. The second, however, has been thought to be inconsistent. I show that this isn’t so, by providing a nonempty class (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
    		•