diff --git a/_CoqProject b/_CoqProject
index 0f71e25dabb9259c7cfd8473a4e08fc8df003803..fc0dbb5108d4ed1f6a011bcb3e507604716b3de0 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -65,8 +65,9 @@ program_logic/resources.v
 program_logic/hoare.v
 program_logic/language.v
 program_logic/tests.v
-program_logic/auth.v
 program_logic/ghost_ownership.v
+program_logic/auth.v
+program_logic/sts.v
 heap_lang/heap_lang.v
 heap_lang/tactics.v
 heap_lang/lifting.v
diff --git a/program_logic/sts.v b/program_logic/sts.v
new file mode 100644
index 0000000000000000000000000000000000000000..b25ed4ded6a408c81be7f601d0593c9a8a1d124d
--- /dev/null
+++ b/program_logic/sts.v
@@ -0,0 +1,32 @@
+From algebra Require Export sts.
+From program_logic Require Export invariants ghost_ownership.
+Import uPred.
+
+Class StsInG Λ Σ (i : gid) {A B} (R : relation A) (tok : A → set B) := {
+  sts_inG :> InG Λ Σ i (stsRA R tok);
+}.
+
+Section definitions.
+  Context {Λ Σ A B} (i : gid) (R : relation A) (tok : A → set B)
+          `{!StsInG Λ Σ i R tok} (γ : gname).
+  Definition sts_inv  (φ : A → iPropG Λ Σ) : iPropG Λ Σ :=
+    (∃ s, own i γ (sts_auth R tok s set_all) ★ φ s)%I.
+  Definition sts_states (S : set A) (T: set B) : iPropG Λ Σ :=
+    (■ sts.closed R tok S T ∧ own i γ (sts_frag R tok S T))%I.
+  Definition sts_state (s : A) (T: set B) : iPropG Λ Σ :=
+    own i γ (sts_frag R tok (sts.up R tok s T) T).
+  Definition sts_ctx (N : namespace) (φ : A → iPropG Λ Σ) : iPropG Λ Σ :=
+    inv N (sts_inv φ).
+End definitions.
+Instance: Params (@sts_inv) 9.
+Instance: Params (@sts_states) 9.
+Instance: Params (@sts_ctx) 10.
+
+Section sts.
+  Context `{StsInG Λ Σ StsI (A:=A) R tok}.
+  Context (φ : A → iPropG Λ Σ).
+  Implicit Types N : namespace.
+  Implicit Types P Q R : iPropG Λ Σ.
+  Implicit Types γ : gname.
+
+End sts.