Inhabitation for Non-idempotent Intersection Types
Logic in Computer Science
2023-06-22 v5
Abstract
The inhabitation problem for intersection types in the lambda-calculus is known to be undecidable. We study the problem in the case of non-idempotent intersection, considering several type assignment systems, which characterize the solvable or the strongly normalizing lambda-terms. We prove the decidability of the inhabitation problem for all the systems considered, by providing sound and complete inhabitation algorithms for them.
Keywords
Cite
@article{arxiv.1712.03829,
title = {Inhabitation for Non-idempotent Intersection Types},
author = {Antonio Bucciarelli and Delia Kesner and Simona Ronchi Della Rocca},
journal= {arXiv preprint arXiv:1712.03829},
year = {2023}
}