2015/03/17 by Kentaro Kikuchi
Computer Science · #cs.LO #cs.PL
paper · pdf · doi:10.4204/eptcs.177.2
published as EPTCS 177, 2015, pp. 10-23 · In Proceedings ITRS 2014, arXiv:1503.04377
arxiv created 2015/03/17 · arxiv updated 2015/03/18
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.