Complete restrictions of the intersection type discipline

DOI10.1016/0304-3975(92)90297-SzbMath0762.03006MaRDI QIDQ1193654

Steffen van Bakel

Publication date: 27 September 1992

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

zbMATH Keywords

type assignment systemfilter lambda modelinference semantics

Mathematics Subject Classification ID

Theory of programming languages (68N15) General topics in the theory of software (68N01) Combinatory logic and lambda calculus (03B40)

Related Items (41)

Intersection types and lambda models ⋮ A classification of intersection type systems ⋮ Intersection types for explicit substitutions ⋮ (Head-)normalization of typeable rewrite systems ⋮ Intersection type assignment systems ⋮ Strong normalization for non-structural subtyping via saturated sets ⋮ Normalization results for typeable rewrite systems ⋮ A resource aware semantics for a focused intuitionistic calculus ⋮ Strong normalization and typability with intersection types ⋮ Unnamed Item ⋮ Semantic types and approximation for Featherweight Java ⋮ Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\) ⋮ On Isomorphisms of Intersection Types ⋮ The heart of intersection type assignment: Normalisation proofs revisited ⋮ Behavioural inverse limit \(\lambda\)-models ⋮ Modularity of termination and confluence in combinations of rewrite systems with λω ⋮ Filter models for conjunctive-disjunctive \(\lambda\)-calculi ⋮ Strong normalization through intersection types and memory ⋮ Approximation and normalization results for typeable term rewriting systems ⋮ Functional Type Assignment for Featherweight Java ⋮ A domain model characterising strong normalisation ⋮ Types with intersection: An introduction ⋮ Functional programs as compressed data ⋮ Logical equivalence for subtyping object and recursive types ⋮ A \(\kappa\)-denotational semantics for map theory in ZFC+SI ⋮ Unnamed Item ⋮ Cut-elimination in the strict intersection type assignment system is strongly normalizing ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Strong Normalizability as a Finiteness Structure via the Taylor Expansion of $$\lambda $$ λ -terms ⋮ Reasoning About Call-by-need by Means of Types ⋮ Infinite \(\lambda\)-calculus and types ⋮ Intersection Types for the Resource Control Lambda Calculi ⋮ Strongly Normalising Cut-Elimination with Strict Intersection Types ⋮ Intersection Typed λ-calculus ⋮ Compositional characterisations of \(\lambda\)-terms using intersection types ⋮ Normalization without reducibility ⋮ From computation to foundations via functions and application: The \(\lambda\)-calculus and its webbed models ⋮ Pre-grammars and inhabitation for a subset of rank 2 intersection types ⋮ Normalization, approximation, and semantics for combinator systems ⋮ Intersection and singleton type assignment characterizing finite Böhm-trees

Uses Software

• ML
• Miranda

Cites Work

• Principal type schemes for an extended type theory
• The lambda calculus. Its syntax and semantics. Rev. ed.
• A characterization of F-complete type assignments
• Type theories, normal forms, and \(D_{\infty}\)-lambda-models
• Principal type scheme and unification for intersection type discipline
• Polymorphic type inference and containment
• An extension of basic functionality theory for \(\lambda\)-calculus
• A theory of type polymorphism in programming
• The completeness theorem for typing lambda-terms
• A filter lambda model and the completeness of type assignment
• Functional Characters of Solvable Terms
• The Category-Theoretic Solution of Recursive Domain Equations
• Functionality in Combinatory Logic
• The Principal Type-Scheme of an Object in Combinatory Logic
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Complete restrictions of the intersection type discipline