Isomorphism of intersection and union types

DOI10.1017/S0960129515000304MaRDI QIDQ5268999zbMATH OpenFDO

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

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

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

Abstract: This paper investigates type isomorphism in a lambda-calculus with intersection and union types. It is known that in lambda-calculus, the isomorphism between two types is realised by a pair of terms inverse one each other. Notably, invertible terms are linear terms of a particular shape, called finite hereditary permutators. Typing properties of finite hereditary permutators are then studied in a relevant type inference system with intersection and union types for linear terms. In particular, an isomorphism preserving reduction between types is defined. Type reduction is confluent and terminating, and induces a notion of normal form of types. The properties of normal types are a crucial step toward the complete characterisation of type isomorphism. The main results of this paper are, on one hand, the fact that two types with the same normal form are isomorphic, on the other hand, the characterisation of the isomorphism between types in normal form, modulo isomorphism of arrow types.

Recommendations

• Toward isomorphism of intersection and union types
• On isomorphisms of intersection types
• On Isomorphisms of Intersection Types
• Isomorphism of "Functional" Intersection Types
• Intersection and union types: Syntax and semantics

Cites work

• A short survey of isomorphisms of types
• An ideal model for recursive polymorphic types
• Characterization of normal forms possessing inverse in the - --calculus
• Elaborating intersection and union types
• scientific article; zbMATH DE number 517016 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• Intersection and union types: Syntax and semantics
• Isomorphism of "Functional" Intersection Types
• Isomorphism of intersection and union types
• On isomorphisms of intersection types
• Principal type scheme and unification for intersection type discipline
• Provable isomorphisms of types
• Remarks on isomorphisms in typed lambda calculi with empty and sum types
• Second order isomorphic types: A proof theoretic study on second order \(\lambda\)-calculus with surjective pairing and terminal object
• The category of finite sets and Cartesian closed categories
• The semantics of entailment. III

Cited in

(7)

• On isomorphisms of intersection types
• Isomorphism of "Functional" Intersection Types
• Automorphisms of types in certain type theories and representation of finite groups
• On Isomorphisms of Intersection Types
• Toward isomorphism of intersection and union types
• Intersection and union types
• Isomorphism of intersection and union types

This page was built for publication: Isomorphism of intersection and union types

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5268999)