diff --git a/racket/typed/syndicate/compile-spin.rkt b/racket/typed/syndicate/compile-spin.rkt
index f56239c..aa59d1c 100644
--- a/racket/typed/syndicate/compile-spin.rkt
+++ b/racket/typed/syndicate/compile-spin.rkt
@@ -779,6 +779,8 @@
      (gen-ltl-bin-op "W" p q)]
     [(strong-until p q)
      (gen-ltl-bin-op "U" p q)]
+    [(release p q)
+     (gen-ltl-bin-op "V" p q)]
     [(ltl-implies p q)
      (gen-ltl-bin-op "->" p q)]
     [(ltl-and p q)
diff --git a/racket/typed/syndicate/ltl.rkt b/racket/typed/syndicate/ltl.rkt
index 8989f42..a61a9b3 100644
--- a/racket/typed/syndicate/ltl.rkt
+++ b/racket/typed/syndicate/ltl.rkt
@@ -7,6 +7,7 @@
 ;;  - (eventually [LTL X])
 ;;  - (weak-until [LTL X] [LTL X])
 ;;  - (strong-until [LTL X] [LTL X])
+;;  - (release [LTL X] [LTL X])
 ;;  - (ltl-implies [LTL X] [LTL X])
 ;;  - (ltl-and [LTL X] [LTL X])
 ;;  - (ltl-or  [LTL X] [LTL X])
@@ -20,6 +21,7 @@
 (struct atomic [p] #:prefab)
 (struct weak-until [p q] #:prefab)
 (struct strong-until [p q] #:prefab)
+(struct release [p q] #:prefab)
 (struct ltl-implies [p q] #:prefab)
 (struct ltl-and [p q] #:prefab)
 (struct ltl-or [p q] #:prefab)
@@ -37,6 +39,8 @@
        (weak-until (loop p) (loop q))]
       [(strong-until p q)
        (strong-until (loop p) (loop q))]
+      [(release p q)
+       (release (loop p) (loop q))]
       [(ltl-implies p q)
        (ltl-implies (loop p) (loop q))]
       [(ltl-and p q)
diff --git a/racket/typed/syndicate/roles.rkt b/racket/typed/syndicate/roles.rkt
index 59d65dd..079caed 100644
--- a/racket/typed/syndicate/roles.rkt
+++ b/racket/typed/syndicate/roles.rkt
@@ -68,7 +68,7 @@
          export-roles export-type check-simulates check-has-simulating-subgraph lift+define-role
          verify-actors
          ;; LTL Syntax
-         True False Always Eventually Until WeakUntil Implies And Or Not A M
+         True False Always Eventually Until WeakUntil Release Implies And Or Not A M
          ;; Extensions
          match cond
          submod for-syntax for-meta only-in except-in
@@ -770,6 +770,7 @@
 (define-type Eventually : LTL -> LTL)
 (define-type Until : LTL LTL -> LTL)
 (define-type WeakUntil : LTL LTL -> LTL)
+(define-type Release : LTL LTL -> LTL)
 (define-type Implies : LTL LTL -> LTL)
 (define-type And : LTL * -> LTL)
 (define-type Or : LTL * -> LTL)
@@ -823,6 +824,7 @@
                     Eventually proto:eventually
                     Until proto:strong-until
                     WeakUntil proto:weak-until
+                    Release proto:release
                     Implies proto:ltl-implies
                     And proto:&&
                     Or proto:||