Uniform Proofs of Normalisation and Approximation for Intersection Types

TL;DR

This paper introduces sequent calculus style intersection type systems that provide uniform proofs of normalization and approximation theorems, offering a more natural alternative to Valentini's systems without reducibility methods.

Contribution

It develops more natural sequent calculus style intersection type systems that are equivalent to natural deduction systems and proves normalization and approximation theorems using direct inductive methods.

Findings

Proves strong and weak normalization characterizations.

Establishes the approximation theorem via inductive arguments.

Provides a uniform proof framework for normalization and approximation.

Abstract

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.