Escape with Your Self: Sound and Expressive Bidirectional Typing with Avoidance for Reachability Types
Songlin Jia, Guannan Wei, Siyuan He, Yuyan Bao, Tiark Rompf

TL;DR
This paper introduces a novel sound and decidable bidirectional type checking algorithm for reachability types that effectively handles avoidance through subtyping, enabling the verification of complex escaping data types.
Contribution
It presents the first algorithmic approach for reachability types with formal soundness, using subtyping-based avoidance and mechanized in Lean.
Findings
Proposes a refined declarative reachability type system with self-aware subtyping.
Develops a bidirectional type system that infers qualifiers via unification.
Successfully type-checks complex escaping Church-encoded data types.
Abstract
Algorithmic type checking and inference of reachability types present a particular challenge with regards to subtyping. As a restricted form of dependent types, reachability types are subject to the avoidance problem: a variable mentioned in types becomes ill-scoped when its defining scope ends. Prior works thus introduce self-references, akin to this pointers in OO languages, to replace the escaping variable, so that an escaping object's this pointer can serve as the new logical owner of any captured resources. Nevertheless, conversions involving self-references require reasoning about function qualifiers. As prior work isolates subtyping judgements from associated qualifiers, their system requires manually-inserted term-level coercions (i.e., -expansion) to support escaping values. This, of course, is highly unsatisfactory for algorithmic avoidance. In this work, we propose…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsMultimedia Communication and Technology · Video Analysis and Summarization · Natural Language Processing Techniques
