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 (...) of these calculi. (The logician's "theory" is the algebraist's "filter".) The coincidence extends to a dual interpretation of key particles—the subtype translates to provable , type intersection to conjunction , function space to implication, and whole domain to the (trivially added but trivial) truth T. This satisfying ointment contains a fly. For it is right, proper, and to be expected that type union should correspond to the logical disjunction of B. But the simulation of functional application by a fusion (or modus ponens product) operation on theories leaves the key Bubbling lemma of work on ITD unprovable for the -prime theories now appropriate for the modeling. The focus of the present paper lies in an appeal to Harrop theories which are (a) prime and (b) closed under fusion. A version of the Bubbling lemma is then proved for Harrop theories, which accordingly furnish a model of and CL. (shrink)

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 (...) the subject-reduction property. We describe a model for this system where types are special subsets of a D∞ model for λ-calculus, without imposing any formal contractiveness constraint on types of the kind considered for a closely related system by MacQueen, Plotkin and Sethi. (shrink)

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 (...) combinatory logic terms are proved to completely codify the associated logical proofs. (shrink)