Recursive Subtyping for All
summary
Presents F_{≤}^{μ}, a kernel F_{≤} extension that adds iso-recursive types plus nominal unfolding rules and new structural folding/unfolding rules, and proves type soundness, subtyping transitivity, and decidability, all formalized in Coq. Shows a sound-and-complete algorithmic subtyping procedure, proves conservativity over kernel F_{≤}, and extends to F_{≤≥}^{μ} with lower bounds. Demonstrates encoding of algebraic datatypes and polymorphic constructors and explains how the size-based measure yields a terminating decision procedure.
AI-written summary · about
chapters (18)
- 0:00Intro
- 1:24F with recursive types
- 3:38Bounded quantification
- 4:19Conservativity
- 5:50Comparing different work
- 8:27The calculus in this work
- 9:35Nominal unfolding rule
- 11:39Type soundness
- 12:36Decidability - a measure approach
- 14:06Kernel F is conservative over kernel F
- 14:45Application: Encodings of algebraic datatypes
- 17:07Subtyping between datatypes
- 17:50Code Reuse
- 18:21Challenge: polymorphic constructors
- 19:37Precise typing
- 20:53Desugar function in Kernel F
- 21:12Summary
- 24:49Structural folding/unfolding rules