Intersection types for combinatory logic
The \(\to\) based type-language for \(\lambda\)-calculus was extended in 1977 by adding a universal type \(\omega\) and a connective \(\cap\) for the intersection of two types. This system, when suitably axiomatised, has the following desirable properties. (i) The set of types given to a \(\lambda\)-term does not change under \(\beta\)-conversion. (ii) The sets of normalizing and solvable \(\lambda\)-terms can be characterized neatly by the types of their members. (iii) \(\lambda\)-models can be built in which the interpretation of a \(\lambda\)-term coincides with the set of all types that can be assigned to it. The authors now propose an extension of the Curry style type assignment system for combinators to include \(\omega\) and \(\cap\) and they prove that, given certain conditions on combinator bases and abstraction algorithms, an exact equivalence between \(\lambda\) terms and combinators with intersection types can be achieved. As a result (i), (ii) (for strong reduction) and (iii) hold for combinators with intersection types. The conditions mentioned are satisfied by the most commonly used bases and abstraction algorithms. In the \(\lambda\)-system of intersection types the rule (\(\leq\)) can be replaced by a typed version of rule \((\eta)\). The authors present a combinatory logic version of this altered system, but this extension of typed combinatory logic is not so simple, but then neither was the extension from weak to \(\beta\eta\)-equality for untyped combinatory logic.
- A filter lambda model and the completeness of type assignment
- Abstraction problems in combinatory logic: A compositive approach
- Another algorithm for bracket abstraction
- Characterization theorems for a filter lambda model
- Combinatory Reductions and Lambda Reductions Compared
- Functional Characters of Solvable Terms
- scientific article; zbMATH DE number 3889502 (Why is no real title available?)
- scientific article; zbMATH DE number 3875232 (Why is no real title available?)
- scientific article; zbMATH DE number 3811535 (Why is no real title available?)
- scientific article; zbMATH DE number 3993540 (Why is no real title available?)
- scientific article; zbMATH DE number 3280068 (Why is no real title available?)
- Principal type schemes for an extended type theory
- Standard and Normal Reductions
- The Relation between Computational and Denotational Properties for Scott’s ${\text{D}}_\infty $-Models of the Lambda-Calculus
- Type theories, normal forms, and \(D_{\infty}\)-lambda-models
- Types with intersection: An introduction
- Types with intersection: An introduction
- Principal types of BCK-lambda-terms
- Proof-functional connectives and realizability
- Lambda terms definable as combinators
- Normalization results for typeable rewrite systems
- The ``relevance of intersection and union types
- The semantics of entailment omega
- How to think of intersection types as Cartesian products
- Normalization, approximation, and semantics for combinator systems
- Towards probabilistic reasoning in type theory -- the intersection type case
- Combinatory logic and the semantics of substructural logics
- Finite combinatory logic with intersection types
- scientific article; zbMATH DE number 2185668 (Why is no real title available?)
- scientific article; zbMATH DE number 4143942 (Why is no real title available?)
- Intersection, Universally Quantified, and Reference Types
- scientific article; zbMATH DE number 3941502 (Why is no real title available?)
- scientific article; zbMATH DE number 1189067 (Why is no real title available?)
- scientific article; zbMATH DE number 176126 (Why is no real title available?)
- Intersection types and λ-definability
- Approximation and normalization results for typeable term rewriting systems
- scientific article; zbMATH DE number 1377610 (Why is no real title available?)
- Intersection types for lambda-terms and combinators and their logics
- scientific article; zbMATH DE number 1841834 (Why is no real title available?)
- Intersection types and computational rules
- scientific article; zbMATH DE number 7526053 (Why is no real title available?)
- Finite combinatory logic with predicates
- Calculi, types and applications: essays in honour of M. Coppo, M. Dezani-Ciancaglini and S. Ronchi della Rocca
This page was built for publication: Intersection types for combinatory logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1199823)
