Switch to: References

Add citations

You must login to add citations.
  1. Comparing cubes of typed and type assignment systems.Steffen van Bakel, Luigi Liquori, Simona Ronchi Della Rocca & Pawel Urzyczyn - 1997 - Annals of Pure and Applied Logic 86 (3):267-303.
    We study the cube of type assignment systems, as introduced in Giannini et al. 87–126), and confront it with Barendregt's typed gl-cube . The first is obtained from the latter through applying a natural type erasing function E to derivation rules, that erases type information from terms. In particular, we address the question whether a judgement, derivable in a type assignment system, is always an erasure of a derivable judgement in a corresponding typed system; we show that this property holds (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • On the role of implication in formal logic.Jonathan P. Seldin - 2000 - Journal of Symbolic Logic 65 (3):1076-1114.
    Evidence is given that implication (and its special case, negation) carry the logical strength of a system of formal logic. This is done by proving normalization and cut elimination for a system based on combinatory logic or λ-calculus with logical constants for and, or, all, and exists, but with none for either implication or negation. The proof is strictly finitary, showing that this system is very weak. The results can be extended to a "classical" version of the system. They can (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • Meeting of the association for symbolic logic: Washington, D. C., 1985.Martin Davis, Edgar E. K. Lopez-Escobar & Wilfred Sieg - 1986 - Journal of Symbolic Logic 51 (4):1085-1092.
    Download  
     
    Export citation  
     
    Bookmark  
  • 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  
  • A weak absolute consistency proof for some systems of illative combinatory logic.M. W. Bunder - 1983 - Journal of Symbolic Logic 48 (3):771-776.
    Download  
     
    Export citation  
     
    Bookmark   3 citations