Non-idempotent intersection types in logical form
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.
Cite
@article{arxiv.1911.01899,
title = {Non-idempotent intersection types in logical form},
author = {Thomas Ehrhard},
journal= {arXiv preprint arXiv:1911.01899},
year = {2019}
}