A binary modal logic for the intersection types of lambda-calculus.

DOI10.1016/S0890-5401(03)00089-0zbMath1035.03006MaRDI QIDQ1427854

Silvio Valentini, Matteo Viale

Publication date: 14 March 2004

Published in: Information and Computation (Search for Journal in Brave)

zbMATH Keywords

modal logicsemanticsintersection typeslambda-calculussub-typing relation

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Functional programming and lambda calculus (68N18) Cut-elimination and normal-form theorems (03F05) Combinatory logic and lambda calculus (03B40)

Related Items (1)

Logic of subtyping

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Coppo-Dezani types do not correspond to propositional logic
• The lambda calculus. Its syntax and semantics. Rev. ed.
• The semantics of entailment. III
• The ``relevance of intersection and union types
• An elementary proof of strong normalization for intersection types
• Intersection and union types: Syntax and semantics
• A filter lambda model and the completeness of type assignment
• Intersection Types as Logical Formulae
• A general method for proving the normalization theorem for first and second order typed λ-calculi
• Proof theory

This page was built for publication: A binary modal logic for the intersection types of lambda-calculus.