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...
| Główni autorzy: | , |
|---|---|
| Wydane: |
2023
|
| Dostęp online: | https://hdl.handle.net/1721.1/149974 |