Loading...
Please wait, while we are loading the content...
Similar Documents
Subtyping Recursive Types in Kernel Fun , preliminary draftDario Colazzo
| Content Provider | Semantic Scholar |
|---|---|
| Author | Colazzo, Dario Ghelli, Giorgio |
| Copyright Year | 1999 |
| Abstract | The problem of deening and checking a subtype relation between recursive types was studied in AC93] for a rst order type system, but for second order systems, which combine subtyping and parametric polymorphism, only negative results are known Ghe93b]. This paper studies the problem of subtype checking for recursive types in system kernel Fun, a typed-calculus with subtyping and bounded second order polymorphism. Along the lines of AC93], we study the deenition of a subtype relation over kernel Fun recursive types, and then we present a subtyping algorithm which is sound and complete with respect to this relation. We show that the natural extension of the techniques introduced in AC93] to compare rst order recursive types gives a non complete algorithm. We prove the completeness and correctness of a diierent algorithm, which also admits an eecient implementation. |
| File Format | PDF HTM / HTML |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
