Cut-elimination in the strict intersection type assignment system is strongly normalizing

DOI10.1305/ndjfl/1094155278zbMath1095.03058OpenAlexW2093271301MaRDI QIDQ558418

Steffen van Bakel

Publication date: 6 July 2005

Published in: Notre Dame Journal of Formal Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1305/ndjfl/1094155278

zbMATH Keywords

cut-eliminationterminationlambda calculusintersection typesstrong normalizationapproximation theorem

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Cut-elimination and normal-form theorems (03F05) Combinatory logic and lambda calculus (03B40)

Related Items (7)

Semantic types and approximation for Featherweight Java ⋮ Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\) ⋮ The heart of intersection type assignment: Normalisation proofs revisited ⋮ A typed lambda calculus with intersection types ⋮ An irregular filter model ⋮ Approximation Semantics and Expressive Predicate Assignment for Object-Oriented Programming ⋮ Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Combinatory logic. With two sections by William Craig.
• 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
• An extension of basic functionality theory for \(\lambda\)-calculus
• Complete restrictions of the intersection type discipline
• Intersection type assignment systems
• Normalization results for typeable rewrite systems
• The semantics of entailment omega
• Normalization, approximation, and semantics for combinator systems
• Strong normalization and typability with intersection types
• Approximation Theorems for Intersection Type Systems
• Strongly Normalising Cut-Elimination with Strict Intersection Types
• A filter lambda model and the completeness of type assignment
• The Relation between Computational and Denotational Properties for Scott’s ${\text{D}}_\infty $-Models of the Lambda-Calculus
• Functionality in Combinatory Logic
• Intensional interpretations of functionals of finite type I
• Intersection types for \(\lambda\)-trees

This page was built for publication: Cut-elimination in the strict intersection type assignment system is strongly normalizing