diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index 7cd0f222eb35e32777e1a9754c206791e62ec4cd..e719e51066b0a495b67ca38d71eee1b7ee3c48e1 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -9,13 +9,14 @@ 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.
+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], which respectively determines the contents of a channel and
-the ownership of it.
+and [chan_own], which respectively determines the contents of a channel using
+a lock over an invariant and the ownership of it using ghost fragments
+over buffers.
 *)
-
 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.
diff --git a/theories/channel/proto_model.v b/theories/channel/proto_model.v
index c9600aa9a588e6c01a952da6e1260f6f0e6783f7..da6ebdff702c2f71ba67480f80da1c549c9da9d5 100644
--- a/theories/channel/proto_model.v
+++ b/theories/channel/proto_model.v
@@ -1,6 +1,6 @@
 (** This file defines the model of Dependent Separation Protocols,
 along with various operations on the connective, such as append
-and map.
+and map and the necessary typeclass instances.
 
 Dependent Separation Protocols can ultimately be expressed as:
 proto := 1 + (B * (V -> (â–¶ proto -> PROP) -> PROP))
@@ -10,9 +10,9 @@ Here the left-hand side of the sum is the terminal protocol
 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.
+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 is defined as a solution to a recursive domain
 equation, as it is self-referential under the guard of â–¶.
diff --git a/theories/examples/sort.v b/theories/examples/sort.v
index c096a665efbb988a0254cecc5582bd03caca04b8..ed59f992d31e48ac618cbdb1f652bb87b2730ee5 100644
--- a/theories/examples/sort.v
+++ b/theories/examples/sort.v
@@ -1,5 +1,7 @@
 (** This file implements a distributed Merge Sort,
-a specification thereof and its proofs. *)
+a specification thereof and its proofs, including
+a variant in which 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.