diff --git a/_CoqProject b/_CoqProject
index 152f62db8786881aa0f90ea5c0e8bb0dff05a46b..7c4d0a6361386a8749aac2e6150e630a9068e94c 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -82,6 +82,7 @@ heap_lang/derived.v
 heap_lang/heap.v
 heap_lang/notation.v
 heap_lang/spawn.v
+heap_lang/par.v
 heap_lang/tests.v
 heap_lang/substitution.v
 barrier/barrier.v
diff --git a/heap_lang/par.v b/heap_lang/par.v
new file mode 100644
index 0000000000000000000000000000000000000000..3bbdda8c5e49c51532f16ae52f9b10080d8d15a9
--- /dev/null
+++ b/heap_lang/par.v
@@ -0,0 +1,23 @@
+From heap_lang Require Export heap.
+From heap_lang Require Import spawn notation.
+
+Definition par : val :=
+  λ: "f1" "f2", let: "handle" := ^spawn '"f1" in
+                let: "v2" := '"f2" #() in
+                let: "v1" := ^join '"handle" in
+                Pair '"v1" '"v2".
+Notation Par e1 e2 := (^par (λ: <>, e1)%V (λ: <>, e2)%V)%E.
+
+Section proof.
+Context {Σ : rFunctorG} `{!heapG Σ, !spawnG Σ}.
+Context (heapN N : namespace).
+Local Notation iProp := (iPropG heap_lang Σ).
+
+Lemma par_spec (Ψ1 Ψ2 : val → iProp) (f1 f2 : val) (Φ : val → iProp) :
+  (#> f1 #() {{ Ψ1 }} ★ #> f2 #() {{ Ψ2 }} ★
+   ∀ v1 v2, Ψ1 v1 ★ Ψ2 v2 -★ Φ (PairV v1 v2))
+  ⊑ #> par f1 f2 {{ Φ }}.
+Proof.
+Abort.
+
+End proof.
\ No newline at end of file