Isomorphism of intersection and union types

DOI10.1017/S0960129515000304zbMath1364.68128arXiv1307.8206MaRDI QIDQ5268999

Ines Margaria, Mario Coppo, Maddalena Zacchi, Mariangiola Dezani-Ciancaglini

Publication date: 14 June 2017

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1307.8206

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Combinatory logic and lambda calculus (03B40)

Related Items

Automorphisms of types in certain type theories and representation of finite groups, Isomorphism of intersection and union types

Cites Work

• Unnamed Item
• Unnamed Item
• Principal type scheme and unification for intersection type discipline
• The semantics of entailment. III
• Characterization of normal forms possessing inverse in the \(\lambda\)- \(\beta\)-\(\eta\)-calculus
• The category of finite sets and Cartesian closed categories
• Second order isomorphic types: A proof theoretic study on second order \(\lambda\)-calculus with surjective pairing and terminal object
• Intersection and union types: Syntax and semantics
• Remarks on isomorphisms in typed lambda calculi with empty and sum types
• Elaborating intersection and union types
• On isomorphisms of intersection types
• Isomorphism of "Functional" Intersection Types
• A short survey of isomorphisms of types
• An ideal model for recursive polymorphic types
• Provable isomorphisms of types
• Isomorphism of intersection and union types