A Calculus with Recursive Types, Record Concatenation and Subtyping
summary
Paper presents a new calculus that combines iso-recursive types with disjoint intersection types and a merge operator that generalizes symmetric record concatenation. It adopts nominal unfolding rules for iso-recursive subtyping, gives a decidable subtyping algorithm, and defines disjointness by checking recursive bodies so merges reject overlapping fields but allow identical terms. Proofs include type soundness and soundness and completeness of disjointness, and all results are fully Coq mechanized.
AI-written summary · about
chapters (13)
- 0:00Start
- 0:22Record calculi
- 1:33An example
- 4:05Disjoint intersection types
- 4:48Adding iso-recursive types to λ
- 6:53Iso-recursive subtyping
- 8:33Disjointness restriction
- 9:43Top-like types and disjointness
- 11:32Disjointness for recursive types
- 12:37Disjointness rules
- 13:14Completeness of disjointness
- 17:08Summary
- 19:01Lower common supertype