Reachability Types

Overview

The $λ^*$-calculus [1] and its variations, gradually increasing in complexity.

• Base -- Type soundness proof in Coq of the simplest system, lacking recursion, function self qualifiers, and a bottom qualifier. Mutable references are restricted to values of a base type. Functions and arguments may not overlap. Qualifiers are represented by a set data type.
• Bot -- Extends the base version with a bottom qualifier for untracked values, which, e.g., enables polymorphic mutable references.
• Overlap -- Extends the base version to support overlap between functions and arguments at call sites. Term typing "eagerly" assigns transitively closed qualifiers.
• Rec -- Adds recursive lambda abstractions to the overlap system.
• Lazy -- "Lazy" version of the overlap system, where term typing assigns minimal qualifiers and uses transitive closures "lazily" on demand.
• Lazy_Rec -- Adds recursive lambda abstractions to the lazy overlap system.
• Self -- Adds function self qualifiers, permitting escaping closures.
• Full -- Adds the bottom qualifier based on Self.

graph TD
    subgraph oopsla[OOPSLA'21]
      Base
      Bot
      Overlap
      Rec
      Lazy
      Lazy_Rec
      Self
      Full
    end
    Base[<a title='Qualifiers are sets, functions and arguments are separate.'>Base</a>] --> Bot[<a title='Adds untracked qualifiers'>Bot</a>]
    Base --> Overlap[<a title='Permit overlap between functions and arguments.'>Overlap</a>]
    Overlap-->Rec[<a title='Adds recursive lambda abstractions.'>Rec</a>]
    Overlap-->Lazy[<a title='Assign minimal qualifiers, transitive closure on demand.'>Lazy</a>]
    Rec-->Lazy_Rec[<a title='Merge Lazy and Rec'>Lazy Rec</a>]
    Lazy-->Lazy_Rec
    Lazy_Rec-->Self[<a title='Adds function self qualifiers.'>Self</a>]
    Bot-->Full[<a title='Merge Bot and Self'>Full</a>]
    Self-->Full

Loading

References

[1] Reachability Types: Tracking Aliasing and Separation in Higher-order Functional Programs (OOPSLA 2021)
by Yuyan Bao, Guannan Wei, Oliver Bračevac, Luke Jiang, Qiyang He, and Tiark Rompf (pdf).