Full Iso-recursive Types

on YouTube ↗16m

" summary

Presents a new formulation called λFiµ that replaces iso-recursive fold/unfold with general erasable casts so equi-recursive programs encode without runtime coercion and without semantic change. Builds a small-step, call-by-value semantics with push rules for function casts, proves type soundness and behavioral equivalence to equi-recursive systems, and shows erasure gives zero overhead. Development is mechanized in Coq and artifacts and proofs are available for reproduction.

AI-written summary · about

" chapters (11)

1. 0:00Full ISO-recursive types intro
2. 0:43Recursive and ISO/AC types background
3. 3:08ISO vs AC recursive types
4. 4:39Full ISO-recursive types
5. 5:22Encoding AC types in ISO systems
6. 6:47Generalized cast operators solution
7. 8:11Type casting rules and soundness
8. 9:36Cast expressions semantics
9. 12:06Equivalence with AC types
10. 13:11Summary and implications
11. 14:57Q&A