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  
  • Variants of the basic calculus of constructions.M. W. Bunder & Jonathan P. Seldin - 2004 - Journal of Applied Logic 2 (2):191-217.