diff --git a/_CoqProject b/_CoqProject
index d44c0b041b98732851b68d953ebc4cc13af29984..89039c02ecdf3ca2a3c4fd2ab440af4bc1e476e9 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,4 +1,4 @@
--Q theories osiris
+-Q theories actris
 -arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
 theories/utils/auth_excl.v
 theories/utils/list.v
diff --git a/experimental/producer_consumer.v b/experimental/producer_consumer.v
index ed3d4d8ea4334457dca95a103349584e1d7b751a..c011e3202164bdd94ca6c8d5189a409702b0eb3c 100644
--- a/experimental/producer_consumer.v
+++ b/experimental/producer_consumer.v
@@ -1,8 +1,8 @@
 From stdpp Require Import sorting.
-From osiris.channel Require Import proto_channel proofmode.
+From actris.channel Require Import proto_channel proofmode.
 From iris.heap_lang Require Import proofmode notation.
 From iris.heap_lang Require Import assert.
-From osiris.utils Require Import list compare spin_lock.
+From actris.utils Require Import list compare spin_lock.
 
 Definition qenqueue : val := λ: "q" "v", #().
 Definition qdequeue : val := λ: "q", #().
diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index c2e70961904d6cc6172d4255b4f75d9cbb252f81..28ed36277807d2aef3e9d7fd15d7bd72c51251a5 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -1,7 +1,7 @@
 From iris.heap_lang Require Import proofmode notation.
 From iris.heap_lang.lib Require Import spin_lock.
 From iris.algebra Require Import excl auth list.
-From osiris.utils Require Import auth_excl list.
+From actris.utils Require Import auth_excl list.
 Set Default Proof Using "Type".
 
 Inductive side := Left | Right.
diff --git a/theories/channel/proofmode.v b/theories/channel/proofmode.v
index 8645c4a2d5b90f3978b46bc05a0798fad8a94367..cb4d487d2a65fcb78501b526cdefeb722682b214 100644
--- a/theories/channel/proofmode.v
+++ b/theories/channel/proofmode.v
@@ -1,6 +1,6 @@
 From iris.heap_lang Require Export proofmode notation.
 From iris.proofmode Require Export tactics.
-From osiris Require Export proto_channel.
+From actris Require Export proto_channel.
 From iris.proofmode Require Import coq_tactics reduction spec_patterns.
 
 (* TODO: strip laters *)
diff --git a/theories/channel/proto_channel.v b/theories/channel/proto_channel.v
index 032674358a04f993010108073bc5f0ce0e6634c1..c14a4559421e2952dffcb51f6c9cd79d0e6341fe 100644
--- a/theories/channel/proto_channel.v
+++ b/theories/channel/proto_channel.v
@@ -1,9 +1,9 @@
-From osiris.channel Require Export channel.
-From osiris.channel Require Import proto_model.
+From actris.channel Require Export channel.
+From actris.channel Require Import proto_model.
 From iris.base_logic.lib Require Import invariants.
 From iris.heap_lang Require Import proofmode notation.
 From iris.algebra Require Import auth excl.
-From osiris.utils Require Import auth_excl.
+From actris.utils Require Import auth_excl.
 Export action.
 
 Definition start_chan : val := λ: "f",
diff --git a/theories/examples/loop_sort.v b/theories/examples/loop_sort.v
index a779c923de7f71407ad0b254906a3fe1afcd759e..04aa8cceb54a03b225355ee0d3f2ba9202c883e9 100644
--- a/theories/examples/loop_sort.v
+++ b/theories/examples/loop_sort.v
@@ -1,8 +1,8 @@
 From stdpp Require Import sorting.
-From osiris.channel Require Import proto_channel.
+From actris.channel Require Import proto_channel.
 From iris.heap_lang Require Import proofmode notation.
-From osiris.utils Require Import list.
-From osiris.examples Require Import sort.
+From actris.utils Require Import list.
+From actris.examples Require Import sort.
 
 Definition loop_sort_service : val :=
   rec: "go" "c" :=
diff --git a/theories/examples/map.v b/theories/examples/map.v
index f134e622fe6cdbeb1b83dace6eb2e9d879e94b50..1282c31b77499f84db064be6e1761efe7ea7da8a 100644
--- a/theories/examples/map.v
+++ b/theories/examples/map.v
@@ -1,6 +1,6 @@
-From osiris.channel Require Import proto_channel proofmode.
+From actris.channel Require Import proto_channel proofmode.
 From iris.heap_lang Require Import proofmode notation lib.spin_lock.
