Equirecursive types consider a recursive type to be equal to its unrolling and have no explicit term-level coercions to change a term's type from the former to the latter or vice versa. This equality makes deciding type equality and subtyping more difficult than the other approach-isorecursive types, in which the types are not equal, but isomorphic, witnessed by explicit term-level coercions. Previous work has built intuition, rules, and polynomial-time decision procedures for equirecursive types for first-order type systems. Some work has been done for type systems with parametric polymorphism, but that work is incomplete (see below). This chapter will give an intuitive theory of equirecursive types for second-order type systems, sound and complete rules, and a decision procedure for subtyping. © 2012 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Glew, N. (2012). Subtyping for F-bounded quantifiers and equirecursive types. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 7230 LNCS, 66–82. https://doi.org/10.1007/978-3-642-29485-3_6
Mendeley helps you to discover research relevant for your work.