Intersection type assignment systems

DOI10.1016/0304-3975(95)00073-6zbMath0871.68031OpenAlexW2158244462MaRDI QIDQ1350344

Steffen van Bakel

Publication date: 27 February 1997

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

Full work available at URL: https://doi.org/10.1016/0304-3975(95)00073-6

zbMATH Keywords

lambda calculus

Mathematics Subject Classification ID

Theory of programming languages (68N15) General topics in the theory of software (68N01)

Related Items (22)

On sets of terms having a given intersection type ⋮ Intersection types for explicit substitutions ⋮ Nominal essential intersection types ⋮ Normalization results for typeable rewrite systems ⋮ Semantic types and approximation for Featherweight Java ⋮ Type Inference for Rank 2 Gradual Intersection Types ⋮ Non-Deterministic Functions as Non-Deterministic Processes (Extended Version) ⋮ From semantics to types: the case of the imperative \(\lambda\)-calculus ⋮ Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\) ⋮ Linearity and iterator types for Gödel's system \(\mathcal T\) ⋮ On strong normalization and type inference in the intersection type discipline ⋮ The heart of intersection type assignment: Normalisation proofs revisited ⋮ A typed lambda calculus with intersection types ⋮ Approximation Semantics and Expressive Predicate Assignment for Object-Oriented Programming ⋮ Functional Type Assignment for Featherweight Java ⋮ Functional programs as compressed data ⋮ Logical equivalence for subtyping object and recursive types ⋮ Unnamed Item ⋮ Cut-elimination in the strict intersection type assignment system is strongly normalizing ⋮ Unnamed Item ⋮ Strongly Normalising Cut-Elimination with Strict Intersection Types ⋮ Normalization, approximation, and semantics for combinator systems

Uses Software

• ML
• Forsythe

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Principal type schemes for an extended type theory
• The lambda calculus. Its syntax and semantics. Rev. ed.
• A characterization of F-complete type assignments
• The system \({\mathcal F}\) of variable types, fifteen years later
• Type theories, normal forms, and \(D_{\infty}\)-lambda-models
• Polymorphic type inference and containment
• An extension of basic functionality theory for \(\lambda\)-calculus
• Algebras and combinators
• Filter models with polymorphic types
• Complete restrictions of the intersection type discipline
• A theory of type polymorphism in programming
• The completeness theorem for typing lambda-terms
• A filter lambda model and the completeness of type assignment
• Lambda‐Calculus Models and Extensionality
• Functional Characters of Solvable Terms
• The Relation between Computational and Denotational Properties for Scott’s ${\text{D}}_\infty $-Models of the Lambda-Calculus
• Principal Type Schemes for the Strict Type Assignment System
• Functionality in Combinatory Logic
• Principal Typing in a ∀Λ-Discipline
• Intensional interpretations of functionals of finite type I
• The Principal Type-Scheme of an Object in Combinatory Logic

This page was built for publication: Intersection type assignment systems