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 (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • (1 other version)Pure type systems with more liberal rules.Martin Bunder & Wil Dekkers - 2001 - Journal of Symbolic Logic 66 (4):1561-1580.
    Pure Type Systems, PTSs, introduced as a generalisation of the type systems of Barendregt's lambda-cube, provide a foundation for actual proof assistants, aiming at the mechanic verification of formal proofs. In this paper we consider simplifications of some of the rules of PTSs. This is of independent interest for PTSs as this produces more flexible PTS-like systems, but it will also help, in a later paper, to bridge the gap between PTSs and systems of Illative Combinatory Logic. First we consider (...)
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • Variants of the basic calculus of constructions.M. W. Bunder & Jonathan P. Seldin - 2004 - Journal of Applied Logic 2 (2):191-217.
    Download  
     
    Export citation  
     
    Bookmark  
  • Interpreting HOL in the calculus of constructions.Jonathan P. Seldin - 2004 - Journal of Applied Logic 2 (2):173-189.
    Download  
     
    Export citation  
     
    Bookmark