@TechReport{Niehren_Priesnitz:1999,
      AUTHOR = {Niehren, Joachim and Priesnitz, Tim},
      TITLE = {Characterizing Subtype Entailment in Automata Theory},
      YEAR = {1999},
      ADDRESS = {Saarbrücken},
      TYPE = {Technical Report},
      INSTITUTION = {Universität des Saarlandes},
      URL = {http://www.ps.uni-sb.de/Papers/abstracts/pauto.html ftp://ftp.ps.uni-sb.de/pub/papers/ProgrammingSysLab/pauto.ps.gz},
      ABSTRACT = {Subtype entailment is the entailment problem of subtype constraints for some type language. Understanding the algorithmic properties of subtype entailment is relevant to several subtype inference systems. For simple types, subtype entailment is coNP complete; when extended with recursive types it becomes PSPACE complete. Adding the least and greatest type renders subtyping non-structural. Whether non-structural subtype entailment is decidable is a prominent open problem. We characterize subtype entailment in automata theory. This yields a uniform proof method by which all known complexity results on subtype entailment in the literature can be derived. The main contribution of the paper is an equivalent characterization of non-structural subtype entailment in automata theory (by so called P-automata). On the one hand side, our characterization implies that several variants of non-structural subtype entailment are polynomial time equivalent (with or without contravariant function types or recursive types). This robustness result is new and nontrivial. On the other hand side, we believe that our characterization contributes an important and necessary step towards answering the open question on decidability of non-structural subtype entailment.},
      ANNOTE = {COLIURL : Niehren:1999:CSE.pdf Niehren:1999:CSE.ps}
}