Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\)

DOI10.1016/J.APAL.2010.04.010zbMath1225.03015OpenAlexW2068044092MaRDI QIDQ636376

Steffen van Bakel

Publication date: 26 August 2011

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.apal.2010.04.010

zbMATH Keywords

completenesssequent calculussoundnessclassical logicintersection and union types

Mathematics Subject Classification ID

Logic in computer science (03B70) Combinatory logic and lambda calculus (03B40)

Related Items (5)

Semantic types and approximation for Featherweight Java ⋮ A Filter Model for the λμ-Calculus ⋮ Approximation Semantics and Expressive Predicate Assignment for Object-Oriented Programming ⋮ Functional Type Assignment for Featherweight Java ⋮ Unnamed Item

Uses Software

• ML

Cites Work

• 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
• Coppo-Dezani types do not correspond to propositional logic
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage
• A syntactic theory of sequential control
• Complete restrictions of the intersection type discipline
• Intersection type assignment systems
• Untersuchungen über das logische Schliessen. I
• Normalization, approximation, and semantics for combinator systems
• Intersection and union types: Syntax and semantics
• Strict intersection types for the Lambda Calculus
• Intersection types and computational effects
• The duality of computation
• A new type assignment for λ-terms
• A filter lambda model and the completeness of type assignment
• Computation with classical sequents
• Call-by-value is dual to call-by-name
• Strong Normalization of the Dual Classical Sequent Calculus
• Theoretical Computer Science
• Programming Languages and Systems
• Completeness of intersection and union type assignment systems for call-by-value \(\lambda\)-models

This page was built for publication: Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\)