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.

The following variants use the new propositional set implementation:

• Overlap -- Overlap version with propositional implementation for sets.

For more information regarding the propositional set implementation, please check out Overlap Prop Set

graph TD
    subgraph oopsla[Variant Maps]
      Base
      Bot
      Overlap
      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>]
    Overlap<-->Overlap*[<a title='Overlap version with propositional set implementation'>Overlap*</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

Note: We are shifting to a propositional set implementation on some versions for more powerful automation. The * versions in the diagram above indicate versions with propositional set implementation.

The initial mechanizations reuse some libraries by the UPenn PL Club that complement the FSet library shipping with Coq. We set up the FSet library with extensional equality as inspired by Boruch-Gruszecki et al.'s artifact.

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