The inhabitation problem for intersection types is known to be undecidable. We study the problem in the case of non-idempotent intersection, and we prove decidability through a sound and complete algorithm. We then consider the inhabitation problem for an extended system typing the λ-calculus with pairs, and we prove the decidability in this case too. The extended system is interesting in its own, since it allows to characterize solvable terms in the λ-calculus with pairs. © 2014 IFIP International Federation for Information Processing.
CITATION STYLE
Bucciarelli, A., Kesner, D., & Ronchi Della Rocca, S. (2014). The inhabitation problem for non-idempotent intersection types. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8705 LNCS, pp. 341–354). Springer Verlag. https://doi.org/10.1007/978-3-662-44602-7_26
Mendeley helps you to discover research relevant for your work.