diff --git a/_CoqProject b/_CoqProject
index 8fcb2177f5fa64098e0247e6eeae67ed1f4c4995..0296f374066876e2fd03d8c4d4130af8fd88d2db 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -60,8 +60,11 @@ theories/examples/coinflip.v
 
 theories/examples/par.v
 
+theories/experimental/cka.v
+
 theories/experimental/helping/offers.v
 theories/experimental/helping/helping_stack.v
 
 theories/experimental/hocap/counter.v
 theories/experimental/hocap/ticket_lock.v
+
diff --git a/theories/examples/or.v b/theories/examples/or.v
index f09352a816e919bbd8a146b424d320e79a528c5d..00ed7125c417c8931d67ce380222195bbeb6b968 100644
--- a/theories/examples/or.v
+++ b/theories/examples/or.v
@@ -153,7 +153,7 @@ Section rules.
   Qed.
 
   (** Associativity *)
-  Lemma or_assoc_l e1 e2 e3 e1' e2' e3' A :
+  Lemma or_assoc_l_v e1 e2 e3 e1' e2' e3' A :
     (REL e1 << e1' : A) -∗
     (REL e2 << e2' : A) -∗
     (REL e3 << e3' : A) -∗
@@ -168,16 +168,48 @@ Section rules.
     - rel_apply_r or_refines_r. by iRight.
   Qed.
 
+  Lemma or_assoc_l e1 e2 e3 e1' e2' e3' A :
+    (REL e1 << e1' : A) -∗
+    (REL e2 << e2' : A) -∗
+    (REL e3 << e3' : A) -∗
+    REL (e1 ⊕ (e2 ⊕ e3)) << ((e1' ⊕ e2') ⊕ e3') : A.
+  Proof.
+    iIntros "H1 H2 H3".
+    rel_pures_r.
+    repeat (rel_pures_l; rel_apply_l or_refines_l; iSplit).
+    - rel_apply_r or_refines_r. iLeft.
+      rel_pures_r. rel_apply_r or_refines_r. by iLeft.
+    - rel_apply_r or_refines_r. iLeft.
+      rel_pures_r. rel_apply_r or_refines_r. by iRight.
+    - rel_apply_r or_refines_r. by iRight.
+  Qed.
+
+  Lemma or_assoc_r e1 e2 e3 e1' e2' e3' A :
+    (REL e1 << e1' : A) -∗
+    (REL e2 << e2' : A) -∗
+    (REL e3 << e3' : A) -∗
+    REL ((e1 ⊕ e2) ⊕ e3) << (e1' ⊕ (e2' ⊕ e3')) : A.
+  Proof.
+    iIntros "H1 H2 H3".
+    rel_pures_r.
+    repeat (rel_pures_l; rel_apply_l or_refines_l; iSplit).
+    - rel_apply_r or_refines_r. by iLeft.
+    - rel_apply_r or_refines_r. iRight.
+      rel_pures_r. rel_apply_r or_refines_r. by iLeft.
+    - rel_apply_r or_refines_r. iRight.
+      rel_pures_r. rel_apply_r or_refines_r. by iRight.
+  Qed.
+
   (** Interaction between OR and sequencing. *)
   (** Standard in algebraic models of programming. *)
   Lemma or_seq_1 (f g h f' g' h' : expr) A :
     (REL f << f' : A) -∗
     (REL g << g' : A) -∗
     (REL h << h' : A) -∗
-    REL ((f ⊕ g)%V;; h)
-      << ((f';; h') ⊕ (g';; h'))%V : A.
+    REL ((f ⊕ g);; h)
+      << ((f';; h') ⊕ (g';; h')) : A.
   Proof.
-    iIntros "Hf Hg Hh".
+    iIntros "Hf Hg Hh". rel_pures_l. rel_pures_r.
     rel_apply_l or_refines_l; iSplit; simpl.
     - rel_apply_r or_refines_r.
       iLeft. iApply (refines_seq with "Hf Hh").
@@ -188,10 +220,10 @@ Section rules.
     (REL f << f' : A) -∗
     (REL g << g' : A) -∗
     (REL h << h' : A) -∗
-    REL ((f;; h) ⊕ (g;; h))%V
-      << ((f' ⊕ g')%V;; h') : A.
+    REL ((f;; h) ⊕ (g;; h))
+      << ((f' ⊕ g');; h') : A.
   Proof.
-    iIntros "Hf Hg Hh".
+    iIntros "Hf Hg Hh". rel_pures_l. rel_pures_r.
     rel_apply_l or_refines_l; iSplit; simpl.
     - rel_apply_r or_refines_r.
       iLeft. iApply (refines_seq with "Hf Hh").
@@ -206,15 +238,15 @@ Section rules.
     (REL f << f' : A) -∗
     (REL g << g' : A) -∗
     (REL h << h' : A) -∗
-    REL ((f;; g) ⊕ (f;; h))%V
-      << (f';; (g' ⊕ h')%V) : A.
+    REL ((f;; g) ⊕ (f;; h))
+      << (f';; (g' ⊕ h')) : A.
   Proof.
-    iIntros "Hf Hg Hh".
+    iIntros "Hf Hg Hh". rel_pures_l.
     rel_apply_l or_refines_l. iSplit.
     - iApply (refines_seq with "Hf").
-      rel_apply_r or_refines_r. by iLeft.
+      rel_pures_r. rel_apply_r or_refines_r. by iLeft.
     - iApply (refines_seq with "Hf").
-      rel_apply_r or_refines_r. by iRight.
+      rel_pures_r. rel_apply_r or_refines_r. by iRight.
   Qed.
 
 
@@ -238,9 +270,9 @@ Section rules.
          f;;
          (((resolve_proph: "p" to: #0);; g) ⊕
           ((resolve_proph: "p" to: #1);; h))%E) << (* Here we *have to* use the expr scope, otherwise "p" won't be substituted *)
-      ((f';; g') ⊕ (f';; h'))%V : A.
+      ((f';; g') ⊕ (f';; h')) : A.
   Proof.
-    iIntros (???) "Hf Hg Hh".
+    iIntros (???) "Hf Hg Hh". rel_pures_r.
     rel_newproph_l vs p as "Hp". repeat rel_pure_l.
     (rewrite !(subst_is_closed []) //; try by set_solver); [].
     rel_apply_r or_refines_r.
@@ -271,7 +303,7 @@ Section rules.
     (REL f << f' : A) -∗
     (REL g << g' : A) -∗
     (REL h << h' : A) -∗
-    REL (f;; (g ⊕ h)%V) <<
+    REL (f;; (g ⊕ h)) <<
     (let: "p" := NewProph in
          f';;
          (((resolve_proph: "p" to: #0);; g') ⊕
@@ -281,7 +313,8 @@ Section rules.
     rel_newproph_r p. repeat rel_pure_r.
     (rewrite !(subst_is_closed []) //; try by set_solver); [].
     iApply (refines_seq with "Hf").
-    repeat rel_pure_r. iApply (or_compatible with "[Hg] [Hh]").
+    rel_pures_l. rel_pures_r.
+    iApply (or_compatible with "[Hg] [Hh]").
     - rel_resolveproph_r. by repeat rel_pure_r.
     - rel_resolveproph_r. by repeat rel_pure_r.
   Qed.
diff --git a/theories/examples/par.v b/theories/examples/par.v
index 666cc2e5d67ef2875088a9d1a138060cf51dbb05..8083c39578b1fffceb7aa235ae7fe0f982528142 100644
--- a/theories/examples/par.v
+++ b/theories/examples/par.v
@@ -16,118 +16,216 @@ Axioms/rules for parallel composition
     also requires unfolding
 *)
 
+Notation "e1 ∥ e2" := (((e1;; #()) ||| (e2;; #()));; #())%E
+                        (at level 60) : expr_scope.
+(* Notation "e1 ∥ e2" := (((e1;; #()) ||| (e2;; #()))%V;; #()) *)
+(*                         (at level 60) : val_scope. *)
+
+
 Section rules.
   Context `{!relocG Σ, !spawnG Σ}.
 
-  Lemma par_r_1 e1 e2 t (A : lrel Σ) E :
-    ↑ relocN ⊆ E →
-    is_closed_expr [] e1 →
-    (∀ i C, i ⤇ fill C e1 ={E}=∗ ∃ (v : val),
-            i ⤇ fill C v ∗ REL t << (v, e2) @ E : A) -∗
-    REL t << (e1 ||| e2)%V @ E : A.
+  Lemma par_l_2 e1 e2 t :
+    (WP e1 {{ _, True }}) -∗
+    (REL e2 << t : ()) -∗
+    REL (e1 ∥ e2) << t : ().
   Proof.
-    iIntros (??) "H".
-    rel_rec_r. repeat rel_pure_r.
-    rel_rec_r.
-    repeat rel_pure_r. rel_alloc_r c2 as "Hc2".
-    repeat rel_pure_r. rel_fork_r i as "Hi".
-    { simpl. eauto. }
-    repeat rel_pure_r.
-    tp_pure i _. tp_bind i e1.
-    iMod ("H" with "Hi") as (v1) "[Hi H]".
-    iSimpl in "Hi". tp_pure i _. tp_store i.
-  Abort.
-    (* rewrite refines_eq /refines_def. *)
-    (* iIntros (ρ') "_". clear ρ'. *)
-    (* iIntros (j K) "Hj". *)
-    (* tp_bind j e2. *)
+    iIntros "He1 He2".
+    rel_pures_l. rel_rec_l.
+    rel_pures_l. rel_bind_l (spawn _).
+    iApply refines_wp_l.
+    pose (N:=nroot.@"par").
+    iApply (spawn_spec N (λ _, True)%I with "[He1]").
+    - wp_pures. wp_bind e1. iApply (wp_wand with "He1").
+      iIntros (?)  "_"; by wp_pures.
+    - iNext. iIntros (l) "hndl". iSimpl.
+      rel_pures_l. rel_bind_l e2. rel_bind_r t.
+      iApply (refines_bind with "He2").
+      iIntros (? ?) "[% %]"; simplify_eq/=.
+      rel_pures_l.
+      rel_bind_l (spawn.join _).
+      iApply refines_wp_l.
+      iApply (join_spec with "hndl").
+      iNext. iIntros (?) "_". simpl.
+      rel_pures_l. by rel_values.
+  Qed.
 
-  (* this one we can prove without unfolding *)
-  Lemma par_unit_1 e A :
-    (REL e << e : A) -∗
-    REL (#() ||| e)%V << e : lrel_true.
+  Lemma par_l_2' Q K e1 e2 t :
+    (WP e1 {{ _, Q }}) -∗
+    (REL e2 << t : ()) -∗
+    (Q -∗ REL #() << fill K (#() : expr) : ()) -∗
+    REL (e1 ∥ e2) << fill K t : ().
   Proof.
-    iIntros "He".
-    rel_rec_l. repeat rel_pure_l.
-    rel_bind_l (spawn _).
+    iIntros "He1 He2 Ht".
+    rel_pures_l. rel_rec_l.
+    rel_pures_l. rel_bind_l (spawn _).
     iApply refines_wp_l.
     pose (N:=nroot.@"par").
-    iApply (spawn_spec N (λ v, True)%I).
-    - by wp_pures.
+    iApply (spawn_spec N (λ _, Q)%I with "[He1]").
+    - wp_pures. wp_bind e1. iApply (wp_wand with "He1").
+      iIntros (?)  "HQ"; by wp_pures.
     - iNext. iIntros (l) "hndl". iSimpl.
-      repeat rel_pure_l. rel_bind_l e. rel_bind_r e.
-      iApply (refines_bind with "He").
-      iIntros (v v') "Hv". simpl.
-      repeat rel_pure_l.
+      rel_pures_l. rel_bind_l e2.
+      iApply (refines_bind with "He2").
+      iIntros (? ?) "[% %]"; simplify_eq/=.
+      rel_pures_l.
       rel_bind_l (spawn.join _).
       iApply refines_wp_l.
       iApply (join_spec with "hndl").
-      iNext. iIntros (?) "_". simpl.
-      repeat rel_pure_l. rel_values.
+      iNext. iIntros (?) "HQ". simpl.
+      rel_pures_l. by iApply "Ht".
   Qed.
-  Lemma par_unit_2 e A :
-    (REL e << e : A) -∗
-    REL e << (#() ||| e)%V : lrel_true.
+
+  Lemma par_l_1 e1 e2 t :
+    (REL e1 << t : ()) -∗
+    (WP e2 {{ _, True }}) -∗
+    REL (e1 ∥ e2) << t : ().
   Proof.
-    iIntros "H".
-    rel_rec_r. repeat rel_pure_r.
-    rel_rec_r.
-    repeat rel_pure_r. rel_alloc_r c2 as "Hc2".
-    repeat rel_pure_r. rel_fork_r i as "Hi".
-    repeat rel_pure_r.
+    iIntros "He1 He2".
+    rel_pures_l. rel_rec_l.
+    rel_pures_l.
+    pose (N:=nroot.@"par").
+    rewrite refines_eq /refines_def. iIntros (j K) "#Hspec Hj".
+    iModIntro. wp_bind (spawn _).
+    iApply (spawn_spec N (λ _, j ⤇ fill K #())%I with "[He1 Hj]").
+    - wp_pures. wp_bind e1.
+      iMod ("He1" with "Hspec Hj") as "He1".
+      iApply (wp_wand with "He1").
+      iIntros (?)  "P". wp_pures.
+      by iDestruct "P" as (v') "[Hj [-> ->]]".
+    - iNext. iIntros (l) "hndl". iSimpl.
+      wp_pures. wp_bind e2.
+      iApply (wp_wand with "He2"). iIntros (?) "_".
+      wp_pures.
+      wp_apply (join_spec with "hndl").
+      iIntros (?) "Hj". wp_pures. iExists #(). eauto with iFrame.
+  Qed.
+
+  Lemma par_l_1' Q K e1 e2 t :
+    (REL e1 << t : ()) -∗
+    (WP e2 {{ _, Q }}) -∗
+    (Q -∗ REL #() << fill K (#() : expr) : ()) -∗
+    REL (e1 ∥ e2) << fill K t : ().
+  Proof.
+    iIntros "He1 He2 Ht".
+    rel_pures_l. rel_rec_l.
+    rel_pures_l.
+    pose (N:=nroot.@"par").
+    rewrite {1 3}refines_eq /refines_def. iIntros (j K') "#Hspec Hj".
+    iModIntro. wp_bind (spawn _).
+    iApply (spawn_spec N (λ _, j ⤇ fill (K++K') #())%I with "[He1 Hj]").
+    - wp_pures. wp_bind e1.
+      rewrite -fill_app.
+      iMod ("He1" with "Hspec Hj") as "He1".
+      iApply (wp_wand with "He1").
+      iIntros (?)  "P". wp_pures.
+      by iDestruct "P" as (v') "[Hj [-> ->]]".
+    - iNext. iIntros (l) "hndl". iSimpl.
+      wp_pures. wp_bind e2.
+      iApply (wp_wand with "He2"). iIntros (?) "HQ".
+      wp_pures.
+      wp_apply (join_spec with "hndl").
+      iIntros (?) "Hj".
+      iSpecialize ("Ht" with "HQ").
+      rewrite refines_eq /refines_def.
+      rewrite fill_app.
+      iMod ("Ht" with "Hspec Hj") as "Ht".
+      rewrite wp_value_inv. iMod "Ht" as (?) "[Ht [_ ->]]".
+      wp_pures. iExists #(). eauto with iFrame.
+  Qed.
+
+  (* Lemma par_r_1 e1 e2 t (A : lrel Σ) E : *)
+  (*   ↑ relocN ⊆ E → *)
+  (*   is_closed_expr [] e1 → *)
+  (*   (∀ i C, i ⤇ fill C e1 ={E}=∗ ∃ (v : val), *)
+  (*           i ⤇ fill C v ∗ REL t << (v, e2) @ E : A) -∗ *)
+  (*   REL t << (e1 ||| e2)%V @ E : A. *)
+  (* Proof. *)
+  (*   iIntros (??) "H". *)
+  (*   rel_rec_r. repeat rel_pure_r. *)
+  (*   rel_rec_r. *)
+  (*   repeat rel_pure_r. rel_alloc_r c2 as "Hc2". *)
+  (*   repeat rel_pure_r. rel_fork_r i as "Hi". *)
+  (*   { simpl. eauto. } *)
+  (*   repeat rel_pure_r. *)
+  (*   tp_rec i. simpl. *)
+  (*   tp_bind i e1. *)
+  (*   iMod ("H" with "Hi") as (v1) "[Hi H]". *)
+  (*   iSimpl in "Hi". tp_pure i (InjR v1). tp_store i. *)
+  (* Abort. *)
+  (*   (* rewrite refines_eq /refines_def. *) *)
+  (*   (* iIntros (ρ') "_". clear ρ'. *) *)
+  (*   (* iIntros (j K) "Hj". *) *)
+  (*   (* tp_bind j e2. *) *)
+
+  (* this one we can prove without unfolding *)
+  Lemma par_unit_1 e :
+    (REL e << e : ()) -∗
+    REL (#() ∥ e) << e : ().
+  Proof.
+    iIntros "He".
+    iApply (par_l_2 with "[] He").
+    by iApply wp_value.
+  Qed.
+  Lemma par_unit_2 e :
+    (REL e << e : ()) -∗
+    REL e << (#() ∥ e) : ().
+  Proof.
+    iIntros "He".
+    rel_pures_r. rel_rec_r. rel_pures_r. rel_rec_r.
+    rel_pures_r. rel_alloc_r c2 as "Hc2".
+    rel_pures_r. rel_fork_r i as "Hi".
+    rel_pures_r.
     tp_rec i. simpl.
-    tp_pure i _. tp_store i.
+    tp_pures i. tp_store i.
     rel_bind_l e. rel_bind_r e.
-    iApply (refines_bind with "H").
-    iIntros (v v') "Hv". simpl.
-    repeat rel_pure_r.
-    rel_rec_r. rel_load_r. repeat rel_pure_r.
+    iApply (refines_bind with "He").
+    iIntros (v v') "[-> ->]".
+    simpl. rel_pures_r.
+    rel_rec_r. rel_load_r. rel_pures_r.
     rel_values.
   Qed.
 
-  Lemma par_comm e1 e2 (A B : lrel Σ) :
+  (* This proof is now simpler but it still requires unfolding the REL judgement *)
+  Lemma par_comm e1 e2 :
     is_closed_expr [] e1 →
     is_closed_expr [] e2 →
-    (REL e1 << e1 : A) -∗
-    (REL e2 << e2 : B) -∗
-    REL (e2 ||| e1)%V << (e1 ||| e2)%V : lrel_true.
+    (REL e1 << e1 : ()) -∗
+    (REL e2 << e2 : ()) -∗
+    REL (e2 ∥ e1) << (e1 ∥ e2) : ().
   Proof.
-    iIntros (??) "He1 He2". rel_rec_r. repeat rel_pure_r.
-    rel_rec_r.
-    repeat rel_pure_r. rel_alloc_r c2 as "Hc2".
-    repeat rel_pure_r. rel_fork_r i as "Hi".
+    iIntros (??) "He1 He2". rel_pures_r.
+    rel_rec_r. rel_pures_r. rel_rec_r.
+    rel_pures_r. rel_alloc_r c2 as "Hc2".
+    rel_pures_r. rel_fork_r i as "Hi".
     { simpl. eauto. }
-    repeat rel_pure_r.
-    tp_rec i. simpl.
-    rel_rec_l. repeat rel_pure_l.
-    rewrite {3}refines_eq /refines_def.
-    iIntros (j K) "#Hs Hj". iModIntro.
-    tp_bind j e2.
-    pose (C:=(AppRCtx (λ: "v2", let: "v1" := spawn.join #c2 in ("v1", "v2")) :: K)).
-    fold C.
-    pose (N:=nroot.@"par").
-    wp_bind (spawn _).
-    iApply (spawn_spec N with "[He2 Hj]").
-    - wp_lam. rewrite refines_eq /refines_def.
-      iMod ("He2" with "Hs Hj") as "He2".
-      iAssumption.
-    - iNext. iIntros (l) "l_hndl".
-      wp_pures. wp_bind e1.
-      rewrite refines_eq /refines_def.
+    tp_pure i (App _ _). simpl.
+    rel_pures_r.
+    rel_bind_r e2.
+    iApply refines_spec_ctx. iIntros "#Hs".
+    iApply (par_l_1' (i ⤇ (#c2 <- InjR (#();; #())))%I
+              with "He2 [He1 Hi]").
+    { rewrite refines_eq /refines_def.
       tp_bind i e1.
-      iMod ("He1" with "Hs Hi") as "He1".
-      iApply (wp_wand with "He1").
-      iIntros (v1). iDestruct 1 as (v2) "[Hi Hv]".
-      wp_pures. wp_bind (spawn.join _).
-      iApply (join_spec with "l_hndl").
-      iNext. iIntros (w1). iDestruct 1 as (w2) "[Hj Hw]".
-      unfold C. iSimpl in "Hi". iSimpl in "Hj".
-      tp_pures i. tp_store i.
-      tp_pures j.
-      tp_rec j.
-      tp_pures j. iApply fupd_wp. tp_load j.
-      tp_pures j.
-      iModIntro. wp_pures. iExists (v2, w2)%V. eauto.
+      iMod ("He1" with "Hs Hi") as "He1". simpl.
+      iApply (wp_wand with "He1"). iIntros (?).
+      iDestruct 1 as (?) "[Hi [-> ->]]". done. }
+    iIntros "Hi". simpl. rel_pures_r.
+    tp_pures i. tp_store i.
+    rel_rec_r. rel_load_r. rel_pures_r. rel_values.
+  Qed.
+
+  Lemma par_bot_2 e1 :
+    ⊢ REL bot #() << e1 ∥ bot #() : ().
+  Proof. rel_apply_l bot_l. Qed.
+
+  Lemma par_bot_1 e1 :
+    (WP e1 {{_ , True}}) -∗ (* TODO: what can we do about this assignment? *)
+    REL (e1 ∥ bot #()) << bot #() : ().
+  Proof.
+    iIntros "He1".
+    iApply (par_l_2 with "He1").
+    rel_apply_l bot_l.
   Qed.
 
   Lemma seq_par e1 e2 (A B : lrel Σ) :
diff --git a/theories/experimental/cka.v b/theories/experimental/cka.v
new file mode 100644
index 0000000000000000000000000000000000000000..9a03a12cde3c12c5697559f1359ea12168343753
--- /dev/null
+++ b/theories/experimental/cka.v
@@ -0,0 +1,238 @@
+(* ReLoC -- Relational logic for fine-grained concurrency *)
+(** (Concurrent) Kleene algebra laws.
+
+    This is still WIP.
+
+    We consider well-typed terms quotiented out by contextual equivalence:
+          { e | ⊢ₜ e : TUnit } / =ctx=
+    and show that this is almost a model of Concurrent Kleene Algebra
+*)
+
+From reloc Require Export reloc.
+From reloc.examples Require Export or par.
+Set Default Proof Using "Type".
+
+Notation "⊥" := (bot #()).
+
+Ltac use_logrel :=
+  eapply (refines_sound #[relocΣ;spawnΣ]); iIntros (? Δ).
+Tactic Notation "use_logrel/=" :=
+  use_logrel; rel_pures_l; rel_pures_r.
+
+
+Lemma typed_is_closed_empty e Ï„ :
+  ∅ ⊢ₜ e : τ → is_closed_expr [] e.
+Proof.
+  intros H%typed_is_closed. revert H.
+  by rewrite dom_empty_L elements_empty.
+Qed.
+
+Ltac fundamental := by iApply (refines_typed TUnit []).
+Ltac closedness := by (eapply typed_is_closed_empty; eauto).
+
+Lemma plus_zero e :
+  ∅ ⊢ₜ e : TUnit →
+  ∅ ⊨ (e ⊕ ⊥) =ctx= e : TUnit.
+Proof.
+  intros He. split.
+  - use_logrel/=. iApply or_bot_l. fundamental.
+  - use_logrel/=. iApply or_bot_r. fundamental.
+Qed.
+
+Lemma plus_idemp e :
+  ∅ ⊢ₜ e : TUnit →
+  ∅ ⊨ (e ⊕ e) =ctx= e : TUnit.
+Proof.
+  intros He. split.
+  - use_logrel/=. iApply or_idemp_l. fundamental.
+  - use_logrel/=. iApply or_idemp_r. fundamental.
+Qed.
+
+Lemma plus_comm e f :
+  ∅ ⊢ₜ e : TUnit →
+  ∅ ⊢ₜ f : TUnit →
+  ∅ ⊨ (e ⊕ f) =ctx= (f ⊕ e) : TUnit.
+Proof.
+  intros He Hf. split; use_logrel/=; iApply or_comm; fundamental.
+Qed.
+
+Lemma plus_assoc e f g :
+  ∅ ⊢ₜ e : TUnit →
+  ∅ ⊢ₜ f : TUnit →
+  ∅ ⊢ₜ g : TUnit →
+  ∅ ⊨ (e ⊕ f) ⊕ g =ctx= e ⊕ (f ⊕ g) : TUnit.
+Proof.
+  intros He Hf Hg. split.
+  - use_logrel. iApply or_assoc_r; fundamental.
+  - use_logrel. iApply or_assoc_l; fundamental.
+Qed.
+
+Lemma mult_assoc e f g :
+  ∅ ⊢ₜ e : TUnit →
+  ∅ ⊢ₜ f : TUnit →
+  ∅ ⊢ₜ g : TUnit →
+  ∅ ⊨ ((e ;; f) ;; g) =ctx= (e ;; (f ;; g)) : TUnit.
+Proof.
+  intros He Hf Hg. split.
+  - use_logrel/=.
+    rel_bind_l e. rel_bind_r e.
+    iApply refines_bind; first by fundamental.
+    iIntros (? ?) "_ /=". rel_pures_l. rel_pures_r.
+    iApply (refines_typed TUnit []). by apply Seq_typed.
+  - use_logrel/=.
+    rel_bind_l e. rel_bind_r e.
+    iApply refines_bind; first by fundamental.
+    iIntros (? ?) "_ /=". rel_pures_l. rel_pures_r.
+    iApply (refines_typed TUnit []). by apply Seq_typed.
+Qed.
+
+Lemma mult_distr_plus_l e f g :
+  ∅ ⊢ₜ e : TUnit →
+  ∅ ⊢ₜ f : TUnit →
+  ∅ ⊢ₜ g : TUnit →
+  ∅ ⊨ (e ;; (f ⊕ g)) =ctx= ((e ;; f) ⊕ (e ;; g)) : TUnit.
+Proof.
+  intros He Hf Hg. split.
+  - (* intermediate instrumented program *)
+    pose (P := (let: "p" := NewProph in
+         e;;
+         (((resolve_proph: "p" to: #0);; f) ⊕
+          ((resolve_proph: "p" to: #1);; g)))%E).
+    eapply (ctx_refines_transitive ∅ TUnit _ P).
+    + use_logrel. iApply seq_or_2_instrument; (fundamental || closedness).
+    + use_logrel. iApply seq_or_2'; (fundamental || closedness).
+  - use_logrel. iApply seq_or_1; fundamental.
+Qed.
+
+Lemma mult_distr_plus_r e f g :
+  ∅ ⊢ₜ e : TUnit →
+  ∅ ⊢ₜ f : TUnit →
+  ∅ ⊢ₜ g : TUnit →
+  ∅ ⊨ ((e ⊕ f) ;; g) =ctx= ((e ;; g) ⊕ (f ;; g)) : TUnit.
+Proof.
+  intros He Hf Hg. split.
+  - use_logrel. iApply or_seq_1; fundamental.
+  - use_logrel. iApply or_seq_2; fundamental.
+Qed.
+
+Lemma mult_one_r e :
+  ∅ ⊢ₜ e : TUnit →
+  ∅ ⊨ (e ;; #()) =ctx= e : TUnit.
+Proof.
+  intros He. split.
+  - use_logrel. rel_bind_l e. rel_bind_r e.
+    iApply refines_bind; first by fundamental.
+    iIntros (? ?) "[-> ->] /=". rel_pures_l.
+    rel_values.
+  - use_logrel. rel_bind_l e. rel_bind_r e.
+    iApply refines_bind; first by fundamental.
+    iIntros (? ?) "[-> ->] /=". rel_pures_r.
+    rel_values.
+Qed.
+
+Lemma mult_one_l e :
+  ∅ ⊢ₜ e : TUnit →
+  ∅ ⊨ (#() ;; e) =ctx= e : TUnit.
+Proof.
+  intros He. split; use_logrel; rel_pures_l; rel_pures_r; fundamental.
+Qed.
+
+Lemma mult_zero_r e :
+  ∅ ⊢ₜ e : TUnit →
+  ∅ ⊨ (e ;; ⊥) =ctx= ⊥ : TUnit.
+Proof.
+  intros He. split.
+  - use_logrel.
+    (* TODO!!! we need unary interpretation to show that e is safe *)
+    Abort.
+  (* - use_logrel. rel_apply_l bot_l. *)
+
+Lemma mult_zero_l e :
+  ∅ ⊢ₜ e : TUnit →
+  ∅ ⊨ (⊥ ;; e) =ctx= ⊥ : TUnit.
+Proof.
+  intros He. split; use_logrel; rel_apply_l bot_l.
+Qed.
+
+Notation "e ∥ f" := ((e ||| f);; #())%E (at level 60).
+
+Lemma par_comm e f :
+  ∅ ⊢ₜ e : TUnit →
+  ∅ ⊢ₜ f : TUnit →
+  ∅ ⊨ (e ∥ f) =ctx= (f ∥ e) : TUnit.
+Proof.
+  intros He Hf. split.
+  - use_logrel.
+    iApply par_comm; (fundamental || closedness).
+  - use_logrel.
+    iApply par_comm; (fundamental || closedness).
+Qed.
+
+Definition star : val := rec: "star" "f" :=
+  #() ⊕ ("f" #();; "star" "f").
+
+Notation "e **" := (star (λ: <>, e)%V) (at level 80).
+
+Section rules.
+  Context `{relocG Σ}.
+
+  Lemma star_compatible e e' :
+    □ (REL e << e' : ()) -∗
+    REL e ** << e' ** : ().
+  Proof.
+    iIntros "#He". iLöb as "IH". rel_rec_l. rel_rec_r.
+    repeat rel_pure_l. repeat rel_pure_r.
+    iApply or_compatible; first by rel_values.
+    iApply refines_seq.
+    - rel_pure_l. rel_pure_r. iAssumption.
+    - iApply "IH".
+  Qed.
+
+  (* Lemma star_refines_l e t : *)
+  (*   REL e ** << t : (). *)
+  (* Proof. *)
+  (*   iIntros "H". rel_rec_l. repeat rel_pure_l. *)
+  (*   iApply or_compatible; first by rel_values. *)
+  (*   iApply refines_seq. *)
+  (*   - rel_pure_l. rel_pure_r. iAssumption. *)
+  (*   - iApply "IH". *)
+
+  Lemma star_id_1 e e' :
+    □(REL e << e' : ()) -∗
+    REL e ** << (#() ⊕ (e';; e' **))%V : ().
+  Proof.
+    iIntros "#He".
+    rel_rec_l. repeat rel_pure_l. repeat rel_pure_r.
+    iApply or_compatible; first by rel_values.
+    iApply refines_seq.
+    - rel_pure_l. iAssumption.
+    - by iApply star_compatible.
+  Qed.
+
+  Lemma star_id_2 e e' :
+    □(REL e << e' : ()) -∗
+    REL (#() ⊕ (e;; e **))%V << e' ** : ().
+  Proof.
+    iIntros "#He". rel_rec_r. repeat rel_pure_r.
+    iApply or_compatible; first by rel_values.
+    iApply refines_seq.
+    - rel_pure_r. iAssumption.
+    - by iApply star_compatible.
+  Qed.
+
+  Lemma star_fp e f g :
+    □ (WP f {{ _, True }}) -∗
+    (REL (e ⊕ (f;; g))%V << g : ()) -∗
+    REL (f **;; e) << g : ().
+  Proof.
+    iIntros "#Hf H". iLöb as "IH".
+    rel_rec_l. repeat rel_pure_l.
+    rel_apply_l or_refines_l. iSplit.
+    - repeat rel_pure_l. (* need transitivity with "H" *) admit.
+    - repeat rel_pure_l. (* need that `f` is safe *)
+      rel_bind_l f. iApply refines_wp_l. iApply (wp_wand with "Hf").
+      iIntros (v) "_". simpl. repeat rel_pure_l. clear v.
+      by iApply "IH".
+  Abort.
+
+End rules.
diff --git a/theories/typing/types.v b/theories/typing/types.v
index c57ddcaa636025af4f904590153f6318c1f4c3fa..b816af339aaeb9d6c58d3456be62845c1d8aecbc 100644
--- a/theories/typing/types.v
+++ b/theories/typing/types.v
@@ -1,7 +1,7 @@
 (* ReLoC -- Relational logic for fine-grained concurrency *)
 (** (Syntactic) Typing for System F_mu_ref with existential types and concurrency *)
 From Autosubst Require Export Autosubst.
-From stdpp Require Export stringmap.
+From stdpp Require Export stringmap fin_map_dom gmap.
 From iris.heap_lang Require Export lang notation metatheory.
 
 (** * Types *)
@@ -233,6 +233,7 @@ Lemma binop_bool_typed_safe (op : bin_op) (b1 b2 : bool) Ï„ :
   binop_bool_res_type op = Some τ → is_Some (bin_op_eval op #b1 #b2).
 Proof. destruct op; naive_solver. Qed.
 
+
 Lemma unop_nat_typed_safe (op : un_op) (n : Z) Ï„ :
   unop_nat_res_type op = Some τ → is_Some (un_op_eval op #n).
 Proof. destruct op; simpl; eauto.  Qed.
@@ -240,3 +241,145 @@ Proof. destruct op; simpl; eauto.  Qed.
 Lemma unop_bool_typed_safe (op : un_op) (b : bool) Ï„ :
   unop_bool_res_type op = Some τ → is_Some (un_op_eval op #b).
 Proof. destruct op; naive_solver. Qed.
+
+(***********************************)
+(** Closedness of typed programs   *)
+
+(* DF: It is not trivial to prove the closedness lemma for
+[is_closed_expr], because it requires a lemma like this:
+
+    Lemma elements_insert Γ x τ :
+        elements (dom stringset (<[x:=τ]> Γ)) = x :: elements (dom stringset Γ).
+
+But this does not hold (it holds only up to multiset equality).
+So we use an auxiliary definition with sets *)
+
+Definition maybe_insert_binder (x : binder) (X : stringset) : stringset :=
+  match x with
+  | BAnon => X
+  | BNamed f => {[f]} ∪ X
+  end.
+
+Local Fixpoint is_closed_expr_set (X : stringset) (e : expr) : bool :=
+  match e with
+  | Val v => is_closed_val_set v
+  | Var x => bool_decide (x ∈ X)
+  | Rec f x e => is_closed_expr_set (maybe_insert_binder f (maybe_insert_binder x X)) e
+  | UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Free e | Load e =>
+     is_closed_expr_set X e
+  | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | AllocN e1 e2 | Store e1 e2 | FAA e1 e2 =>
+     is_closed_expr_set X e1 && is_closed_expr_set X e2
+  | If e0 e1 e2 | Case e0 e1 e2 | CmpXchg e0 e1 e2 | Resolve e0 e1 e2 =>
+     is_closed_expr_set X e0 && is_closed_expr_set X e1 && is_closed_expr_set X e2
+  | NewProph => true
+  end
+with is_closed_val_set (v : val) : bool :=
+  match v with
+  | LitV _ => true
+  | RecV f x e => is_closed_expr_set (maybe_insert_binder f (maybe_insert_binder x ∅)) e
+  | PairV v1 v2 => is_closed_val_set v1 && is_closed_val_set v2
+  | InjLV v | InjRV v => is_closed_val_set v
+  end.
+
+Lemma is_closed_expr_permute (e : expr) (xs ys : list string) :
+  xs ≡ₚ ys →
+  is_closed_expr xs e = is_closed_expr ys e.
+Proof.
+  revert xs ys. induction e=>xs ys Hxsys /=;
+    repeat match goal with
+    | [ |- _ && _ = _ && _ ] => f_equal
+    | [ H : ∀ xs ys, xs ≡ₚ ys → is_closed_expr xs _ = is_closed_expr ys _
+      |- is_closed_expr _ _ = is_closed_expr _ _ ] => eapply H; eauto
+    end; try done.
+  - apply bool_decide_iff. by rewrite Hxsys.
+  - by rewrite Hxsys.
+Qed.
+
+Global Instance is_closed_expr_proper : Proper (Permutation ==> eq ==> eq) is_closed_expr.
+Proof.
+  intros X1 X2 HX x y ->. by eapply is_closed_expr_permute.
+Qed.
+
+Lemma is_closed_expr_set_sound (X : stringset) (e : expr) :
+  is_closed_expr_set X e → is_closed_expr (elements X) e
+with is_closed_val_set_sound (v : val) :
+  is_closed_val_set v → is_closed_val v.
+Proof.
+  - induction e; simplify_eq/=; try by (intros; destruct_and?; split_and?; eauto).
+    + intros. case_bool_decide; last done.
+      by apply bool_decide_pack, elem_of_elements.
+    + destruct f as [|f], x as [|x]; simplify_eq/=.
+      * eapply IHe.
+      * intros H%is_closed_expr_set_sound.
+        eapply is_closed_weaken; eauto. by set_solver.
+      * intros H%is_closed_expr_set_sound.
+        eapply is_closed_weaken; eauto. by set_solver.
+      * intros H%is_closed_expr_set_sound.
+        eapply is_closed_weaken; eauto. by set_solver.
+  - induction v; simplify_eq/=; try naive_solver.
+    destruct f as [|f], x as [|x]; simplify_eq/=;
+      intros H%is_closed_expr_set_sound; revert H.
+    + set_solver.
+    + by rewrite ?right_id_L elements_singleton.
+    + by rewrite ?right_id_L elements_singleton.
+    + rewrite ?right_id_L.
+      intros. eapply is_closed_weaken; eauto.
+      destruct (decide (f = x)) as [->|?].
+      * rewrite union_idemp_L elements_singleton.
+        set_solver.
+      * rewrite elements_disj_union; last set_solver.
+        rewrite !elements_singleton. set_solver.
+Qed.
+
+Local Lemma typed_is_closed_set Γ e τ :
+  Γ ⊢ₜ e : τ → is_closed_expr_set (dom stringset Γ) e
+with typed_is_closed_val_set v Ï„ :
+    ⊢ᵥ v : τ → is_closed_val_set v.
+Proof.
+  - induction 1; simplify_eq/=; try (split_and?; by eapply typed_is_closed_set).
+    + apply bool_decide_pack. apply elem_of_dom. eauto.
+    + by eapply typed_is_closed_val_set.
+    + destruct f as [|f], x as [|x]; simplify_eq/=.
+      * eapply typed_is_closed_set. eauto.
+      * specialize (typed_is_closed_set (<[x:=τ1]>Γ) e τ2 H).
+        revert typed_is_closed_set. by rewrite dom_insert_L.
+      * specialize (typed_is_closed_set (<[f:=(τ1→τ2)%ty]>Γ) e τ2 H).
+        revert typed_is_closed_set. by rewrite dom_insert_L.
+      * specialize (typed_is_closed_set _ e Ï„2 H).
+        revert typed_is_closed_set.
+        rewrite (dom_insert_L (D:=stringset) (<[x:=τ1]> Γ) f (τ1→τ2)%ty).
+        by rewrite dom_insert_L.
+    + specialize (typed_is_closed_set (⤉Γ) e τ H).
+      revert typed_is_closed_set. by rewrite dom_fmap_L.
+    + by split_and?.
+    + by split_and?.
+    + split_and?; eauto. try (apply bool_decide_pack; by set_solver).
+      destruct x as [|x]; simplify_eq/=.
+      ++ specialize (typed_is_closed_set _ _ _ H0).
+         revert typed_is_closed_set. by rewrite dom_fmap_L.
+      ++ specialize (typed_is_closed_set _ _ _ H0).
+         revert typed_is_closed_set. rewrite (dom_insert_L (D:=stringset) (⤉Γ) x).
+         by rewrite dom_fmap_L.
+  - induction 1; simplify_eq/=; try done.
+    + by split_and?.
+    + destruct f as [|f], x as [|x]; simplify_eq/=.
+      * specialize (typed_is_closed_set _ _ _ H).
+        revert typed_is_closed_set. by rewrite dom_empty_L.
+      * specialize (typed_is_closed_set (<[x:=τ1]>∅) _ _ H).
+        revert typed_is_closed_set. by rewrite dom_insert_L dom_empty_L.
+      * specialize (typed_is_closed_set _ _ _ H).
+        revert typed_is_closed_set.
+        rewrite (dom_insert_L (D:=stringset) _ f (τ1→τ2)%ty).
+        by rewrite dom_empty_L.
+      * specialize (typed_is_closed_set _ _ _ H).
+        revert typed_is_closed_set.
+        rewrite (dom_insert_L (D:=stringset) (<[x:=τ1]> ∅) f (τ1→τ2)%ty).
+        by rewrite dom_insert_L dom_empty_L.
+    + specialize (typed_is_closed_set _ _ _ H).
+      revert typed_is_closed_set. by rewrite dom_empty_L.
+Qed.
+
+Theorem typed_is_closed Γ e τ :
+  Γ ⊢ₜ e : τ → is_closed_expr (elements (dom stringset Γ)) e.
+Proof. intros. eapply is_closed_expr_set_sound, typed_is_closed_set; eauto. Qed.
+