diff --git a/_CoqProject b/_CoqProject
index 5e5ad4f5c7fe9470ebb6457b38de40e2ad5aacf1..04256a8e63d51c4619561378ef3b57803a63b4b7 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -6,9 +6,9 @@ theories/proto/list.v
 theories/proto/channel.v
 theories/proto/involutive.v
 theories/proto/side.v
-theories/proto/stype_def.v
-theories/proto/stype.v
-theories/proto/stype_enc.v
+theories/proto/proto_def.v
+theories/proto/proto_specs.v
+theories/proto/proto_enc.v
 theories/proto/branching.v
 theories/examples/examples.v
 theories/examples/proofs.v
diff --git a/theories/examples/examples.v b/theories/examples/examples.v
index 4b6976d23ec8b1b3fb52eb17bb76cb6171acdf71..bf596026775dbf589071a49f49de420e4d4fafb6 100644
--- a/theories/examples/examples.v
+++ b/theories/examples/examples.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Import proofmode notation.
 From iris.base_logic Require Import invariants.
-From osiris.proto Require Import stype.
+From osiris.proto Require Import proto_specs.
 
 Section Examples.
   Context `{!heapG Σ} (N : namespace).
diff --git a/theories/examples/list_sort.v b/theories/examples/list_sort.v
index 9f492865d3b8e5340808c5ac8f33fcd0d6bd842f..630702ea5b4a67482fb3abd4443d6b310c50b964 100644
--- a/theories/examples/list_sort.v
+++ b/theories/examples/list_sort.v
@@ -4,8 +4,8 @@ Require Import Omega.
 From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Import proofmode notation.
-From osiris.proto Require Import list channel stype_enc.
 From iris.base_logic Require Import invariants.
+From osiris.proto Require Import list channel proto_enc.
 
 Section ListSortExample.
   Context `{!heapG Σ} `{logrelG val Σ} (N : namespace).
diff --git a/theories/examples/proofs.v b/theories/examples/proofs.v
index dc679f7b9307b5cc0c04219fe002a3761d9806ca..0e472cf5398ef9ff4d54707f9ebe93429cc5102d 100644
--- a/theories/examples/proofs.v
+++ b/theories/examples/proofs.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Import proofmode notation.
 From iris.base_logic Require Import invariants.
-From osiris.proto Require Import stype.
+From osiris.proto Require Import proto_specs.
 From osiris.examples Require Import examples.
 
 Section ExampleProofs.
diff --git a/theories/examples/proofs_enc.v b/theories/examples/proofs_enc.v
index 186c70668c9cad66b5753b842b13737360d6aeab..608ecfbf7b8eed9d77403ac786aa3b4dadeba40f 100644
--- a/theories/examples/proofs_enc.v
+++ b/theories/examples/proofs_enc.v
@@ -3,7 +3,7 @@ From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Import proofmode notation.
 From iris.algebra Require Import list auth excl.
 From iris.base_logic Require Import invariants.
-From osiris.proto Require Import stype_enc.
+From osiris.proto Require Import proto_enc.
 From osiris.examples Require Import examples.
 
 Section ExampleProofsEnc.
diff --git a/theories/proto/branching.v b/theories/proto/branching.v
index 7c552dc1ee3a55996da966bf688d2c625a4e9451..b511fa273e3839d3032b27ec56c96b80dad6df94 100644
--- a/theories/proto/branching.v
+++ b/theories/proto/branching.v
@@ -3,7 +3,7 @@ From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Import proofmode notation.
 From iris.algebra Require Import list auth excl.
 From iris.base_logic Require Import invariants.
-From osiris.proto Require Export stype_enc.
+From osiris.proto Require Export proto_enc.
 
 Section DualBranch.
   Context `{PROP : bi}.
diff --git a/theories/proto/stype_def.v b/theories/proto/proto_def.v
similarity index 100%
rename from theories/proto/stype_def.v
rename to theories/proto/proto_def.v
diff --git a/theories/proto/stype_enc.v b/theories/proto/proto_enc.v
similarity index 98%
rename from theories/proto/stype_enc.v
rename to theories/proto/proto_enc.v
index de6637fec83b1a062ca2f3959366f81fd3f0c9c5..05a775eb654f594d935fdf8aab0b45293c520077 100644
--- a/theories/proto/stype_enc.v
+++ b/theories/proto/proto_enc.v
@@ -3,7 +3,7 @@ From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Import proofmode notation.
 From iris.algebra Require Import list auth excl.
 From iris.base_logic Require Import invariants.
-From osiris.proto Require Export encodable stype.
+From osiris.proto Require Export encodable proto_specs.
 
 Section DualStypeEnc.
   Context `{EncDec V} `{PROP: bi} .
diff --git a/theories/proto/stype.v b/theories/proto/proto_specs.v
similarity index 99%
rename from theories/proto/stype.v
rename to theories/proto/proto_specs.v
index 48df2098e58b6569117e90533943e8139f32857f..c6d1277a333135b9c545323ee653824eef24950c 100644
--- a/theories/proto/stype.v
+++ b/theories/proto/proto_specs.v
@@ -6,7 +6,7 @@ From iris.heap_lang.lib Require Import spin_lock.
 From iris.algebra Require Import list auth excl.
 From iris.base_logic Require Import invariants.
 From osiris.base_logic Require Import auth_excl.
-From osiris.proto Require Export stype_def.
+From osiris.proto Require Export proto_def.
 From osiris.proto Require Export channel.
 
 Class logrelG A Σ := {