diff --git a/_CoqProject b/_CoqProject
index 54d3925c65972949475d6f505488ec71f7159e7d..8d3655da76fc44193dcca31018625bd1665c36ba 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -67,7 +67,7 @@ base_logic/big_op.v
 base_logic/hlist.v
 base_logic/soundness.v
 base_logic/double_negation.v
-program_logic/model.v
+program_logic/iprop.v
 program_logic/adequacy.v
 program_logic/lifting.v
 program_logic/invariants.v
@@ -80,7 +80,7 @@ program_logic/language.v
 program_logic/ectx_language.v
 program_logic/ectxi_language.v
 program_logic/ectx_lifting.v
-program_logic/ghost_ownership.v
+program_logic/own.v
 program_logic/saved_prop.v
 program_logic/auth.v
 program_logic/sts.v
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 9bf95350bd2959611940870d2337457741ff50e4..6cc7e17833cb208baa868ad9f30dfbfc1b09ab26 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -1,6 +1,6 @@
 From iris.heap_lang Require Export lifting.
 From iris.algebra Require Import auth gmap frac dec_agree.
-From iris.program_logic Require Export invariants ghost_ownership.
+From iris.program_logic Require Export invariants.
 From iris.program_logic Require Import wsat auth.
 From iris.proofmode Require Import tactics.
 Import uPred.
diff --git a/heap_lang/lib/barrier/protocol.v b/heap_lang/lib/barrier/protocol.v
index 97258bf775a636219142bb1df6ebf34f0ec5bd74..f59a64247884052841bda917db392355e0ad08f9 100644
--- a/heap_lang/lib/barrier/protocol.v
+++ b/heap_lang/lib/barrier/protocol.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Export sts.
-From iris.program_logic Require Import ghost_ownership.
+From iris.program_logic Require Import own.
 From iris.prelude Require Export gmap.
 
 (** The STS describing the main barrier protocol. Every state has an index-set
diff --git a/program_logic/model.v b/program_logic/iprop.v
similarity index 100%
rename from program_logic/model.v
rename to program_logic/iprop.v
diff --git a/program_logic/iris.v b/program_logic/iris.v
index 17d827315fcde3bc7b6a4117d84c5943e96d34dc..f0c91c2940682ba0eb7d8273e6f27be008ab8716 100644
--- a/program_logic/iris.v
+++ b/program_logic/iris.v
@@ -1,4 +1,4 @@
-From iris.program_logic Require Export ghost_ownership language.
+From iris.program_logic Require Export own language.
 From iris.prelude Require Export coPset.
 From iris.algebra Require Import gmap auth agree gset coPset.
 
diff --git a/program_logic/ghost_ownership.v b/program_logic/own.v
similarity index 99%
rename from program_logic/ghost_ownership.v
rename to program_logic/own.v
index 40c65ecd406b779d1da8f6be08aa89b5c8d059c7..e29317bb2771bbcf09ef2c5cd1b4c926e4e9d5c3 100644
--- a/program_logic/ghost_ownership.v
+++ b/program_logic/own.v
@@ -1,4 +1,4 @@
-From iris.program_logic Require Export model.
+From iris.program_logic Require Export iprop.
 From iris.algebra Require Import iprod gmap.
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import classes.
diff --git a/program_logic/saved_prop.v b/program_logic/saved_prop.v
index 235c246e384a48d78608c3737429d094a8e2c607..5a804a2a1f6f4e72c77576db631043ac921308a8 100644
--- a/program_logic/saved_prop.v
+++ b/program_logic/saved_prop.v
@@ -1,4 +1,4 @@
-From iris.program_logic Require Export ghost_ownership.
+From iris.program_logic Require Export own.
 From iris.algebra Require Import agree.
 From iris.prelude Require Import gmap.
 Import uPred.