The Inhabitation Problem for Non-idempotent Intersection Types - Theoretical Computer Science
Conference Papers Year : 2014

The Inhabitation Problem for Non-idempotent Intersection Types

Abstract

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.
Fichier principal
Vignette du fichier
978-3-662-44602-7_26_Chapter.pdf (347.63 Ko) Télécharger le fichier
Origin Files produced by the author(s)
Loading...

Dates and versions

hal-01402082 , version 1 (24-11-2016)

Licence

Identifiers

Cite

Antonio Bucciarelli, Delia Kesner, Simona Ronchi Della Rocca. The Inhabitation Problem for Non-idempotent Intersection Types. 8th IFIP International Conference on Theoretical Computer Science (TCS), Sep 2014, Rome, Italy. pp.341-354, ⟨10.1007/978-3-662-44602-7_26⟩. ⟨hal-01402082⟩
123 View
126 Download

Altmetric

Share

More