Revisiting Iso-Recursive Subtyping

on YouTube ↗24m

" summary

Presents a new declarative finite unfolding specification that says two mu-types are subtypes iff all same-depth finite unfoldings are subtypes, proves the classic Amber rules sound relative to it, and derives a double unfolding algorithm (and an equivalent nominal unfolding) that is sound, complete and decidable. All metatheory — equivalence proofs, reflexivity derivation, easier transitivity proofs and extensions to polymorphism — is mechanized in Coq, targeting unrestricted iso-recursive types.

AI-written summary · about

" chapters (19)

1. 0:00Introduction
2. 0:23Recursive types background
3. 3:16Recursive subtyping history
4. 6:25Issues with ISO Amber rules
5. 8:34Intuitions behind subtyping
6. 9:40Unfolding rule specification
7. 12:29Comparison with active subtyping
8. 12:50Advantages of new spec
9. 13:11Double unfolding rule
10. 14:36Nominal unfolding rule
11. 15:39Positive subtyping rule
12. 16:00Equivalence and extensibility
13. 16:20Follow-up works
14. 17:11Acknowledgments
15. 18:03Q&A
16. 18:32Generic recursive types
17. 20:42Polymorphic systems
18. 21:24Mutually recursive types
19. 22:26Closing remarks