diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index fdca205b09b3becd2ae749c2e0719655080c1eac..7cd0f222eb35e32777e1a9754c206791e62ec4cd 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -1,3 +1,21 @@
+(** This file contains the definition of the Channel language encoding,
+being a pair of buffers, with the three message-passing primitives
+[new_chan], [send] and [receive], along with their respective specifications.
+
+The abstract representation of a channel endpoint is two buffer references
+and a lock. [new_chan] creates references to two empty buffers and a lock, and
+returns a pair of such endpoints, where the order of the two references
+determines the polarity of the endpoints.
+
+The [send] primitive takes such an endpoint abstraction and adds an element to
+the first buffer under the lock. Conversely [recv] loops until there is
+something in the second, locking during each peek.
+
+The specifications are defined in terms of the logical connectives [is_chan]
+and [chan_own], which respectively determines the contents of a channel and
+the ownership of it.
+*)
+
 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.
@@ -9,6 +27,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 *)
 Definition new_chan : val :=
   λ: <>,
      let: "l" := lnil #() in
@@ -39,6 +58,7 @@ Definition recv : val :=
     | NONE => "go" "c"
     end.
 
+(** Channel ghost functor *)
 Class chanG Σ := {
   chanG_lockG :> lockG Σ;
   chanG_authG :> auth_exclG (listO valO) Σ;
@@ -65,6 +85,7 @@ Section channel.
     chan_r_name : gname
   }.
 
+  (** The invariant of channels *)
   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) ∗
@@ -79,6 +100,18 @@ Section channel.
   Global Instance is_chan_persistent : Persistent (is_chan γ c1 c2).
   Proof. by apply _. Qed.
 
+  Lemma chan_inv_alt s γ l r :
+    chan_inv γ l r ⊣⊢ ∃ ls rs,
+      llist sbi_internal_eq (side_elim s l r) ls ∗
+      own (side_elim s chan_l_name chan_r_name γ) (● to_auth_excl ls) ∗
+      llist sbi_internal_eq (side_elim s r l) rs ∗
+      own (side_elim s chan_r_name chan_l_name γ) (● to_auth_excl rs).
+  Proof.
+    destruct s; rewrite /chan_inv //=.
+    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.
 
@@ -94,9 +127,9 @@ Section channel.
     wp_lam.
     wp_apply (lnil_spec with "[//]"); iIntros (l) "Hl".
     wp_apply (lnil_spec with "[//]"); iIntros (r) "Hr".
-    iMod (own_alloc (● (to_auth_excl []) ⋅ ◯ (to_auth_excl []))) as (lsγ) "[Hls Hls']".
+    iMod (own_alloc (● (to_auth_excl [])  ◯ (to_auth_excl []))) as (lsγ) "[Hls Hls']".
     { by apply auth_both_valid. }
