4 found
  1.  36
    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.
  2.  20
    The Semantics of Entailment Omega.Yoko Motohama, Robert K. Meyer & Mariangiola Dezani-Ciancaglini - 2002 - Notre Dame Journal of Formal Logic 43 (3):129-145.
    This paper discusses the relation between the minimal positive relevant logic B and intersection and union type theories. There is a marvelous coincidence between these very differently motivated research areas. First, we show a perfect fit between the Intersection Type Discipline ITD and the tweaking BT of B, which saves implication and conjunction but drops disjunction . The filter models of the -calculus (and its intimate partner Combinatory Logic CL) of the first author and her coauthors then become theory models (...)
    Direct download (8 more)  
    Export citation  
    Bookmark   6 citations  
  3.  9
    Combining Type Disciplines.Felice Cardone, Mariangiola Dezani-Ciancaglini & Ugo de'Liguoro - 1994 - Annals of Pure and Applied Logic 66 (3):197-230.
    We present a type inference system for pure λ-calculus which includes, in addition to arrow types, also universal and existential type quantifiers, intersection and union types, and type recursion. The interest of this system lies in the fact that it offers a possibility to study in a unified framework a wide range of type constructors. We investigate the main syntactical properties of the system, including an analysis of the preservation of types under parallel reduction strategies, leading to a form of (...)
    Direct download (4 more)  
    Export citation  
  4.  30
    The "Relevance" of Intersection and Union Types.Mariangiola Dezani-Ciancaglini, Silvia Ghilezan & Betti Venneri - 1997 - Notre Dame Journal of Formal Logic 38 (2):246-269.
    The aim of this paper is to investigate a Curry-Howard interpretation of the intersection and union type inference system for Combinatory Logic. Types are interpreted as formulas of a Hilbert-style logic L, which turns out to be an extension of the intuitionistic logic with respect to provable disjunctive formulas (because of new equivalence relations on formulas), while the implicational-conjunctive fragment of L is still a fragment of intuitionistic logic. Moreover, typable terms are translated in a typed version, so that --typed (...)
    Direct download (6 more)  
    Export citation  
    Bookmark   1 citation