On the Semantic Expressiveness of Recursive Types

on YouTube ↗23m

" summary

Paper proves iso-recursive types, equirecursive types, and a term-level fix are semantically equivalent by constructing three fully abstract compilers (including the identity compiler that erases fold/unfold) and proving preservation/reflection of contextual equivalence. Proofs use step-indexed, asymmetric logical relations plus an approximate backtranslation that indexes backtranslation types by n and inserts an inject conversion to make types check. Results cover interactions over recursively-typed interfaces, the constructions complete and the theorems carry.

AI-written summary · about

" chapters (10)

1. 0:00On the Semantic Expressiveness
2. 2:06Talk Outline
3. 2:26Recursive Types (in STLC)
4. 3:34Iso-recursive Types
5. 5:06Coinductive Type Equality
6. 11:31FAC for Language Expressiveness
7. 14:53Asymmetric Logical Approximation
8. 15:33The Need to Approximate
9. 17:07Approximate Backtranslation Type
10. 18:57Backtranslation Example and Relation