First-Order Theory of Subtyping Constraints

Zhendong Su 1 Alex Aiken 1 Joachim Niehren 2 Tim Priesnitz 2 Ralf Treinen 3
1 Department of Mathematics [Berkeley]
2 Programming Systems Lab [Saarland]
3 LRI - Laboratoire de Recherche en Informatique
Abstract : We investigate the first-order theory of subtyping constraints. We show that the first-order theory of non-structural subtyping is undecidable, and we show that in the case where all constructors are either unary or nullary, the first-order theory is decidable for both structural and non-structural subtyping. The decidability results are shown by reduction to a decision problem on tree automata. This work is a step towards resolving long-standing open problems of the decidability of entailment for non-structural subtyping.
Type de document :
Communication dans un congrès
The 29th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2002, Portland, United States. ACM Press, pp.203-216, 2002
Liste complète des métadonnées

Littérature citée [42 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/inria-00536828
Contributeur : Joachim Niehren <>
Soumis le : mardi 16 novembre 2010 - 23:13:03
Dernière modification le : mardi 24 avril 2018 - 13:39:07
Document(s) archivé(s) le : jeudi 17 février 2011 - 03:18:24

Fichier

fot02.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00536828, version 1

Collections

UMR8623 | INRIA

Citation

Zhendong Su, Alex Aiken, Joachim Niehren, Tim Priesnitz, Ralf Treinen. First-Order Theory of Subtyping Constraints. The 29th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2002, Portland, United States. ACM Press, pp.203-216, 2002. 〈inria-00536828〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

125

Téléchargements de fichiers

105

Contact


archive-ouverte@inria.fr