Intersection types and lambda models

DOI10.1016/J.TCS.2006.01.004zbMath1088.68031OpenAlexW2139609129MaRDI QIDQ2369008

Franco Barbanera, Fabio Alessi, Mariangiola Dezani-Ciancaglini

Publication date: 28 April 2006

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

Full work available at URL: https://doi.org/10.1016/j.tcs.2006.01.004

zbMATH Keywords

intersection-type assignment systems

Mathematics Subject Classification ID

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

Related Items (8)

A completeness result for a realisability semantics for an intersection type system ⋮ From semantics to types: the case of the imperative \(\lambda\)-calculus ⋮ Calculi, types and applications: essays in honour of M. Coppo, M. Dezani-Ciancaglini and S. Ronchi della Rocca ⋮ A typed lambda calculus with intersection types ⋮ A Filter Model for the λμ-Calculus ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Inhabitation of Low-Rank Intersection Types

Cites Work

• Combinatory logic. With two sections by William Craig.
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Type theories, normal forms, and \(D_{\infty}\)-lambda-models
• Algebras and combinators
• Domain theory in logical form
• Complete restrictions of the intersection type discipline
• An approximation theorem for topological lambda models and the topological incompleteness of lambda calculus
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Full abstraction in the lazy lambda calculus
• Semantical analysis of perpetual strategies in \(\lambda\)-calculus
• Set-theoretical and other elementary models of the \(\lambda\)-calculus
• Intersection types and domain operators
• Behavioural inverse limit \(\lambda\)-models
• Compositional characterisations of \(\lambda\)-terms using intersection types
• Simple Easy Terms
• A filter lambda model and the completeness of type assignment
• Lambda‐Calculus Models and Extensionality
• Functional Characters of Solvable Terms
• Intersection Types and Computational Rules
• A complete characterization of complete intersection-type preorders
• Types for Proofs and Programs
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Intersection types and lambda models