Non-idempotent intersection types in logical form

TL;DR

This paper presents a logical framework for non-idempotent intersection types, enabling their analysis within a formal logical system by using indexed formulas, which enhances understanding of lambda calculus and functional programs.

Contribution

It introduces a logical form for non-idempotent intersection types using indexed formulas, bridging the gap between type systems and logical frameworks.

Findings

Non-idempotent intersection types can be represented in a logical system.

Indexed formulas allow for a logical interpretation of non-idempotent types.

The approach connects type analysis with linear logic principles.

Abstract

Intersection types are an essential tool in the analysis of operational and denotational properties of lambda-terms and functional programs. Among them, non-idempotent intersection types provide precise quantitative information about the evaluation of terms and programs. However, unlike simple or second-order types, intersection types cannot be considered as a logical system because the application rule (or the intersection rule, depending on the presentation of the system) involves a condition expressing that the proofs of premises satisfy a very strong uniformity condition: the underlying lambda-terms must be the same. Using earlier work introducing an indexed version of Linear Logic, we show that non-idempotent typing can be given a logical form in a system where formulas represent hereditarily indexed families of intersection types.