Switch to: Citations

Add references

You must login to add references.
  1. A completeness result for the simply typed λμ-calculus.Karim Nour & Khelifa Saber - 2010 - Annals of Pure and Applied Logic 161 (1):109-118.
    In this paper, we define a realizability semantics for the simply typed $lambdamu$-calculus. We show that if a term is typable, then it inhabits the interpretation of its type. This result serves to give characterizations of the computational behavior of some closed typed terms. We also prove a completeness result of our realizability semantics using a particular term model.
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • An extension of the basic functionality theory for the $\lambda$-calculus.M. Coppo & M. Dezani-Ciancaglini - 1980 - Notre Dame Journal of Formal Logic 21 (4):685-693.
    Download  
     
    Export citation  
     
    Bookmark   9 citations  
  • Normalization without reducibility.René David - 2000 - Annals of Pure and Applied Logic 107 (1-3):121-130.
    In [gallier], general results (due to Coppo, Dezani and Veneri) relating properties of pure lambda terms and their typability in some systems with conjunctive types are proved in a uniform way by using the reducibility method.This paper gives a very short proof of the same results (actually, one of them is a bit stronger) using purely arithmetical methods.
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • A new type assignment for λ-terms.M. Coppo & M. Dezani-Ciancaglini - 1978 - Archive for Mathematical Logic 19 (1):139-156.
    Download  
     
    Export citation  
     
    Bookmark   14 citations  
  • A Filter lambda model and the completeness of type assignment.Henk Barendregt, Mario Coppo & Mariangiola Dezani-Ciancaglini - 1983 - Journal of Symbolic Logic 48 (4):931-940.
    Download  
     
    Export citation  
     
    Bookmark   24 citations