On the Theory of Structural Subtyping
We show that the first-order theory of structural subtyping of non-recursive types is decidable. Let Sigma 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 primitiv...
| Main Authors: | , |
|---|---|
| Published: |
2023
|
| Online Access: | https://hdl.handle.net/1721.1/149974 |