diff --git a/_CoqProject b/_CoqProject
index 2ccb23daf7082a0525187b630dad842a20656a30..1757f9d37abf659873e57e41e329f8520bd296e1 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -34,35 +34,35 @@ prelude/sets.v
 prelude/decidable.v
 prelude/list.v
 prelude/error.v
-modures/option.v
-modures/cmra.v
-modures/cmra_big_op.v
-modures/cmra_tactics.v
-modures/sts.v
-modures/auth.v
-modures/fin_maps.v
-modures/logic.v
-modures/cofe.v
-modures/base.v
-modures/dra.v
-modures/cofe_solver.v
-modures/agree.v
-modures/excl.v
-iris/model.v
-iris/adequacy.v
-iris/hoare_lifting.v
-iris/lifting.v
-iris/namespace.v
-iris/viewshifts.v
-iris/wsat.v
-iris/ownership.v
-iris/weakestpre.v
-iris/pviewshifts.v
-iris/resources.v
-iris/hoare.v
-iris/language.v
-iris/functor.v
-iris/tests.v
+algebra/option.v
+algebra/cmra.v
+algebra/cmra_big_op.v
+algebra/cmra_tactics.v
+algebra/sts.v
+algebra/auth.v
+algebra/fin_maps.v
+logic/upred.v
+algebra/cofe.v
+algebra/base.v
+algebra/dra.v
+algebra/cofe_solver.v
+algebra/agree.v
+algebra/excl.v
+program_logic/model.v
+program_logic/adequacy.v
+program_logic/hoare_lifting.v
+program_logic/lifting.v
+program_logic/namespace.v
+program_logic/viewshifts.v
+program_logic/wsat.v
+program_logic/ownership.v
+program_logic/weakestpre.v
+program_logic/pviewshifts.v
+program_logic/resources.v
+program_logic/hoare.v
+program_logic/language.v
+program_logic/functor.v
+program_logic/tests.v
 heap_lang/heap_lang.v
 heap_lang/heap_lang_tactics.v
 heap_lang/lifting.v