-    iMod (own_alloc (● (to_auth_excl []) ⋅ ◯ (to_auth_excl []))) as (rsγ) "[Hrs Hrs']".
+    iMod (own_alloc (● (to_auth_excl [])  ◯ (to_auth_excl []))) as (rsγ) "[Hrs Hrs']".
     { by apply auth_both_valid. }
     wp_apply (newlock_spec N (∃ ls rs,
       llist sbi_internal_eq l ls ∗ own lsγ (● to_auth_excl ls) ∗
@@ -107,17 +140,6 @@ Section channel.
     rewrite /chan_inv /=. eauto 20 with iFrame.
   Qed.
 
-  Lemma chan_inv_alt s γ l r :
-    chan_inv γ l r ⊣⊢ ∃ ls rs,
-      llist sbi_internal_eq (side_elim s l r) ls ∗
-      own (side_elim s chan_l_name chan_r_name γ) (● to_auth_excl ls) ∗
-      llist sbi_internal_eq (side_elim s r l) rs ∗
-      own (side_elim s chan_r_name chan_l_name γ) (● to_auth_excl rs).
-  Proof.
-    destruct s; rewrite /chan_inv //=.
-    iSplit; iDestruct 1 as (ls rs) "(?&?&?&?)"; iExists rs, ls; iFrame.
-  Qed.
-
   Lemma send_spec Φ E γ c1 c2 v s :
     is_chan γ c1 c2 -∗
     (|={⊤,E}=> ∃ vs,
@@ -194,4 +216,5 @@ 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 ea2a2e8af662bd0ee7b527c6e8a37df41b2236ae..969b503308edca030343323c8c3e302776582023 100644
--- a/theories/channel/proofmode.v
+++ b/theories/channel/proofmode.v
@@ -1,3 +1,11 @@
+(** 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.
+ *)
 From iris.heap_lang Require Export proofmode notation.
 From iris.proofmode Require Export tactics.
 From actris Require Export proto_channel.
diff --git a/theories/channel/proto_channel.v b/theories/channel/proto_channel.v
index 5a02c3ca944b668bdce6d9599877792f2663ade8..0d9033497fad8c5dc6f4142222ab2a7e9dd2c608 100644
--- a/theories/channel/proto_channel.v
+++ b/theories/channel/proto_channel.v
@@ -1,3 +1,22 @@
+(** This file contains the instantiation of the
+Dependent Separation Protocols with the encoded messages.
+For starters this means fixing the types of message to the
+language value type [val] and the logic to the iris logic [iProp Σ].
+
+It then defines a convenient way of constructing instances of the type
+via [iProto_end] and [iProto_message] with associated notation,
+as well as type-specific variants of [dual] and [append].
+An encoding of branching behaviour is additionally included, defined
+in terms of sending and receiving boolean flags, along with relevant notation.
+
+The logical connectives of protocol ownership [c >-> prot] are then defined.
+This is achieved through Iris invariants and ghost state along with the
+logical connectives of the channel encodings. 
+
+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.
diff --git a/theories/channel/proto_model.v b/theories/channel/proto_model.v
index 41af2dec95ebbe37a53c2c3a6fb46b98cb42e7c4..c9600aa9a588e6c01a952da6e1260f6f0e6783f7 100644
--- a/theories/channel/proto_model.v
+++ b/theories/channel/proto_model.v
@@ -1,3 +1,23 @@
+(** This file defines the model of Dependent Separation Protocols,
+along with various operations on the connective, such as append
+and map.
+
+Dependent Separation Protocols can ultimately be expressed as:
+proto := 1 + (B * (V -> (â–¶ proto -> PROP) -> PROP))
+
+Here the left-hand side of the sum is the terminal protocol
+[proto_end], while the right-hand side is [proto_message],
+where B is the canonical representation of actions determining
+whether the protocol sends or receives, and
+(V -> (â–¶ proto -> PROP) -> PROP) is a continuation that
+depends on a communicated value V and the dependent tail
+(â–¶ proto -> PROP) from protocols guarded under laters,
+ to the propositions of the logic.
+
+The type is defined as a solution to a recursive domain
+equation, as it is self-referential under the guard of â–¶.
+*)
+
 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 b1f8784a676a95119f5ff7999ff847f07f3f1802..1088d62b53181588f5b17a027961fd92e3fee4b0 100644
--- a/theories/examples/basics.v
+++ b/theories/examples/basics.v
@@ -1,15 +1,21 @@
+(** This file includes basic examples that each
+encapsulate a feature of the 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.
 
+(** Basic *)
 Definition prog1 : val := λ: <>,
   let: "c" := start_chan (λ: "c'", send "c'" #42) in
   recv "c".
 
+(** References *)
 Definition prog2 : val := λ: <>,
   let: "c" := start_chan (λ: "c'", send "c'" (ref #42)) in
   ! (recv "c").
 
+(** Delegation *)
 Definition prog3 : val := λ: <>,
   let: "c1" := start_chan (λ: "c1'",
     let: "cc2" := new_chan #() in
@@ -17,12 +23,14 @@ Definition prog3 : val := λ: <>,
     send (Snd "cc2") #42) in
   recv (recv "c1").
 
+(** Dependent Behaviour *)
 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 *)
 Definition prog5 : val := λ: <>,
   let: "c" := start_chan (λ: "c'",
     let: "f" := recv "c'" in send "c'" (λ: <>, "f" #() + #2)) in
@@ -30,6 +38,7 @@ Definition prog5 : val := λ: <>,
   send "c" (λ: <>, !"r");;
   recv "c" #().
 
+(** Locks *)
 Definition prog_lock : val := λ: <>,
   let: "c" := start_chan (λ: "c'",
     let: "l" := newlock #() in
@@ -40,6 +49,7 @@ Definition prog_lock : val := λ: <>,
 Section proofs.
 Context `{heapG Σ, proto_chanG Σ}.
 
+(** Protocols for their respective programs *)
 Definition prot1 : iProto Σ :=
   (<?> MSG #42; END)%proto.
 
@@ -65,6 +75,7 @@ Fixpoint prot_lock (n : nat) : iProto Σ :=
   | S n' => <?> MSG #21; prot_lock n'
   end%proto.
 
+(** Specs and proofs of their 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 5cafc7fe16ef5ff26cb09586c7320df1583e4473..7a446714beb7f91060ca96d536ac97b54e723e01 100644
--- a/theories/examples/map.v
+++ b/theories/examples/map.v
@@ -1,3 +1,5 @@
+(** This file implements a distributed map 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.
diff --git a/theories/examples/map_reduce.v b/theories/examples/map_reduce.v
index 903a017b6814cbe08944edc1409b29d43c831b09..a14aa347e8d95aaa2df2c94735cab7f814e5d3ec 100644
--- a/theories/examples/map_reduce.v
+++ b/theories/examples/map_reduce.v
@@ -1,3 +1,5 @@
+(** This file implements a map-reduce program,
+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.
diff --git a/theories/examples/sort.v b/theories/examples/sort.v
index 5860079210d0e333fd7f3afdbf57d170c865d7df..c096a665efbb988a0254cecc5582bd03caca04b8 100644
--- a/theories/examples/sort.v
+++ b/theories/examples/sort.v
@@ -1,3 +1,5 @@
+(** This file implements a distributed Merge Sort,
+a specification thereof and its proofs. *)
 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 296e1b42ae2d5b009333026a51aca17786944ae7..68670d74ac44e7d2a6a8c402283cc76373e974f5 100644
--- a/theories/examples/sort_br_del.v
+++ b/theories/examples/sort_br_del.v
@@ -1,3 +1,5 @@
+(** This file implements a looping distributed Merge Sort,
+a specification thereof and its proofs. *)
 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 bc5edc7e9e16d36b9ef557ee618bb086d0d4740a..410f929371fe7b6982515dac314ab54a556a217a 100644
--- a/theories/examples/sort_fg.v
+++ b/theories/examples/sort_fg.v
@@ -1,3 +1,5 @@
+(** This file implements a fine-grained Merge Sort,
+a specification thereof and its proofs. *)
 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 f9a5871a79f0f5020d9fab76a02779f80a42d31f..952adadce11fd59ad810e593875d308ab1e7086d 100644
--- a/theories/utils/auth_excl.v
+++ b/theories/utils/auth_excl.v
@@ -1,3 +1,5 @@
+(** This file provides utility for defining and using
+the commonly used ghost functor over authoritative exclusive ownership. *)
 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 422bf77ffc6cad3b42754592f8f5308ac65ddf93..dc19a1da230d9cebdddc6b98dc55f625a8b4f6fc 100644
--- a/theories/utils/compare.v
+++ b/theories/utils/compare.v
@@ -1,3 +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.*)
 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 c221ed56d33aeaa569d0cc85da58a432972b5a87..15cb3efd783a0f2c1c094f1bfb63920d9f6f8549 100644
--- a/theories/utils/contribution.v
+++ b/theories/utils/contribution.v
@@ -1,3 +1,15 @@
+(** 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] and
+a number of [client] fragments. The server keeps track
+of the number of active clients, and what resources they
+are currently holding.
+To deallocate a client it must hold no resources.
+To deallocate a server there must be no remaining clients.
+*)
 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 90c86fa70760c104566012604b20dd53a4f609e9..9b3b0b0a715fd424e782a339db46db78ad3acf75 100644
--- a/theories/utils/group.v
+++ b/theories/utils/group.v
@@ -1,3 +1,5 @@
+(** This file provides utility for grouping elements
+based on keys. *)
 From stdpp Require Export prelude.
 From Coq Require Export SetoidPermutation.
 
diff --git a/theories/utils/llist.v b/theories/utils/llist.v
index a948859050c307cce4ce8875a96d619c14e5707b..d710ab054d77f85a5ae1a2e66bddeead1c88bab6 100644
--- a/theories/utils/llist.v
+++ b/theories/utils/llist.v
@@ -1,3 +1,5 @@
+(** This file defines an encoding of lists in the [heap_lang]
+language, along with common functions such as append and split. *)
 From iris.heap_lang Require Export proofmode notation.
 From iris.heap_lang Require Import assert.