Switch to: References

Add citations

You must login to add citations.
  1. Church-Rosser property and intersection types.George Koletsos & George Stavrinos - 2008 - Australasian Journal of Logic 6:37-54.
    We give a proof via reducibility of the Church-Rosser property for the system D of λ-calculus with intersection types. As a consequence we can get the confluence property for developments directly, without making use of the strong normalization property for developments, by using only the typability in D and a suitable embedding of developments in this system. As an application we get a proof of the Church-Rosser theorem for the untyped λ-calculus.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  • Typing untyped λ-terms, or reducibility strikes again!Jean Gallier - 1998 - Annals of Pure and Applied Logic 91 (2-3):231-270.
    It was observed by Curry that when λ-terms can be assigned types, for example, simple types, these terms have nice properties . Coppo, Dezani, and Veneri, introduced type systems using conjunctive types, and showed that several important classes of terms can be characterized according to the shape of the types that can be assigned to these terms. For example, the strongly normalizable terms, the normalizable terms, and the terms having head-normal forms, can be characterized in some systems and Ω. The (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation