Strong Normalization in the π-calculus with Intersection and Union Types

Issue title: Intersection Types and Related Systems (ITRS)

Article type: Research Article

Authors: Piccolo, Mauro

Affiliations: Dipartimento di Informatica, Università degli Studi di Torino, Preuve Programmes et Systèmes , Paris VII, France. piccolo@di.unito.it

Note: [] Address for correspondence: Dipartimento di Informatica, Università degli Studi di Torino

Abstract: In this work we present an extension of the linear typing discipline for π-calculus, introduced by Yoshida, Honda and Berger, with Intersection and Union Types. We show that we are able to define a typing system for the π-calculus, which guarantees that every well-typed term is strongly normalizing. This typing system is an extension of that presented in [30] since it is able to type more terms than that presented there.

DOI: 10.3233/FI-2012-777

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