Intersection types for combinatory logic

DOI10.1016/0304-3975(92)90306-ZMaRDI QIDQ1199823zbMATH OpenOpenAlexWikidataFDO

Authors Mariangiola Dezani-Ciancaglini, J. Roger Hindley

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)

Recommendations

• Intersection types for lambda-terms and combinators and their logics
• Intersection Types as Logical Formulae
• Intersection types for λGtz-calculus
• A classification of intersection type systems
• Intersection-types à la Church

Cites work

• 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?)
• 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
• 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

Cited in

(25)

• Calculi, types and applications: essays in honour of M. Coppo, M. Dezani-Ciancaglini and S. Ronchi della Rocca
• Principal types of BCK-lambda-terms
• The ``relevance of intersection and union types
• Proof-functional connectives and realizability
• Intersection types and λ-definability
• Normalization results for typeable rewrite systems
• Finite combinatory logic with intersection types
• scientific article; zbMATH DE number 1189067 (Why is no real title available?)
• scientific article; zbMATH DE number 3941502 (Why is no real title available?)
• Normalization, approximation, and semantics for combinator systems
• scientific article; zbMATH DE number 7526053 (Why is no real title available?)
• Towards probabilistic reasoning in type theory -- the intersection type case
• Intersection types for lambda-terms and combinators and their logics
• scientific article; zbMATH DE number 2185668 (Why is no real title available?)
• Intersection types and computational rules
• scientific article; zbMATH DE number 4143942 (Why is no real title available?)
• Combinatory logic and the semantics of substructural logics
• How to think of intersection types as Cartesian products
• scientific article; zbMATH DE number 176126 (Why is no real title available?)
• Approximation and normalization results for typeable term rewriting systems
• scientific article; zbMATH DE number 1841834 (Why is no real title available?)
• Types with intersection: An introduction
• The semantics of entailment omega
• Intersection, Universally Quantified, and Reference Types
• Lambda terms definable as combinators

Describes a project that uses

Uses Software

• Forsythe

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)