The Inhabitation Problem for Non-idempotent Intersection Types - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2014

The Inhabitation Problem for Non-idempotent Intersection Types

Résumé

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
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

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

Licence

Paternité

Identifiants

Citer

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⟩
101 Consultations
111 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More