Uniform Proofs of Normalisation and Approximation for Intersection Types

Kentaro Kikuchi
(RIEC, Tohoku University, Japan)

We present intersection type systems in the style of sequent calculus, modifying the systems that Valentini introduced to prove normalisation properties without using the reducibility method. Our systems are more natural than Valentini's ones and equivalent to the usual natural deduction style systems. We prove the characterisation theorems of strong and weak normalisation through the proposed systems, and, moreover, the approximation theorem by means of direct inductive arguments. This provides in a uniform way proofs of the normalisation and approximation theorems via type systems in sequent calculus style.

In Jakob Rehof: Proceedings Seventh Workshop on Intersection Types and Related Systems (ITRS 2014), Vienna, Austria, 18 July 2014, Electronic Proceedings in Theoretical Computer Science 177, pp. 10–23.
Published: 17th March 2015.

ArXived at: http://dx.doi.org/10.4204/EPTCS.177.2 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org