diff --git a/modures/agree.v b/algebra/agree.v
similarity index 99%
rename from modures/agree.v
rename to algebra/agree.v
index bceadd5189d4bc01d34855af417e1727f20a3fbc..65464cdd1f56cc45e7340b298be7693e53a470bc 100644
--- a/modures/agree.v
+++ b/algebra/agree.v
@@ -1,4 +1,4 @@
-Require Export modures.cmra.
+Require Export algebra.cmra.
 Local Hint Extern 10 (_ ≤ _) => omega.
 
 Record agree (A : Type) : Type := Agree {
diff --git a/modures/auth.v b/algebra/auth.v
similarity index 99%
rename from modures/auth.v
rename to algebra/auth.v
index c99b37013d75adfc4a748483d60b438f77be596f..32e76cd48c8b2a06d1214a3b8a8a0b27cf4eeb18 100644
--- a/modures/auth.v
+++ b/algebra/auth.v
@@ -1,4 +1,4 @@
-Require Export modures.excl.
+Require Export algebra.excl.
 Local Arguments validN _ _ _ !_ /.
 
 Record auth (A : Type) : Type := Auth { authoritative : excl A ; own : A }.
diff --git a/modures/base.v b/algebra/base.v
similarity index 100%
rename from modures/base.v
rename to algebra/base.v
diff --git a/modures/cmra.v b/algebra/cmra.v
similarity index 99%
rename from modures/cmra.v
rename to algebra/cmra.v
index 326f8b490bc583e9af63d475cecb46dc3ca7919b..8e1bbdff9697da2054894e3f811dbbe78600bc51 100644
--- a/modures/cmra.v
+++ b/algebra/cmra.v
@@ -1,4 +1,4 @@
-Require Export modures.cofe.
+Require Export algebra.cofe.
 
 Class Unit (A : Type) := unit : A → A.
 Instance: Params (@unit) 2.
diff --git a/modures/cmra_big_op.v b/algebra/cmra_big_op.v
similarity index 99%
rename from modures/cmra_big_op.v
rename to algebra/cmra_big_op.v
index c96118a095d009aa0644004294360c23c4392691..a11ce17f6a84882f99ce798099fddac572d1286c 100644
--- a/modures/cmra_big_op.v
+++ b/algebra/cmra_big_op.v
@@ -1,4 +1,4 @@
-Require Export modures.cmra.
+Require Export algebra.cmra.
 Require Import prelude.fin_maps.
 
 Fixpoint big_op {A : cmraT} `{Empty A} (xs : list A) : A :=
diff --git a/modures/cmra_tactics.v b/algebra/cmra_tactics.v
similarity index 97%
rename from modures/cmra_tactics.v
rename to algebra/cmra_tactics.v
index c2cce946a58e44e8b5fc5b43248471872fc56019..27b6efb85ab1b3457d0966bc38bbbb8413302a0a 100644
--- a/modures/cmra_tactics.v
+++ b/algebra/cmra_tactics.v
@@ -1,5 +1,5 @@
-Require Export modures.cmra.
-Require Import modures.cmra_big_op.
+Require Export algebra.cmra.
+Require Import algebra.cmra_big_op.
 
 (** * Simple solver for validity and inclusion by reflection *)
 Module ra_reflection. Section ra_reflection.
diff --git a/modures/cofe.v b/algebra/cofe.v
similarity index 99%
rename from modures/cofe.v
rename to algebra/cofe.v
index bab5b05d0f1387e3db3e6097895db3f063bd9ac7..2b48fcc6a5bc1a2551e39e16d48dd3655572d269 100644
--- a/modures/cofe.v
+++ b/algebra/cofe.v
@@ -1,4 +1,4 @@
-Require Export modures.base.
+Require Export algebra.base.
 
 (** Unbundeled version *)
 Class Dist A := dist : nat → relation A.
diff --git a/modures/cofe_solver.v b/algebra/cofe_solver.v
similarity index 99%
rename from modures/cofe_solver.v
rename to algebra/cofe_solver.v
index 977a6fdc5d6852f4986d93c370aa9cf12ad53bf8..b0c1543a48c0acf26afc5d08119f2a0af1c0ef86 100644
--- a/modures/cofe_solver.v
+++ b/algebra/cofe_solver.v
@@ -1,4 +1,4 @@
-Require Export modures.cofe.
+Require Export algebra.cofe.
 
 Record solution (F : cofeT → cofeT → cofeT) := Solution {
   solution_car :> cofeT;
diff --git a/modures/dra.v b/algebra/dra.v
similarity index 99%
rename from modures/dra.v
rename to algebra/dra.v
index 933deff4a0a7582946e6c0b4d1102c60e39c52eb..0e61179dac2bb483184e77cc9489aa2491c4d6f8 100644
--- a/modures/dra.v
+++ b/algebra/dra.v
@@ -1,4 +1,4 @@
-Require Export modures.cmra.
+Require Export algebra.cmra.
 
 (** From disjoint pcm *)
 Record validity {A} (P : A → Prop) : Type := Validity {
diff --git a/modures/excl.v b/algebra/excl.v
similarity index 99%
rename from modures/excl.v
rename to algebra/excl.v
index a86ccd72ed39153865250b7628d460940ea34e8f..a0be19baf60fa079e29e5923df257a8805f523ee 100644
--- a/modures/excl.v
+++ b/algebra/excl.v
@@ -1,4 +1,4 @@
-Require Export modures.cmra.
+Require Export algebra.cmra.
 Local Arguments validN _ _ _ !_ /.
 Local Arguments valid _ _  !_ /.
 
diff --git a/modures/fin_maps.v b/algebra/fin_maps.v
similarity index 99%
rename from modures/fin_maps.v
rename to algebra/fin_maps.v
index 58eb39cd178035ff341bd62d5d8e1e69e0a57b10..d9062626f465bf8f794c5a11efde21763bed82a3 100644
--- a/modures/fin_maps.v
+++ b/algebra/fin_maps.v
@@ -1,4 +1,4 @@
-Require Export modures.cmra prelude.gmap modures.option.
+Require Export algebra.cmra prelude.gmap algebra.option.
 
 Section cofe.
 Context `{Countable K} {A : cofeT}.
diff --git a/modures/option.v b/algebra/option.v
similarity index 99%
rename from modures/option.v
rename to algebra/option.v
index a553fa1b0df343e9c03e973824690e17a47a157e..071ecafb2c0719a064709dce1bf71fe1b0d1afb5 100644
--- a/modures/option.v
+++ b/algebra/option.v
@@ -1,4 +1,4 @@
-Require Export modures.cmra.
+Require Export algebra.cmra.
 
 (* COFE *)
 Section cofe.
diff --git a/modures/sts.v b/algebra/sts.v
similarity index 99%
rename from modures/sts.v
rename to algebra/sts.v
index 90ad94ba353c0376e779f20e2985a2b4d8b6a9c0..4e699e1d3f92c0e68946ccce691a3b1a6b141973 100644
--- a/modures/sts.v
+++ b/algebra/sts.v
@@ -1,5 +1,5 @@
-Require Export modures.cmra.
-Require Import prelude.sets modures.dra.
+Require Export algebra.cmra.
+Require Import prelude.sets algebra.dra.
 Local Arguments valid _ _ !_ /.
 Local Arguments op _ _ !_ !_ /.
 Local Arguments unit _ _ !_ /.
diff --git a/heap_lang/heap_lang.v b/heap_lang/heap_lang.v
index 5482c8e012b9fa59644b4021ebbf07389fa2ab1b..1511b05a59c78ba1b66c7d9c91a5057fc2c12cfa 100644
--- a/heap_lang/heap_lang.v
+++ b/heap_lang/heap_lang.v
@@ -1,5 +1,5 @@
 Require Export Autosubst.Autosubst.
-Require Export iris.language.
+Require Export program_logic.language.
 Require Import prelude.gmap.
 
 Module heap_lang.
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index e89728dacf42c632d1841d94f0d3c382e018d5f7..62df239ee2a0f44e9e213bd746e9907073165bd7 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -1,5 +1,5 @@
-Require Import prelude.gmap iris.lifting.
-Require Export iris.weakestpre heap_lang.heap_lang_tactics.
+Require Import prelude.gmap program_logic.lifting.
+Require Export program_logic.weakestpre heap_lang.heap_lang_tactics.
 Import uPred.
 Import heap_lang.
 Local Hint Extern 0 (language.reducible _ _) => do_step ltac:(eauto 2).
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index d5297a534633b8bbace109529d4973e01d7746e8..4ca0d01e22cc10f4c7ac51f07d13b924467cfb11 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -1,5 +1,5 @@
 (** This file is essentially a bunch of testcases. *)
-Require Import modures.logic.
+Require Import logic.upred.
 Require Import heap_lang.lifting heap_lang.sugar.
 Import heap_lang.
 Import uPred.
diff --git a/modures/logic.v b/logic/upred.v
similarity index 99%
rename from modures/logic.v
rename to logic/upred.v
index a50c0dbc344506883ae80b45a0249ff6acea0fb7..01f467cb0ee4c0e4abe110b5110a0f50cb376506 100644
--- a/modures/logic.v
+++ b/logic/upred.v
@@ -1,4 +1,4 @@
-Require Export modures.cmra.
+Require Export algebra.cmra.
 Local Hint Extern 1 (_ ≼ _) => etransitivity; [eassumption|].
 Local Hint Extern 1 (_ ≼ _) => etransitivity; [|eassumption].
 Local Hint Extern 10 (_ ≤ _) => omega.
diff --git a/iris/adequacy.v b/program_logic/adequacy.v
similarity index 98%
rename from iris/adequacy.v
rename to program_logic/adequacy.v
index 27d5ab13d304efdc35007edf55c3c541563845fd..1efb3abcd050b25f4e5e211fefa584df1769208a 100644
--- a/iris/adequacy.v
+++ b/program_logic/adequacy.v
@@ -1,5 +1,5 @@
-Require Export iris.hoare.
-Require Import iris.wsat.
+Require Export program_logic.hoare.
+Require Import program_logic.wsat.
 Local Hint Extern 10 (_ ≤ _) => omega.
 Local Hint Extern 100 (@eq coPset _ _) => eassumption || solve_elem_of.
 Local Hint Extern 10 (✓{_} _) =>
diff --git a/iris/functor.v b/program_logic/functor.v
similarity index 97%
rename from iris/functor.v
rename to program_logic/functor.v
index 49c7a0dfe2b3ad1a6ba3557ed0150b55fea9d388..cecfd67b288516515129a92e4fa5484b7858c7a0 100644
--- a/iris/functor.v
+++ b/program_logic/functor.v
@@ -1,4 +1,4 @@
-Require Export modures.cmra.
+Require Export algebra.cmra.
 
 Structure iFunctor := IFunctor {
   ifunctor_car :> cofeT → cmraT;
diff --git a/iris/hoare.v b/program_logic/hoare.v
similarity index 98%
rename from iris/hoare.v
rename to program_logic/hoare.v
index 100998cc27383d5a54daa9005cb5c653c861f473..f34281bf7f8f30b1eaa1b744bba761180fe026ec 100644
--- a/iris/hoare.v
+++ b/program_logic/hoare.v
@@ -1,4 +1,4 @@
-Require Export iris.weakestpre iris.viewshifts.
+Require Export program_logic.weakestpre program_logic.viewshifts.
 
 Definition ht {Λ Σ} (E : coPset) (P : iProp Λ Σ)
     (e : expr Λ) (Q : val Λ → iProp Λ Σ) : iProp Λ Σ :=
diff --git a/iris/hoare_lifting.v b/program_logic/hoare_lifting.v
similarity index 99%
rename from iris/hoare_lifting.v
rename to program_logic/hoare_lifting.v
index 172ce73bce51093eafc909f71af90c18e1b9f3a3..7ff9d1d7fe1ad19fa96c2a7d4d125bef96227bea 100644
--- a/iris/hoare_lifting.v
+++ b/program_logic/hoare_lifting.v
@@ -1,4 +1,4 @@
-Require Export iris.hoare iris.lifting.
+Require Export program_logic.hoare program_logic.lifting.
 
 Local Notation "{{ P } } ef ?@ E {{ Q } }" :=
   (default True%I ef (λ e, ht E P e Q))
diff --git a/iris/language.v b/program_logic/language.v
similarity index 98%
rename from iris/language.v
rename to program_logic/language.v
index 1a4bc01b2e71d1f942027e8a10f7dcffacfdf8af..783ac2a73205c49436b4248d8296ef246af6551e 100644
--- a/iris/language.v
+++ b/program_logic/language.v
@@ -1,4 +1,4 @@
-Require Export modures.cofe.
+Require Export algebra.cofe.
 
 Structure language := Language {
   expr : Type;
diff --git a/iris/lifting.v b/program_logic/lifting.v
similarity index 98%
rename from iris/lifting.v
rename to program_logic/lifting.v
index 94093941b2e5957a84d240be93a6ee4e784fa5bf..c028b22ce684f4742d6937cef16814571536178b 100644
--- a/iris/lifting.v
+++ b/program_logic/lifting.v
@@ -1,5 +1,5 @@
-Require Export iris.weakestpre.
-Require Import iris.wsat.
+Require Export program_logic.weakestpre.
+Require Import program_logic.wsat.
 Local Hint Extern 10 (_ ≤ _) => omega.
 Local Hint Extern 100 (@eq coPset _ _) => solve_elem_of.
 Local Hint Extern 10 (✓{_} _) =>
diff --git a/iris/model.v b/program_logic/model.v
similarity index 96%
rename from iris/model.v
rename to program_logic/model.v
index 6fde393bbf486b06a72d169c73c9378c281371d4..40be67805f849501a21349ae326bdf2eb9a8286e 100644
--- a/iris/model.v
+++ b/program_logic/model.v
@@ -1,5 +1,5 @@
-Require Export modures.logic iris.resources.
-Require Import modures.cofe_solver.
+Require Export logic.upred program_logic.resources.
+Require Import algebra.cofe_solver.
 
 Module iProp.
 Definition F (Λ : language) (Σ : iFunctor) (A B : cofeT) : cofeT :=
diff --git a/iris/namespace.v b/program_logic/namespace.v
similarity index 96%
rename from iris/namespace.v
rename to program_logic/namespace.v
index 7db3889275a6a5749595a5f5f9d6af05612ff13b..11c3a001c7dd849312843fc279801ce67ec3d142 100644
--- a/iris/namespace.v
+++ b/program_logic/namespace.v
@@ -1,4 +1,4 @@
-Require Export modures.base prelude.countable prelude.co_pset.
+Require Export algebra.base prelude.countable prelude.co_pset.
 
 Definition namespace := list positive.
 Definition nnil : namespace := nil.
diff --git a/iris/ownership.v b/program_logic/ownership.v
similarity index 98%
rename from iris/ownership.v
rename to program_logic/ownership.v
index fc168f419792c322719e1cefe6c7ff03827f102c..0fbbeb8ff18649f297af0fe645ac7e841ec4911d 100644
--- a/iris/ownership.v
+++ b/program_logic/ownership.v
@@ -1,4 +1,4 @@
-Require Export iris.model.
+Require Export program_logic.model.
 
 Definition inv {Λ Σ} (i : positive) (P : iProp Λ Σ) : iProp Λ Σ :=
   uPred_own (Res {[ i ↦ to_agree (Later (iProp_unfold P)) ]} ∅ ∅).
diff --git a/iris/pviewshifts.v b/program_logic/pviewshifts.v
similarity index 98%
rename from iris/pviewshifts.v
rename to program_logic/pviewshifts.v
index 4ff9bf80f3da6113267b80967d7f64a1342ad8f7..1ce9fc629bae1c826717f0cd36d8846f838d73cd 100644
--- a/iris/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -1,5 +1,5 @@
-Require Export iris.ownership prelude.co_pset.
-Require Import iris.wsat.
+Require Export program_logic.ownership prelude.co_pset.
+Require Import program_logic.wsat.
 Local Hint Extern 10 (_ ≤ _) => omega.
 Local Hint Extern 100 (@eq coPset _ _) => solve_elem_of.
 Local Hint Extern 100 (_ ∉ _) => solve_elem_of.
diff --git a/iris/resources.v b/program_logic/resources.v
similarity index 98%
rename from iris/resources.v
rename to program_logic/resources.v
index d2692b7daf05efa57f3cc8c74d80f58a099fd789..5692e645de60392349d6ce941908278035301622 100644
--- a/iris/resources.v
+++ b/program_logic/resources.v
@@ -1,5 +1,5 @@
-Require Export modures.fin_maps modures.agree modures.excl.
-Require Export iris.language iris.functor.
+Require Export algebra.fin_maps algebra.agree algebra.excl.
+Require Export program_logic.language program_logic.functor.
 
 Record res (Λ : language) (Σ : iFunctor) (A : cofeT) := Res {
   wld : mapRA positive (agreeRA A);
diff --git a/iris/tests.v b/program_logic/tests.v
similarity index 87%
rename from iris/tests.v
rename to program_logic/tests.v
index 6c03babaa8e1bc7ed78de3fea7e3ee6a6d5ed798..b499de9fab926a473890175117ac11f5c7ee42dc 100644
--- a/iris/tests.v
+++ b/program_logic/tests.v
@@ -1,5 +1,5 @@
 (** This file tests a bunch of things. *)
-Require Import iris.model.
+Require Import program_logic.model.
 
 Module ModelTest. (* Make sure we got the notations right. *)
   Definition iResTest {Λ : language} {Σ : iFunctor}
diff --git a/iris/viewshifts.v b/program_logic/viewshifts.v
similarity index 98%
rename from iris/viewshifts.v
rename to program_logic/viewshifts.v
index 55a54e1c1cb4a18b1e52fafc7e46d55438b777c5..c44d8a4158df434357bbc75b85d8ff32c9d8db98 100644
--- a/iris/viewshifts.v
+++ b/program_logic/viewshifts.v
@@ -1,4 +1,4 @@
-Require Export iris.pviewshifts.
+Require Export program_logic.pviewshifts.
 
 Definition vs {Λ Σ} (E1 E2 : coPset) (P Q : iProp Λ Σ) : iProp Λ Σ :=
   (□ (P → pvs E1 E2 Q))%I.
diff --git a/iris/weakestpre.v b/program_logic/weakestpre.v
similarity index 99%
rename from iris/weakestpre.v
rename to program_logic/weakestpre.v
index 2f4d50aeceebd53e2e46671a422bc0f103e07275..5d3a383f9874d0a1b5c923e96c17dde964e3c6a7 100644
--- a/iris/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -1,5 +1,5 @@
-Require Export iris.pviewshifts.
-Require Import iris.wsat.
+Require Export program_logic.pviewshifts.
+Require Import program_logic.wsat.
 Local Hint Extern 10 (_ ≤ _) => omega.
 Local Hint Extern 100 (@eq coPset _ _) => eassumption || solve_elem_of.
 Local Hint Extern 100 (_ ∉ _) => solve_elem_of.
diff --git a/iris/wsat.v b/program_logic/wsat.v
similarity index 98%
rename from iris/wsat.v
rename to program_logic/wsat.v
index 996842ca57debc795b932436a3a59516437acd77..6df7ef4be9423adf35becaf6cdd42fbf1a68539f 100644
--- a/iris/wsat.v
+++ b/program_logic/wsat.v
@@ -1,5 +1,5 @@
-Require Export iris.model prelude.co_pset.
-Require Export modures.cmra_big_op modures.cmra_tactics.
+Require Export program_logic.model prelude.co_pset.
+Require Export algebra.cmra_big_op algebra.cmra_tactics.
 Local Hint Extern 10 (_ ≤ _) => omega.
 Local Hint Extern 10 (✓{_} _) => solve_validN.
 Local Hint Extern 1 (✓{_} (gst _)) => apply gst_validN.