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.
Type de document :
Communication dans un congrès
Josep Diaz; Ivan Lanese; Davide Sangiorgi. 8th IFIP International Conference on Theoretical Computer Science (TCS), Sep 2014, Rome, Italy. Springer, Lecture Notes in Computer Science, LNCS-8705, pp.341-354, 2014, Theoretical Computer Science. 〈10.1007/978-3-662-44602-7_26〉
Liste complète des métadonnées

Littérature citée [24 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01402082
Contributeur : Hal Ifip <>
Soumis le : jeudi 24 novembre 2016 - 11:09:54
Dernière modification le : jeudi 15 novembre 2018 - 20:27:00
Document(s) archivé(s) le : mardi 21 mars 2017 - 05:37:37

Fichier

978-3-662-44602-7_26_Chapter.p...
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Antonio Bucciarelli, Delia Kesner, Simona Ronchi Della Rocca. The Inhabitation Problem for Non-idempotent Intersection Types. Josep Diaz; Ivan Lanese; Davide Sangiorgi. 8th IFIP International Conference on Theoretical Computer Science (TCS), Sep 2014, Rome, Italy. Springer, Lecture Notes in Computer Science, LNCS-8705, pp.341-354, 2014, Theoretical Computer Science. 〈10.1007/978-3-662-44602-7_26〉. 〈hal-01402082〉

Partager

Métriques

Consultations de la notice

110

Téléchargements de fichiers

35