Intersection Types with Subtyping by Means of Cut Elimination

Issue title: Intersection Types and Related Systems (ITRS)

Article type: Research Article

Authors: Laurent, Olivier

Affiliations: Laboratoire de l'Informatique du Parallélisme, Université de Lyon, ENS Lyon, CNRS, UCBL, INRIA, France. [email protected]

Note: [] Address for correspondence: Olivier Laurent — Laboratoire de l'Informatique du Parallélisme — UMR 5668, Université de Lyon, ENS Lyon, CNRS, UCBL, INRIA — 46, allée d'Italie — 69364 Lyon cedex 07 — France

Abstract: We give a purely syntactic proof (from scratch) of the subject equality property of the BCD intersection type system through a reformulation of the subtyping relation having a “cut-elimination” property.

DOI: 10.3233/FI-2012-776

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