| Title: |
First-Order Theory of Subtyping Constraints |
| Authors: |
Su, Zhendong; Aiken, Alex; Niehren, Joachim; Priesnitz, Tim; Treinen, Ralf |
| Contributors: |
Department of Mathematics Berkeley; University of California Berkeley (UC Berkeley); University of California (UC)-University of California (UC); Programming Systems Lab Saarland; Universität des Saarlandes Saarbrücken = Saarland University Saarbrücken; Laboratoire de Recherche en Informatique (LRI); Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS) |
| Source: |
The 29th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages ; https://inria.hal.science/inria-00536828 ; The 29th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2002, Portland, United States. pp.203-216 |
| Publisher Information: |
CCSD; ACM Press |
| Publication Year: |
2002 |
| Subject Terms: |
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] |
| Subject Geographic: |
Portland; United States |
| Description: |
International audience ; 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. |
| Document Type: |
conference object |
| Language: |
English |
| Availability: |
https://inria.hal.science/inria-00536828; https://inria.hal.science/inria-00536828v1/document; https://inria.hal.science/inria-00536828v1/file/fot02.pdf |
| Rights: |
info:eu-repo/semantics/OpenAccess |
| Accession Number: |
edsbas.8F26F442 |
| Database: |
BASE |