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.

@article{paperbot389,
  title = {Inhabitation for Non-idempotent Intersection Types},
  author = {Antonio Bucciarelli and Delia Kesner and Simona Ronchi Della Rocca},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 14, Issue 3},
  year = {2018},
  doi = {10.23638/lmcs-14(3:7)2018}
}