[ list |
abstracts |
bib |
http ]

## On the Theory of Structural Subtyping

paper pdf
paper ps
### Abstract

We show that the first-order theory of structural subtyping
of non-recursive types is decidable. Let Σ be a
language consisting of function symbols (representing type
constructors) and *C* a decidable structure in the
relational language *L* containing a binary relation
<=. *C* represents primitive types; <= represents a
subtype ordering. We introduce the notion of
Σ-term-power of *C*, which generalizes the structure
arising in structural subtyping. The domain of the
Σ-term-power of *C* is the set of Σ-terms over
the set of elements of *C*. We show that the decidability of
the first-order theory of *C* implies the decidability of
the first-order theory of the Σ-term-power of
*C*. Our decision procedure makes use of quantifier
elimination for term algebras and Feferman-Vaught
theorem. Our result implies the decidability of the
first-order theory of structural subtyping of non-recursive
types.

### Citation

Viktor Kuncak and Martin Rinard.
On the theory of structural subtyping.
Technical Report 879, MIT LCS, 2003.
Technical report version of
[20].### BibTex Entry

@TECHREPORT{KuncakRinard03TheoryStructuralSubtyping,
author = {Viktor Kuncak and Martin Rinard},
title = {On the Theory of Structural Subtyping},
institution = {MIT LCS},
number = 879,
year = 2003,
url = {http://arxiv.org/abs/cs.LO/0408015},
note = {Technical report version of
\cite{KuncakRinard03StructuralSubtypingNonRecursiveTypesDecidable}},
localurl = {http://lara.epfl.ch/~kuncak/papers/KuncakRinard03TheoryStructuralSubtyping.pdf}
}

[ list |
abstracts |
bib |
http ]