Towards a Logic for Union Types

Abstract

We examine a logical foundation for the intersection and union types assignment system (IUT). The proposed system is Intersection and Union Logic (IUL), an extension of Intersection Logic (IL) with the canonical rules for union. We investigate two different formalisms for IUL, as well as its properties and its relation with minimal intuitionistic logic.