Tony's Wiki
Search
Search
Dark mode
Light mode
Explorer
Home
❯
10 Projects
❯
Recursive Types
❯
BCD subtyping
Folder: 10-Projects/Recursive-Types/BCD-subtyping
14 items under this folder.
May 16, 2026
A fix to Jsub-mu rule
May 16, 2026
A note on Jsub-mu rule
May 16, 2026
Alternative translate subtyping
May 16, 2026
Compute the Intermediate Type v.2
May 16, 2026
Compute the Intermediate Type
May 16, 2026
Direct Splitting on Source Types
May 16, 2026
Distributivity Subtyping
May 16, 2026
Full Splitting
May 16, 2026
Inductively find the middle type (cont.)
idea
May 16, 2026
Inductively find the middle type
May 16, 2026
Intermediate Type from Left
May 16, 2026
One algorithm on the source type to try
May 16, 2026
Some careful thoughts on splitting RHS
todo
Sep 16, 2025
Formalization progress of controlled subtyping in Coq
type/moc
topic/distributivity
context/hkuplg
status/ongoing