Sync up mechanization for f_sub_trans (#14)

* import new f_sub_trans * ckean up * doc * nits
TiarkRompf · Feb 19, 2025 · 03ac382 · 03ac382
1 parent c50eae2
commit 03ac382
Show file tree

Hide file tree

Showing 14 changed files with 10,176 additions and 0 deletions.
diff --git a/polymorphism/README.md b/polymorphism/README.md
@@ -6,16 +6,21 @@ The $λ^\diamond$-calculus [1], a refined reachability model that scales to para
 
 * [`Base`](lambda_diamond_base) -- Base system introducing the new reachability model, lacking type polymorphism.
 * [`Fsub`](f_sub_diamond) -- Bounded type-and-reachability polymorphism.
+* [`Fsub-Trans`](f_sub_trans) -- Bounded type-and-reachability polymorphism with explicit transitive closure.
 
 ```mermaid
 graph TD
     subgraph poly[Polymorphism]
       Base
       Fsub
+	  Fsub-Trans
     end
     Base-->Fsub
+	Base-->Fsub-Trans
 ```
 
+[`Fsub-Trans`](f_sub_trans) should be considered as the reference mechanization of the $F_{<:}^\diamond$-calculus from POPL '24.
+
 ## References
 
 [1] **Polymorphic Reachability Types: Tracking Aliasing and Separation in Higher-order Generic Programs** (POPL 2024)</br>