Switch to: References

Add citations

You must login to add citations.
  1. Cut-Elimination in the Strict Intersection Type Assignment System is Strongly Normalizing.Steffen van Bakel - 2004 - Notre Dame Journal of Formal Logic 45 (1):35-63.
    This paper defines reduction on derivations (cut-elimination) in the Strict Intersection Type Assignment System of an earlier paper and shows a strong normalization result for this reduction. Using this result, new proofs are given for the approximation theorem and the characterization of normalizability of terms using intersection types.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  • Term-Space Semantics of Typed Lambda Calculus.Ryo Kashima, Naosuke Matsuda & Takao Yuyama - 2020 - Notre Dame Journal of Formal Logic 61 (4):591-600.
    Barendregt gave a sound semantics of the simple type assignment system λ → by generalizing Tait’s proof of the strong normalization theorem. In this paper, we aim to extend the semantics so that the completeness theorem holds.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  • Non-idempotent intersection types for the Lambda-Calculus.Antonio Bucciarelli, Delia Kesner & Daniel Ventura - 2017 - Logic Journal of the IGPL 25 (4):431-464.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark