Completeness and Soundness Results for 𝒳 with Intersection and Union Types

Issue title: Intersection Types and Related Systems (ITRS)

Article type: Research Article

Authors: van Bakel, Steffen

Affiliations: Department of Computing, Imperial College London, 180 Queen's Gate, London SW7 2BZ, UK. [email protected]

Note: [] Address for correspondence: Department of Computing, Imperial College London, 180 Queen's Gate, London SW7 2BZ, UK

Abstract: With the eye on defining a type-based semantics, this paper defines intersection and union type assignment for the sequent calculus 𝒳, a substitution-free language that enjoys the Curry-Howard correspondence with respect to the implicative fragment of Gentzen's sequent calculus for classical logic. We investigate the minimal requirements for such a system to be complete (i.e. closed under redex expansion), and show that the non-logical nature of both intersection and union types disturbs the soundness (i.e. closed uder reduction) properties. This implies that this notion of intersection-union type assignment needs to be restricted to satisfy soundness as well, making it unsuitable to define a semantics. We will look at two (confluent) notions of reduction, called Call-by-Name and Call-by-Value, and prove soundness results for those.

Keywords: Classical Logic, Sequent Calculus, intersection types, union types

DOI: 10.3233/FI-2012-770

Journal: Fundamenta Informaticae, vol. 121, no. 1-4, pp. 1-41, 2012