-From osiris.utils Require Import list contribution.
+From actris.utils Require Import list contribution.
 From iris.algebra Require Import gmultiset.
 
 Definition map_worker : val :=
diff --git a/theories/examples/map_reduce.v b/theories/examples/map_reduce.v
index 4a015a22ce6485dd87aeafe94adbd0eec856d449..56176cc67f9c97b8f4467f7c4e48953facc6502f 100644
--- a/theories/examples/map_reduce.v
+++ b/theories/examples/map_reduce.v
@@ -1,8 +1,8 @@
 From stdpp Require Import sorting.
-From osiris.channel Require Import proto_channel proofmode.
+From actris.channel Require Import proto_channel proofmode.
 From iris.heap_lang Require Import proofmode notation.
-From osiris.utils Require Import list compare contribution.
-From osiris.examples Require Import map sort_elem sort_elem_client.
+From actris.utils Require Import list compare contribution.
+From actris.examples Require Import map sort_elem sort_elem_client.
 From iris.algebra Require Import gmultiset.
 From Coq Require Import SetoidPermutation.
 
diff --git a/theories/examples/sort.v b/theories/examples/sort.v
index 5ab7100086d097c1b81277e9dd44e3cebac9e644..6d29875fdb3537c5e1048ed3ab1f2726ee8f5920 100644
--- a/theories/examples/sort.v
+++ b/theories/examples/sort.v
@@ -1,7 +1,7 @@
 From stdpp Require Import sorting.
-From osiris.channel Require Import proto_channel proofmode.
+From actris.channel Require Import proto_channel proofmode.
 From iris.heap_lang Require Import proofmode notation.
-From osiris.utils Require Import list compare.
+From actris.utils Require Import list compare.
 
 Definition lmerge : val :=
   rec: "go" "cmp" "ys" "zs" :=
diff --git a/theories/examples/sort_client.v b/theories/examples/sort_client.v
index ec3de225aae7620fe21cd1f919e0c153531504b2..1353293c81f7ef6cdd03f83e8dad6eeca2412980 100644
--- a/theories/examples/sort_client.v
+++ b/theories/examples/sort_client.v
@@ -1,8 +1,8 @@
 From stdpp Require Import sorting.
-From osiris.channel Require Import proto_channel proofmode.
+From actris.channel Require Import proto_channel proofmode.
 From iris.heap_lang Require Import proofmode notation.
-From osiris.utils Require Import list compare.
-From osiris.examples Require Import sort.
+From actris.utils Require Import list compare.
+From actris.examples Require Import sort.
 
 Definition sort_client : val := λ: "cmp" "xs",
   let: "c" := start_chan sort_service in
diff --git a/theories/examples/sort_elem.v b/theories/examples/sort_elem.v
index def7cb92eb36a8801d5245743de72b1e3009dd77..171a70742a0dd4899e450453032df738bfa1c966 100644
--- a/theories/examples/sort_elem.v
+++ b/theories/examples/sort_elem.v
@@ -1,8 +1,8 @@
 From stdpp Require Import sorting.
-From osiris.channel Require Import proto_channel proofmode.
+From actris.channel Require Import proto_channel proofmode.
 From iris.heap_lang Require Import proofmode notation.
 From iris.heap_lang Require Import assert.
-From osiris.utils Require Import list compare.
+From actris.utils Require Import list compare.
 
 Definition cont := true.
 Definition stop := false.
diff --git a/theories/examples/sort_elem_client.v b/theories/examples/sort_elem_client.v
index 1c12e473ac8e2daace341a209df51942fc809db8..7662c6cedbb3800bc0ba62fbf42400803e088544 100644
--- a/theories/examples/sort_elem_client.v
+++ b/theories/examples/sort_elem_client.v
@@ -1,9 +1,9 @@
 From stdpp Require Import sorting.
-From osiris.channel Require Import proto_channel proofmode.
+From actris.channel Require Import proto_channel proofmode.
 From iris.heap_lang Require Import proofmode notation.
 From iris.heap_lang Require Import assert.
-From osiris.utils Require Import list compare.
-From osiris.examples Require Import sort_elem.
+From actris.utils Require Import list compare.
+From actris.examples Require Import sort_elem.
 
 Definition send_all : val :=
   rec: "go" "c" "xs" :=