diff --git a/_CoqProject b/_CoqProject
index 46417a25346bf0ed913857e8c0c4fff86c301306..b5191d5d98dfa5629a64572586134966af166ebd 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -68,6 +68,7 @@ program_logic/ownership.v
 program_logic/weakestpre.v
 program_logic/weakestpre_fix.v
 program_logic/pviewshifts.v
+program_logic/lviewshifts.v
 program_logic/resources.v
 program_logic/hoare.v
 program_logic/language.v
diff --git a/program_logic/lviewshifts.v b/program_logic/lviewshifts.v
new file mode 100644
index 0000000000000000000000000000000000000000..694d153301647d44c33e8086be1f5fdcacb679df
--- /dev/null
+++ b/program_logic/lviewshifts.v
@@ -0,0 +1,23 @@
+From iris.program_logic Require Export pviewshifts.
+Import uPred.
+
+(* Some notation for linear view shifts. *)
+
+Definition lvs {Λ Σ} (E1 E2 : coPset) (P Q : iProp Λ Σ) : iProp Λ Σ :=
+  (P -★ |={E1,E2}=> Q)%I.
+Arguments lvs {_ _} _ _ _%I _%I.
+Instance: Params (@lvs) 4.
+Notation "P ={ E1 , E2 }=★ Q" := (lvs E1 E2 P%I Q%I)
+  (at level 99, E1,E2 at level 50, Q at level 200,
+   format "P  ={ E1 , E2 }=★  Q") : uPred_scope.
+Notation "P ={ E1 , E2 }=★ Q" := (True ⊢ (P ={E1,E2}=★ Q)%I)
+  (at level 99, E1, E2 at level 50, Q at level 200,
+   format "P  ={ E1 , E2 }=★  Q") : C_scope.
+Notation "P ={ E }=★ Q" := (P ={E,E}=★ Q)%I
+  (at level 99, E at level 50, Q at level 200,
+   format "P  ={ E }=★  Q") : uPred_scope.
+Notation "P ={ E }=★ Q" := (True ⊢ (P ={E}=★ Q)%I)
+  (at level 99, E at level 50, Q at level 200,
+   format "P  ={ E }=★  Q") : C_scope.
+
+(* TODO: Also prove some lemmas. *)