Intersection types for combinatory logic

DOI10.1016/0304-3975(92)90306-ZzbMath0771.03004OpenAlexW1966026637WikidataQ126989194 ScholiaQ126989194MaRDI QIDQ1199823

J. Roger Hindley, Mariangiola Dezani-Ciancaglini

Publication date: 17 January 1993

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(92)90306-z

zbMATH Keywords

combinatory logicequivalence between \(\lambda\) terms and combinators with intersection typesextension of the Curry style type assignment system

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Related Items (12)

Proof-functional connectives and realizability ⋮ Lambda terms definable as combinators ⋮ Normalization results for typeable rewrite systems ⋮ Combinatory logic and the semantics of substructural logics ⋮ The ``relevance of intersection and union types ⋮ The semantics of entailment omega ⋮ Calculi, types and applications: essays in honour of M. Coppo, M. Dezani-Ciancaglini and S. Ronchi della Rocca ⋮ Finite Combinatory Logic with Intersection Types ⋮ Approximation and normalization results for typeable term rewriting systems ⋮ Types with intersection: An introduction ⋮ Principal types of BCK-lambda-terms ⋮ Normalization, approximation, and semantics for combinator systems

Uses Software

• Forsythe

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Principal type schemes for an extended type theory
• Type theories, normal forms, and \(D_{\infty}\)-lambda-models
• Types with intersection: An introduction
• Abstraction problems in combinatory logic: A compositive approach
• A filter lambda model and the completeness of type assignment
• Characterization theorems for a filter lambda model
• Functional Characters of Solvable Terms
• The Relation between Computational and Denotational Properties for Scott’s ${\text{D}}_\infty $-Models of the Lambda-Calculus
• Combinatory Reductions and Lambda Reductions Compared
• Standard and Normal Reductions
• Another algorithm for bracket abstraction

This page was built for publication: Intersection types for combinatory logic