diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index 6ae5317db11f4a58bed825fdece0fef5a7b21149..7917ec7db29632c3356f81d160d3fbd42a2651f9 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -1,5 +1,9 @@
 (** This file contains the definition of the channels, encoded as a pair of
-lock-protected buffers, on which we define the three message-passing primitives:
+lock-protected buffers, and their primitive proof rules. Actris's proof rules
+for channels in terms of dependent separation protocols can be found in the file
+[theories/channel/proto_channel.v].
+
+In this file we define the three message-passing connectives:
 
 - [new_chan] creates references to two empty buffers and a lock, and returns a
   pair of endpoints, where the order of the two references determines the
@@ -8,13 +12,18 @@ lock-protected buffers, on which we define the three message-passing primitives:
 - [recv] performs a busy loop until there is something in the second buffer,
   which it pops and returns, locking during each peek.
 
-The specifications are defined in terms of the logical connectives [is_chan]
-and [chan_own]:
+The logically-atomic basic (i.e. non dependent separation protocol)
+proof rules [new_chan_spec], [send_spec] and [recv_spec] are defined in terms
+of the logical connectives [is_chan] and [chan_own]:
 
 - [is_chan γ v1 v2] is a persistent proposition expressing that [v1] and [v2]
   are the endpoints of a channel with logical name [γ].
 - [chan_own γ s vs] is an exclusive proposition expressing the buffer of side
-  [s] ([Left] or [Right]) has contents [vs]. *)
+  [s] ([Left] or [Right]) has contents [vs].
+
+Note that the specifications include 3 laters [â–·] to account for the three
+levels of indirection due to step-indexing in the model of dependent separation
+protocols. *)
 From iris.heap_lang Require Import proofmode notation.
 From iris.heap_lang.lib Require Import spin_lock.
 From iris.heap_lang Require Import lifting.
@@ -27,7 +36,7 @@ Instance side_inhabited : Inhabited side := populate Left.
 Definition side_elim {A} (s : side) (l r : A) : A :=
   match s with Left => l | Right => r end.
 
-(** Message-Passing Primitives *)
+(** * The definition of the message-passing connectives *)
 Definition new_chan : val :=
   λ: <>,
      let: "l" := lnil #() in
@@ -58,7 +67,7 @@ Definition recv : val :=
     | NONE => "go" "c"
     end.
 
