A typed lambda calculus with intersection types

DOI10.1016/j.tcs.2008.01.046zbMath1145.68009OpenAlexW2105663497MaRDI QIDQ930870

Lorenzo Bettini, Viviana Bono, Betti Venneri

Publication date: 24 June 2008

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

Full work available at URL: http://hdl.handle.net/2158/257190

zbMATH Keywords

parallelismlambda calculusintersection typestype inferenceshared resourcesChurch styleCurry style

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Combinatory logic and lambda calculus (03B40)

Related Items

On Isomorphisms of Intersection Types, Unnamed Item, Unnamed Item

Uses Software

• Forsythe

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Cut-elimination in the strict intersection type assignment system is strongly normalizing
• Lectures on the Curry-Howard isomorphism
• The semantics of entailment. III
• Intersection type assignment systems
• The ``relevance of intersection and union types
• The semantics of entailment omega
• Intersection types and lambda models
• Intersection-types à la Church
• The Relevance of Semantic Subtyping
• Intersection Typed λ-calculus
• A new type assignment for λ-terms
• A filter lambda model and the completeness of type assignment
• Semantic subtyping
• Intersection Types as Logical Formulae
• Type reconstruction in F_ω
• Intersection types for lambda-terms and combinators and their logics
• Hyperformulae, Parallel Deductions and Intersection Types
• Strongly typed flow-directed representation transformations (extended abstract)