-(** Channel ghost functor *)
+(** * Setup of Iris's cameras *)
 Class chanG Σ := {
   chanG_lockG :> lockG Σ;
   chanG_authG :> auth_exclG (listO valO) Σ;
@@ -77,7 +86,7 @@ Section channel.
     chan_r_name : gname
   }.
 
-  (** The invariant of channels *)
+  (** * The logical connectives *)
   Definition chan_inv (γ : chan_name) (l r : loc) : iProp Σ :=
     (∃ ls rs,
       llist sbi_internal_eq l ls ∗ own (chan_l_name γ) (● to_auth_excl ls) ∗
@@ -103,10 +112,10 @@ Section channel.
     iSplit; iDestruct 1 as (ls rs) "(?&?&?&?)"; iExists rs, ls; iFrame.
   Qed.
 
-  (** The ownership of channels *)
   Definition chan_own (γ : chan_name) (s : side) (vs : list val) : iProp Σ :=
     own (side_elim s chan_l_name chan_r_name γ) (◯ to_auth_excl vs)%I.
 
+  (** * The proof rules *)
   Global Instance chan_own_timeless γ s vs : Timeless (chan_own γ s vs).
   Proof. by apply _. Qed.
 
@@ -208,5 +217,4 @@ Section channel.
       iIntros "!> !>" (v vs' ->) "Hvs".
       iMod ("HΦ" with "[//] Hvs") as "HΦ". iIntros "!> !> !>". by wp_pures.
   Qed.
-
 End channel.
diff --git a/theories/channel/proofmode.v b/theories/channel/proofmode.v
index 74ca04083f3faf12327cec59a0315d38f970c876..ceb4f25639ea8e98836dd52089998616719dace6 100644
--- a/theories/channel/proofmode.v
+++ b/theories/channel/proofmode.v
@@ -1,44 +1,18 @@
-(** This file contains tactics for the message-passing connectives,
-as well as the necessary typeclasses.
-This includes a way of reducing protocols to a normal form, to prepare
-them for use in the appropriate specifications.
-This normalisation includes e.g. resolving duals.
-
-The tactics are:
-- [wp_send (x1 .. xn) with "selpat"] which resolves weakest preconditions of the
-form [wp (send c v) Q], in the presence of an ownership of a send protocol
-[c ↣  <!> x .. y, MSG v; {{ P }}; prot] in the context. That is done by using
-[x1 .. xn] to existentially quantify the variables [x .. y], and "ipat" to
-resolve the predicate [P]. The result is continuing as [Q],
-with [c ↣  prot] in the context.
-
-- [wp_recv (x1 .. xn) as "ipat"] which conversely resolves [wp (recv c) Q] with
-[c ↣  <?> x .. y, MSG v; {{ P }}; prot] in the context, where the variables
-[x .. y] are introduced as [x1 .. xn], and the predicate [P] is introduces based
-on the pattern [ipat].
-
-- [wp_select with "selpat"] which resolves [wp (select c b) Q] with
-[c ↣  prot1 {Q1}<+>{Q2} prot2] in the context. Here [selpat] is used to
-resolve either [Q1] or [Q2], based on the chosen branch. The resulting
-protocol is similarly [c ↣  prot1] or [c ↣  prot2] based on the chosen
-branch.
-
-- [wp_branch as ipat1 | ipat2] which resolves [wp (branch c e1 e2) Q] with
-[c ↣  prot1 {Q1}<&>{Q2} prot2] in the context. The result is two subgoals,
-in which [Q1] and [Q2] are introduced using [ipat1] and [ipat2], and the
-protocol ownership is [c ↣  prot1] and [c ↣  prot2] respectively. *)
-
+(** This file contains the definitions of Actris's tactics for symbolic
+execution of message-passing programs. The API of these tactics is documented
+in the [README.md] file. The implementation follows the same pattern for the
+implementation of these tactics that is used in Iris. In addition, it uses a
+standard pattern using type classes to perform the normalization.
+
+In addition to the tactics for symbolic execution, this file defines the tactic
+[solve_proto_contractive], which can be used to automatically prove that
+recursive protocols are contractive. *)
 From iris.heap_lang Require Export proofmode notation.
 From iris.proofmode Require Export tactics.
 From actris Require Export proto_channel.
 From iris.proofmode Require Import coq_tactics reduction spec_patterns.
 
-(** Classes *)
-Class ActionDualIf (d : bool) (a1 a2 : action) :=
-  dual_action_if : a2 = if d then action_dual a1 else a1.
-Hint Mode ActionDualIf ! ! - : typeclass_instances.
-
-(** Tactics for proving contractiveness of protocols *)
+(** * Tactics for proving contractiveness of protocols *)
 Ltac f_proto_contractive :=
   match goal with
   | _ => apply iProto_branch_contractive
@@ -53,7 +27,11 @@ Ltac f_proto_contractive :=
 Ltac solve_proto_contractive :=
   solve_proper_core ltac:(fun _ => first [f_contractive | f_proto_contractive | f_equiv]).
 
-(** Normalization of protocols *)
+(** * Normalization of protocols *)
+Class ActionDualIf (d : bool) (a1 a2 : action) :=
+  dual_action_if : a2 = if d then action_dual a1 else a1.
+Hint Mode ActionDualIf ! ! - : typeclass_instances.
+
 Instance action_dual_if_false a : ActionDualIf false a a := eq_refl.
 Instance action_dual_if_true_send : ActionDualIf true Send Receive := eq_refl.
 Instance action_dual_if_true_receive : ActionDualIf true Receive Send := eq_refl.
@@ -82,7 +60,6 @@ Section classes.
   Implicit Types p : iProto Σ.
   Implicit Types TT : tele.
 
-  (** Classes *)
   Lemma proto_unfold_eq p1 p2 : p1 ≡ p2 → ProtoUnfold p1 p2.
   Proof. rewrite /ProtoNormalize=> Hp d pas q ->. by rewrite Hp. Qed.
 
@@ -166,7 +143,8 @@ Section classes.
     destruct d; by rewrite /= -?iProto_app_branch -?iProto_dual_branch.
   Qed.
 
-  (** Automatically perform normalization of protocols in the proof mode *)
+  (** Automatically perform normalization of protocols in the proof mode when
+  using [iAssumption] and [iFrame]. *)
   Global Instance mapsto_proto_from_assumption q c p1 p2 :
     ProtoNormalize false p1 [] p2 →
     FromAssumption q (c ↣ p1) (c ↣ p2).
@@ -183,8 +161,8 @@ Section classes.
   Qed.
 End classes.
 
-(** Symbolic execution tactics *)
-(* TODO: strip laters *)
+(** * Symbolic execution tactics *)
+(* TODO: Maybe strip laters from other hypotheses in the future? *)
 Lemma tac_wp_recv `{!proto_chanG Σ, !heapG Σ} {TT : tele} Δ i j K
     c p (pc : TT → val * iProp Σ * iProto Σ) Φ :
   envs_lookup i Δ = Some (false, c ↣ p)%I →
diff --git a/theories/channel/proto_channel.v b/theories/channel/proto_channel.v
index ffb89b78aa4fdb5b636781f86d781932b88c1b21..3f237b011d5b56f2016f84f1b18d83b9b7ffbad9 100644
--- a/theories/channel/proto_channel.v
+++ b/theories/channel/proto_channel.v
@@ -1,44 +1,43 @@
-(** This file contains an instantiation of the
-Dependent Separation Protocols and an integration with the channel encodings.
-For starters this means fixing the types of messages to the
-value type of the language [val] and the logic to the Iris logic [iProp Σ].
+(** This file defines the core of the Actris logic:
+
+- It defines dependent separation protocols and the various operations on it
+  dual, append, branching
+- It defines the connective [c ↣ prot] for ownership of channel endpoints.
+- It proves Actris's specifications of [send] and [receive] w.r.t. dependent
+  separation protocols.
+
+Dependent separation protocols are defined by instanting the parametrized
+version in [proto_model] with type of values [val] of HeapLang and the
+propositions [iProp] of Iris.
 
 In doing so we define ways of constructing instances of the instantiated type
 via two constructors:
-- [iProto_end] which is identical to [proto_end]
-- [iProto_message] which takes an action and a continuation to construct
-the corresponding message protocols.
-
-For convenience sake the following notation is provided:
-- [END] which is simply [iProto_end]
-- [<!> x .. y, MSG v; {{ P }}; prot] and
-- [<?> x .. y, MSG v; {{ P }}; prot] which constructs an instance of
-iProto_message with an appropriate continuation.
-
-Said continuation ultimately establishes the following:
-- Existential quantification of variables [x .. y].
-- The equivalence [v = w], where [w] is the value that is eventually exchanged.
-- Ownership of the predicate [P]
-- A continuation as [prot]
-
-Futhermore type-specific variants of dual and append are provided:
-- [iProto_dual] which turns all [Send] of a protocol into [Recv] and vice-versa
-- [iProto_app] which appends two protocols as described in proto_model.v
-
-An encoding of branching behaviour is additionally included, defined
-in terms of sending and receiving boolean flags:
-- [prot1 {Q1}<+>{Q2} prot2] and
-- [prot1 {Q1}<&>{Q2} prot2] which defines ownership of Q1 or Q2, and continues as
-Q1 or Q2, based on the exchanged flag.
-
-The logical connective of protocol ownership is then defined:
-- [c ↣  prot] which describes that channel endpoint [c] adheres
-to protocol [prot], achieved through Iris invariants and ghost state along
-with the logical connectives of the channel encodings [is_chan] and [chan_own]. 
-
-Lastly, relevant typeclasses are defined for each of the above notions,
-such as contractiveness and non-expansiveness, after which the specifications
-of the message-passing primitives are defined in terms of the protocol connectives.*)
+- [iProto_end], which is identical to [proto_end].
+- [iProto_message], which takes an action and a continuation to construct
+  the corresponding message protocols.
+
+For convenience sake, we provide the following notations:
+- [END], which is simply [iProto_end].
+- [<!> x1 .. xn, MSG v; {{ P }}; prot] and [<?> x1 .. xn, MSG v; {{ P }}; prot],
+  which construct an instance of [iProto_message] with the appropriate
+  continuation.
+
+Futhermore, we define the following operations:
+- [iProto_dual], which turns all [Send] of a protocol into [Recv] and vice-versa
+- [iProto_app], which appends two protocols as described in proto_model.v
+
+An encoding of the usual branching connectives [prot1 {Q1}<+>{Q2} prot2] and
+[prot1 {Q1}<&>{Q2} prot2], inspired by session types, is also included in this
+file.
+
+The logical connective for protocol ownership is denoted as [c ↣ prot]. It
+describes that channel endpoint [c] adheres to protocol [prot]. This connective
+is modeled using Iris invariants and ghost state along with the logical
+connectives of the channel encodings [is_chan] and [chan_own].
+
+Lastly, relevant typeclasses are defined for each of the above notions, such as
+contractiveness and non-expansiveness, after which the specifications of the
+message-passing primitives are defined in terms of the protocol connectives. *)
 From actris.channel Require Export channel.
 From actris.channel Require Import proto_model.
 From iris.base_logic.lib Require Import invariants.
@@ -51,7 +50,7 @@ Definition start_chan : val := λ: "f",
   let: "cc" := new_chan #() in
   Fork ("f" (Snd "cc"));; Fst "cc".
 
-(** Camera setup *)
+(** * Setup of Iris's cameras *)
 Class proto_chanG Σ := {
   proto_chanG_chanG :> chanG Σ;
   proto_chanG_authG :> auth_exclG (laterO (proto val (iPrePropO Σ) (iPrePropO Σ))) Σ;
@@ -64,12 +63,12 @@ Definition proto_chanΣ := #[
 Instance subG_chanΣ {Σ} : subG proto_chanΣ Σ → proto_chanG Σ.
 Proof. intros [??%subG_auth_exclG]%subG_inv. constructor; apply _. Qed.
 
-(** Types *)
+(** * Types *)
 Definition iProto Σ := proto val (iPropO Σ) (iPropO Σ).
 Delimit Scope proto_scope with proto.
 Bind Scope proto_scope with iProto.
 
-(** Operators *)
+(** * Operators *)
 Definition iProto_end_def {Σ} : iProto Σ := proto_end.
 Definition iProto_end_aux : seal (@iProto_end_def). by eexists. Qed.
 Definition iProto_end := iProto_end_aux.(unseal).
@@ -79,7 +78,7 @@ Arguments iProto_end {_}.
 Program Definition iProto_message_def {Σ} {TT : tele} (a : action)
     (pc : TT → val * iProp Σ * iProto Σ) : iProto Σ :=
   proto_message a (λ v, λne f, ∃ x : TT,
-    (* Need the laters to make [iProto_message] contractive *)
+    (** We need the later to make [iProto_message] contractive *)
     ⌜ v = (pc x).1.1 ⌝ ∗
     ▷ (pc x).1.2 ∗
     f (Next (pc x).2))%I.
@@ -163,7 +162,7 @@ Notation "<?> 'MSG' v ; p" :=
 
 Notation "'END'" := iProto_end : proto_scope.
 
-(** Dual *)
+(** * Operations *)
 Definition iProto_dual {Σ} (p : iProto Σ) : iProto Σ :=
   proto_map action_dual cid cid p.
 Arguments iProto_dual {_} _%proto.
@@ -173,7 +172,6 @@ Definition iProto_dual_if {Σ} (d : bool) (p : iProto Σ) : iProto Σ :=
 Arguments iProto_dual_if {_} _ _%proto.
 Instance: Params (@iProto_dual_if) 2 := {}.
 
-(** Branching *)
 Definition iProto_branch {Σ} (a : action) (P1 P2 : iProp Σ)
     (p1 p2 : iProto Σ) : iProto Σ :=
   (<a> (b : bool), MSG #b {{ if b then P1 else P2 }}; if b then p1 else p2)%proto.
@@ -189,13 +187,12 @@ Infix "<{ P1 }&>" := (iProto_branch Receive P1 True) (at level 85) : proto_scope
 Infix "<+>" := (iProto_branch Send True True) (at level 85) : proto_scope.
 Infix "<&>" := (iProto_branch Receive True True) (at level 85) : proto_scope.
 
-(** Append *)
 Definition iProto_app {Σ} (p1 p2 : iProto Σ) : iProto Σ := proto_app p1 p2.
 Arguments iProto_app {_} _%proto _%proto.
 Instance: Params (@iProto_app) 1 := {}.
 Infix "<++>" := iProto_app (at level 60) : proto_scope.
 
-(** Auxiliary definitions and invariants *)
+(** * Auxiliary definitions and invariants *)
 Fixpoint proto_interp `{!proto_chanG Σ} (vs : list val) (p1 p2 : iProto Σ) : iProp Σ :=
   match vs with
   | [] => p1 ≡ iProto_dual p2
@@ -234,6 +231,7 @@ Definition proto_inv `{!proto_chanG Σ} (γ : proto_name) : iProp Σ :=
 
 Definition protoN := nroot .@ "proto".
 
+(** * The connective for ownership of channel ends *)
 Definition mapsto_proto_def `{!proto_chanG Σ, !heapG Σ}
     (c : val) (p : iProto Σ) : iProp Σ :=
   (∃ s (c1 c2 : val) γ,
@@ -248,12 +246,13 @@ Instance: Params (@mapsto_proto) 4 := {}.
 Notation "c ↣ p" := (mapsto_proto c p)
   (at level 20, format "c  ↣  p").
 
+(** * Proofs *)
 Section proto.
   Context `{!proto_chanG Σ, !heapG Σ}.
   Implicit Types p : iProto Σ.
   Implicit Types TT : tele.
 
-  (** Non-expansiveness of operators *)
+  (** ** Non-expansiveness of operators *)
   Lemma iProto_message_contractive {TT} a
       (pc1 pc2 : TT → val * iProp Σ * iProto Σ) n :
     (∀.. x, (pc1 x).1.1 = (pc2 x).1.1) →
@@ -307,7 +306,7 @@ Section proto.
     by apply iProto_message_proper=> /= -[].
   Qed.
 
-  (** Dual *)
+  (** ** Dual *)
   Global Instance iProto_dual_ne : NonExpansive (@iProto_dual Σ).
   Proof. solve_proper. Qed.
   Global Instance iProto_dual_proper : Proper ((≡) ==> (≡)) (@iProto_dual Σ).
@@ -341,7 +340,7 @@ Section proto.
     by apply iProto_message_proper=> /= -[].
   Qed.
 
-  (** Append *)
+  (** ** Append *)
   Global Instance iProto_app_ne : NonExpansive2 (@iProto_app Σ).
   Proof. apply _. Qed.
   Global Instance iProto_app_proper : Proper ((≡) ==> (≡) ==> (≡)) (@iProto_app Σ).
@@ -377,7 +376,7 @@ Section proto.
     iProto_dual (p1 <++> p2) ≡ (iProto_dual p1 <++> iProto_dual p2)%proto.
   Proof. by rewrite /iProto_dual /iProto_app proto_map_app. Qed.
 
-  (** Auxiliary definitions and invariants *)
+  (** ** Auxiliary definitions and invariants *)
   Global Instance proto_interp_ne : NonExpansive2 (proto_interp vs).
   Proof. induction vs; solve_proper. Qed.
   Global Instance proto_interp_proper vs : Proper ((≡) ==> (≡) ==> (≡)) (proto_interp vs).
@@ -457,7 +456,7 @@ Section proto.
 
   Arguments proto_interp : simpl never.
 
-  (** The actual specs *)
+  (** ** Initialization of a channel *)
   Lemma proto_init E cγ c1 c2 p :
     is_chan protoN cγ c1 c2 -∗
     chan_own cγ Left [] -∗ chan_own cγ Right [] ={E}=∗
@@ -478,7 +477,7 @@ Section proto.
     - iExists Right, c1, c2, pγ; iFrame; auto.
   Qed.
 
-  (** Accessor style lemmas *)
+  (** ** Accessor style lemmas *)
   Lemma proto_send_acc {TT} E c (pc : TT → val * iProp Σ * iProto Σ) :
     ↑protoN ⊆ E →
     c ↣ iProto_message Send pc -∗ ∃ s c1 c2 γ,
@@ -611,7 +610,7 @@ Section proto.
         iExists x. iFrame "Hv HP". by iRewrite "Hq".
   Qed.
 
-  (** Specifications of send and receive *)
+  (** ** Specifications of [send] and [receive] *)
   Lemma new_chan_proto_spec :
     {{{ True }}}
       new_chan #()
@@ -648,6 +647,8 @@ Section proto.
     iMod ("H" $! x with "Hf Hvs"); auto.
   Qed.
 
+  (** A version written without Texan triples that is more convenient to use
+  (via [iApply] in Coq. *)
   Lemma send_proto_spec {TT} Ψ c v (pc : TT → val * iProp Σ * iProto Σ) :
     c ↣ iProto_message Send pc -∗
     (∃.. x : TT,
@@ -688,6 +689,8 @@ Section proto.
     iDestruct "H" as (x ->) "H". by iApply "HΨ".
   Qed.
 
+  (** A version written without Texan triples that is more convenient to use
+  (via [iApply] in Coq. *)
   Lemma recv_proto_spec {TT} Ψ c (pc : TT → val * iProp Σ * iProto Σ) :
     c ↣ iProto_message Receive pc -∗
     ▷ (∀.. x : TT, c ↣ (pc x).2 -∗ (pc x).1.2 -∗ Ψ (pc x).1.1) -∗
@@ -698,7 +701,7 @@ Section proto.
     iApply ("H" with "[$] [$]").
   Qed.
 
-  (** Branching *)
+  (** ** Specifications for branching *)
   Lemma select_spec c (b : bool) P1 P2 p1 p2 :
     {{{ c ↣ (p1 <{P1}+{P2}> p2) ∗ if b then P1 else P2 }}}
       send c #b
diff --git a/theories/channel/proto_model.v b/theories/channel/proto_model.v
index 172a45122b550eae0490879660af32134e73f902..aed495a33d6de9f095e5e0258750372ba6f1543a 100644
--- a/theories/channel/proto_model.v
+++ b/theories/channel/proto_model.v
@@ -1,41 +1,44 @@
-(** This file defines the model of Dependent Separation Protocols,
-along with various operations on the connective, such as append
-and map and the necessary typeclass instances.
-
-They are designed with inspiration from Session Types, mimicking
-their constructors !T.st, ?T.st and END, respectively representing
-sending and receiving messages of type T and termination.
-The main difference is that the protocols are defined over predicates,
-in place of types.
-
-Dependent Separation Protocols are modelled as the following type:
-- [proto := 1 + (action * (V → (▶ proto → PROP) → PROP))]
-
-Here the left-hand side of the sum is used for the terminated process,
-while the right-hand side is used for the communication constructors.
-[action] is an inductively defined datatype with two constructors,
-that is used to differentiate between sending and received, rather than
-having two distinct sums in [proto].
-- [action := Send | Receive]
-
-The remainder (V → (▶ [proto] → PROP) → PROP)) is a continuation that
-depends on the communicated value V and the dependent tail (▶ proto → PROP)
-from protocols guarded under laters to the propositions of the logic.
-
-The constructors of the protocol are:
-- [proto_end] which constructs the left-side of the sum.
-- [proto_msg] which takes an action and a continuation and constructs the
-right-hand side of the sum accodingly.
-
-The type is defined as a solution to a recursive domain
-equation, as it is self-referential under the guard of [â–¶ ].
-
-The available functions on [proto] are:
-- [proto_map] which can be used to map the actions and the propositions of
-a given protocol.
-- [proto_app] which appends two protocols [p1] and [p2], by substituting
- all terminations in [p1] with [p2].*)
+(** This file defines the model of dependent separation protocols, along with
+various operations on the connective, such as append and map.
 
+Important: This file should not be used directly, but rather the wrappers in
+[proto_channel] should be used.
+
+Dependent separation protocols are designed with inspiration from session types,
+mimicking their constructors [!T.st], [?T.st] and [END], respectively,
+representing sending and receiving messages of type [T] and termination. The
+main difference is that the dependent separation protocols are defined over
+separation logic propositions, instead of types.
+
+Dependent Separation Protocols are modeled as the following type:
+
+[proto := 1 + (action * (V → (▶ proto → PROP) → PROP))]
+
+Here, the left-hand side of the sum is used for the terminated process, while
+the right-hand side is used for the communication constructors. The type
+[action] is an inductively defined datatype with two constructors [Send] and
+[Receive]. Compared to having an additional sum in [proto], this makes it
+possible to factorize the code in a better way.
+
+The remainder [V → (▶ [proto] → PROP) → PROP)] is a continuation that depends
+on the communicated value [V] and the dependent tail [▶ proto → PROP] from
+protocols guarded under laters to the propositions of the logic.
+
+The type [proto] is defined as a solution to a recursive domain equation, as
+it is self-referential under the guard of [â–¶].
+
+On top of the type [proto], we define the constructors:
+
+- [proto_end], which constructs the left-side of the sum.
+- [proto_msg], which takes an action and a continuation and constructs the
+  right-hand side of the sum accodingly.
+
+The defined functions on the type [proto] are:
+
+- [proto_map], which can be used to map the actions and the propositions of
+  a given protocol.
+- [proto_app], which appends two protocols [p1] and [p2], by substituting
+  all terminations [END] in [p1] with [p2]. *)
 From iris.base_logic Require Import base_logic.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import cofe_solver.
diff --git a/theories/examples/basics.v b/theories/examples/basics.v
index 1088d62b53181588f5b17a027961fd92e3fee4b0..789d5c3046e93857816f7dcf75cc2588287b0d72 100644
--- a/theories/examples/basics.v
+++ b/theories/examples/basics.v
@@ -1,6 +1,5 @@
-(** This file includes basic examples that each
-encapsulate a feature of the Dependent Separation Protocols.
-*)
+(** This file includes basic examples that each describe a unique feature of 
+dependent separation protocols. *)
 From actris.channel Require Import proto_channel proofmode.
 From iris.heap_lang Require Import proofmode notation lib.spin_lock.
 From actris.utils Require Import contribution.
@@ -10,12 +9,12 @@ Definition prog1 : val := λ: <>,
   let: "c" := start_chan (λ: "c'", send "c'" #42) in
   recv "c".
 
-(** References *)
+(** Tranfering References *)
 Definition prog2 : val := λ: <>,
   let: "c" := start_chan (λ: "c'", send "c'" (ref #42)) in
   ! (recv "c").
 
-(** Delegation *)
+(** Delegation, i.e. transfering channels *)
 Definition prog3 : val := λ: <>,
   let: "c1" := start_chan (λ: "c1'",
     let: "cc2" := new_chan #() in
@@ -23,14 +22,14 @@ Definition prog3 : val := λ: <>,
     send (Snd "cc2") #42) in
   recv (recv "c1").
 
-(** Dependent Behaviour *)
+(** Dependent protocols *)
 Definition prog4 : val := λ: <>,
   let: "c" := start_chan (λ: "c'",
     let: "x" := recv "c'" in send "c'" ("x" + #2)) in
   send "c" #40;;
   recv "c".
 
-(** Higher-Order *)
+(** Transfering higher-order functions *)
 Definition prog5 : val := λ: <>,
   let: "c" := start_chan (λ: "c'",
     let: "f" := recv "c'" in send "c'" (λ: <>, "f" #() + #2)) in
@@ -38,7 +37,7 @@ Definition prog5 : val := λ: <>,
   send "c" (λ: <>, !"r");;
   recv "c" #().
 
-(** Locks *)
+(** Lock protected channel endpoints *)
 Definition prog_lock : val := λ: <>,
   let: "c" := start_chan (λ: "c'",
     let: "l" := newlock #() in
@@ -49,7 +48,7 @@ Definition prog_lock : val := λ: <>,
 Section proofs.
 Context `{heapG Σ, proto_chanG Σ}.
 
-(** Protocols for their respective programs *)
+(** Protocols for the respective programs *)
 Definition prot1 : iProto Σ :=
   (<?> MSG #42; END)%proto.
 
@@ -75,7 +74,7 @@ Fixpoint prot_lock (n : nat) : iProto Σ :=
   | S n' => <?> MSG #21; prot_lock n'
   end%proto.
 
-(** Specs and proofs of their respective programs *)
+(** Specs and proofs of the respective programs *)
 Lemma prog1_spec : {{{ True }}} prog1 #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
diff --git a/theories/examples/map.v b/theories/examples/map.v
index 7a446714beb7f91060ca96d536ac97b54e723e01..7bd7d6ecfd8b19dc1249f1765e76da4c4c4db0e7 100644
--- a/theories/examples/map.v
+++ b/theories/examples/map.v
@@ -1,10 +1,11 @@
-(** This file implements a distributed map service,
-a specification thereof and its proofs. *)
+(** This file implements a distributed mapper service, a specification thereof,
+and its proofs. *)
 From actris.channel Require Import proto_channel proofmode.
 From iris.heap_lang Require Import proofmode notation lib.spin_lock.
 From actris.utils Require Import llist contribution.
 From iris.algebra Require Import gmultiset.
 
+(** * Distributed version (aka the implementation) *)
 Definition par_map_worker : val :=
   rec: "go" "map" "l" "c" :=
     acquire "l";;
@@ -51,6 +52,7 @@ Definition par_map_client : val := λ: "n" "map" "xs",
   par_map_client_loop "n" "c" "xs" "ys";;
   lapp "xs" "ys".
 
+(** * Correctness proofs of the distributed version *)
 Class mapG Σ A `{Countable A} := {
   map_contributionG :> contributionG Σ (gmultisetUR A);
   map_lockG :> lockG Σ;
diff --git a/theories/examples/map_reduce.v b/theories/examples/map_reduce.v
index b69df0464b70f8a679c96aca4756c5db0d322f3d..5b1601123408f53df4a712ee2ec5492f8c12f88d 100644
--- a/theories/examples/map_reduce.v
+++ b/theories/examples/map_reduce.v
@@ -1,18 +1,18 @@
-(** This file implements a map-reduce program,
-a specification thereof and its proofs. *)
+(** This file implements a simple distributed map-reduce function, a
+specification thereof, and its proofs. *)
 From actris.channel Require Import proto_channel proofmode.
 From iris.heap_lang Require Import proofmode notation.
 From actris.utils Require Import llist compare contribution group.
 From actris.examples Require Import map sort_fg.
 From iris.algebra Require Import gmultiset.
 
-(** Functional version of map reduce (aka the specification) *)
+(** * Functional version of map reduce (aka the specification) *)
 Definition map_reduce {A B C} `{EqDecision K}
     (map : A → list (K * B)) (red : K → list B → list C) : list A → list C :=
   mbind (curry red) ∘ group ∘ mbind map.
 Instance: Params (@map_reduce) 7 := {}.
 
-(** Distributed version *)
+(** * Distributed version (aka the implementation) *)
 Definition par_map_reduce_map : val :=
   rec: "go" "n" "cmap" "csort" "xs" :=
     if: "n" = #0 then #() else
@@ -72,7 +72,7 @@ Definition par_map_reduce : val := λ: "n" "m" "map" "red" "xs",
   par_map_reduce_reduce "m" "csort" "cred" (SOME "jy") "xs".
 
 
-(** Properties about the functional version *)
+(** * Properties about the functional version *)
 Section map_reduce.
   Context {A B C} `{EqDecision K} (map : A → list (K * B)) (red : K → list B → list C).
   Context `{!∀ j, Proper ((≡ₚ) ==> (≡ₚ)) (red j)}.
@@ -89,7 +89,7 @@ Section map_reduce.
   Proof. intros xs1 xs2 Hxs. by rewrite /map_reduce /= Hxs. Qed.
 End map_reduce.
 
-(** Correctness proofs of the distributed version *)
+(** * Correctness proofs of the distributed version *)
 Class map_reduceG Σ A B `{Countable A, Countable B} := {
   map_reduce_mapG :> mapG Σ A;
   map_reduce_reduceG :> mapG Σ (Z * list B);
diff --git a/theories/examples/sort.v b/theories/examples/sort.v
index 1cd272b9c41656de834ca4acbcc1830b76a1c042..66ed64e7bf62ace1875a99523236c4ce7ffab7f2 100644
--- a/theories/examples/sort.v
+++ b/theories/examples/sort.v
@@ -1,7 +1,10 @@
-(** This file implements a distributed Merge Sort,
-a specification thereof and its proofs, including
-a variant in which the comparison function is sent
-over the channel. *)
+(** This file implements a distributed version of merge sort, a specification
+thereof, and its proofs. There are two variants:
+
+- [sort_service]: a service that takes both a comparison function and a channel
+  as its arguments.
+- [sort_service_func]: a service that only takes a channel as its argument. The
+  comparison function is sent over the channel. *)
 From stdpp Require Import sorting.
 From actris.channel Require Import proto_channel proofmode.
 From iris.heap_lang Require Import proofmode notation.
diff --git a/theories/examples/sort_br_del.v b/theories/examples/sort_br_del.v
index 68670d74ac44e7d2a6a8c402283cc76373e974f5..7666bff72b3ce6e3b6409bc259bd599e1f632524 100644
--- a/theories/examples/sort_br_del.v
+++ b/theories/examples/sort_br_del.v
@@ -1,5 +1,12 @@
-(** This file implements a looping distributed Merge Sort,
-a specification thereof and its proofs. *)
+(** This file provides three wrappers around the distributed version of merge
+sort, demonstrating Actris's support for delegation and branching:
+
+- [sort_service_br]: a service that allows one to sort a series of lists in 
+  sequence. 
+- [sort_service_del]: a service that allows one to sort a series of lists in
+  parallel by delegating a sort service for a single list to a new channel.
+- [sort_service_br_del]: a service that allows one to sort a series of list by
+  forking itself. *)
 From stdpp Require Import sorting.
 From actris.channel Require Import proto_channel proofmode.
 From iris.heap_lang Require Import proofmode notation.
diff --git a/theories/examples/sort_fg.v b/theories/examples/sort_fg.v
index 410f929371fe7b6982515dac314ab54a556a217a..6612052d7ded31322336d3a49a98f9edfa810a96 100644
--- a/theories/examples/sort_fg.v
+++ b/theories/examples/sort_fg.v
@@ -1,5 +1,7 @@
-(** This file implements a fine-grained Merge Sort,
-a specification thereof and its proofs. *)
+(** This file implements a "fine-grained" distributed version of merge sort, a
+specification thereof, and its proofs. We call this version fine-grained because
+the lists are not transmitted using a single message, but using a series of
+messages. *)
 From stdpp Require Export sorting.
 From actris.channel Require Import proto_channel proofmode.
 From iris.heap_lang Require Import proofmode notation.
diff --git a/theories/utils/auth_excl.v b/theories/utils/auth_excl.v
index 5c7691f7583f8f735627cf0ff59744e16b09e0f1..a8a9e5588fbb7b294776b11b60d37f1cf169ae6a 100644
--- a/theories/utils/auth_excl.v
+++ b/theories/utils/auth_excl.v
@@ -1,11 +1,5 @@
-(** This file provides utility for defining and using
-a commonly used ghost functor over authoritative exclusive ownership.
-[AuthExcl A := Auth (Option (Excl A))]
-
-This is isomorphic to a half-ownership, with an intuitive
-use-case, being putting the authoritative part in an
-invariant, while giving the other fragment to the client
-with write permissions.  *)
+(** This file provides some utilities for the commonly used camera of
+authoritative exclusive ownership, [auth (option (excl A))]. *)
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import excl auth.
 From iris.base_logic.lib Require Import own.
diff --git a/theories/utils/compare.v b/theories/utils/compare.v
index dc19a1da230d9cebdddc6b98dc55f625a8b4f6fc..909604a96c6c8142535d07bb274acf3bb5300066 100644
--- a/theories/utils/compare.v
+++ b/theories/utils/compare.v
@@ -1,7 +1,7 @@
-(** This file includes a definition and specification
-for comparing values based on a given interpretation [I]
-and a relation [R], along with an implementation in the [heap_lang]
-language, given the [≤] relation.*)
+(** This file includes a specification [cmp_spec] for comparing values based on
+a given interpretation [I], a relation [R] that matches up with a HeapLang
+implementation [cmp]. The file also provides an instance for the [≤] relation
+on integers [Z].*)
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
 
diff --git a/theories/utils/contribution.v b/theories/utils/contribution.v
index 496150ec7b1ebb0eb7fd88dda8548475ff916a07..ab48460002e95a9f6d012ffef7eb632b58be5b50 100644
--- a/theories/utils/contribution.v
+++ b/theories/utils/contribution.v
@@ -1,17 +1,20 @@
-(** This file defines a ghost functor for tracking
-"contributions" made to a shared concurrent effort.
-It is ultimately defined as:
-[contribution := Auth (Option ((Pos * A) + Excl 1))]
-
-Intuitively it allows one to allocate a [server γ n v] and a
-number of [client γ v] fragments that can each hold resources.
-The intended use is to allocate a client for each thread that
-contributes to a channel endpoint, where the resources [v] are
-things that are currently owned by the thread, that is later
-used in the protocol.
-
-The server keeps track of the number of active clients [n],
-and what resources they are currently holding [v].*)
+(** This file defines the "authoritative contribution ghost theory" for tracking
+contributions made by clients towards a shared concurrent effort. Compared to
+the paper, the construction is defined over a user-given carrier camera [A],
+instead of multisets.
+
+This ghost theory construction exposes two connectives:
+
+- [server γ n v]: keeps track of the number of active clients [n] and the total
+  amount of resources hold by all clients [x : A].
+- [client γ x]: keeps track of the resources [x : A] hold by a single client.
+
+The intended use case is to allocate a [client] for each thread that contributes
+to a channel endpoint, where the resources [x] are owned by the thread, that is
+later used in the protocol.
+
+To model this ghost theory construction, we use the camera
+[auth (option (csum (positive * A) (excl unit)))]. *)
 From iris.base_logic Require Export base_logic lib.iprop lib.own.
 From iris.proofmode Require Export tactics.
 From iris.algebra Require Import excl auth csum gmultiset frac_auth.
diff --git a/theories/utils/group.v b/theories/utils/group.v
index 15490997feae760dbeecfc5e6e84a2450690a7b4..92791a593a59151e0cc54b890a10e310c14bca24 100644
--- a/theories/utils/group.v
+++ b/theories/utils/group.v
@@ -1,5 +1,5 @@
-(** This file provides utility for grouping elements
-based on keys. *)
+(** This file provides utility functions for grouping association lists based on
+their keys, as well as basic theorems about them. *)
 From stdpp Require Export prelude.
 From Coq Require Export SetoidPermutation.
 
diff --git a/theories/utils/llist.v b/theories/utils/llist.v
index d710ab054d77f85a5ae1a2e66bddeead1c88bab6..dcce8a7e39170a40e3ff76a28794b9dd563fbb05 100644
--- a/theories/utils/llist.v
+++ b/theories/utils/llist.v
@@ -1,9 +1,10 @@
-(** This file defines an encoding of lists in the [heap_lang]
-language, along with common functions such as append and split. *)
+(** This file defines a separation logic representation predicates [llist] for
+mutable linked-lists. It comes with a small library of operations (head, pop,
+lookup, length, append, prepend, snoc, split). *)
 From iris.heap_lang Require Export proofmode notation.
 From iris.heap_lang Require Import assert.
 
-(** Immutable ML-style functional lists *)
+(**  *)
 Fixpoint llist `{heapG Σ} {A} (I : A → val → iProp Σ)
     (l : loc) (xs : list A) : iProp Σ :=
   match xs with