diff --git a/README.md b/README.md
index 66f49670d8fd46511c04e24a1e120296ad5cceec..befa2f077d5984b02038ea7a61fe1965cc08e072 100644
--- a/README.md
+++ b/README.md
@@ -4,6 +4,12 @@ This repository contains the main Coq specification & proof development of the [
 
 <center><img alt="RT-Proofs logo" src="http://prosa.mpi-sws.org/figures/rt-proofs-logo.png" width="300px"></center>
 
+## Documentation
+
+Up-to-date documentation for all branches of the main Prosa repository is available on the Prosa homeage:
+
+- <https://prosa.mpi-sws.org/branches>
+
 ## Publications
 
 Please see the [list of publications](http://prosa.mpi-sws.org/documentation.html#publications) on the Prosa project's homepage. 
@@ -46,11 +52,6 @@ Second, compile the library.
 make -j
 ```
 
-## Documentation
-
-Up-to-date documentation for all branches of the main Prosa repository is available at <https://prosa.mpi-sws.org/branches>.
-
-
 ## Generating HTML Documentation
 
 The Coqdoc documentation (as shown on the [webpage](http://prosa.mpi-sws.org/documentation.html)) can be easily generated with the provided `Makefile`:
diff --git a/restructuring/behavior/arrival_sequence.v b/restructuring/behavior/arrival_sequence.v
index 976c01568bee1e3ce6e6546d743a929c5a73776b..6f913ff30412c21be5ae646e2d4f9c2c8e1afa3b 100644
--- a/restructuring/behavior/arrival_sequence.v
+++ b/restructuring/behavior/arrival_sequence.v
@@ -2,7 +2,10 @@ From mathcomp Require Export ssreflect seq ssrnat ssrbool bigop eqtype ssrfun.
 From rt.restructuring.behavior Require Export time job.
 From rt.util Require Import notation.
 
-(** Definitions and properties of job arrival sequences. *)
+(** This module contains basic definitions and properties of job arrival
+    sequences. *)
+
+(** * Notion of an Arrival Sequence *)
 
 (** We begin by defining a job arrival sequence. *)
 Section ArrivalSequence.
@@ -15,6 +18,8 @@ Section ArrivalSequence.
 
 End ArrivalSequence.
 
+(** * Arrival of a Job *)
+
 (** Next, we define properties of jobs in a given arrival sequence. *)
 Section JobProperties.
 
@@ -35,6 +40,8 @@ Section JobProperties.
 
 End JobProperties.
 
+(** * Validity of an Arrival Sequence *)
+
 (** Next, we define valid arrival sequences. *)
 Section ValidArrivalSequence.
 
@@ -62,6 +69,8 @@ Section ValidArrivalSequence.
 
 End ValidArrivalSequence.
 
+(** * Arrival Time Predicates *)
+
 (** Next, we define properties of job arrival times. *)
 Section ArrivalTimeProperties.
 
@@ -86,6 +95,8 @@ Section ArrivalTimeProperties.
 
 End ArrivalTimeProperties.
 
+(** * Finite Arrival Sequence Prefixes *)
+
 (** In this section, we define arrival sequence prefixes, which are useful to
    define (computable) properties over sets of jobs in the schedule. *)
 Section ArrivalSequencePrefix.
diff --git a/restructuring/behavior/job.v b/restructuring/behavior/job.v
index 26ae4c6fc02a0e3bd72043a39116360aef17589a..6a152ccbb076b9fb5f088ce8cc2eb83ff624c092 100644
--- a/restructuring/behavior/job.v
+++ b/restructuring/behavior/job.v
@@ -1,13 +1,19 @@
 From rt.restructuring.behavior Require Export time.
 From mathcomp Require Export eqtype ssrnat.
 
+(** * Notion of a Job Type *)
+
 (** Throughout the library we assume that jobs have decidable equality. *)
 Definition JobType := eqType.
 
+(** * Unit of Work *)
+
 (** We define 'work' to denote the unit of service received or needed. In a
    real system, this corresponds to the number of processor cycles. *)
 Definition work  := nat.
 
+(** * Basic Job Parameters — Cost, Arrival Time, and Absolute Deadline *)
+
 (** Definition of a generic type of parameter relating jobs to a discrete cost. *)
 Class JobCost (Job : JobType) := job_cost : Job -> work.
 
diff --git a/restructuring/behavior/ready.v b/restructuring/behavior/ready.v
index a2a5d2ee337b836e87c494b481a206994fd91766..30587b082db0960302f4ff6142c82260eda01d92 100644
--- a/restructuring/behavior/ready.v
+++ b/restructuring/behavior/ready.v
@@ -1,6 +1,7 @@
 From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
 From rt.restructuring.behavior Require Export service.
 
+(** * Readiness of a Job *)
 
 (** We define a general notion of readiness of a job: a job can be
    scheduled only when it is ready, as determined by the predicate
@@ -19,6 +20,8 @@ Class JobReady (Job : JobType) (PState : Type)
     _ : forall sched j t, job_ready sched j t -> pending sched j t;
   }.
 
+(** * Backlogged Jobs *)
+
 (** Based on the general notion of readiness, we define what it means to be
    backlogged, i.e., ready to run but not executing. *)
 Section Backlogged.
@@ -36,9 +39,11 @@ Section Backlogged.
 End Backlogged.
 
 
+(** * Validity of a Schedule *)
+
 (** With the readiness concept in place, we define the notion of valid schedules. *)
 Section ValidSchedule.
-  (** Consider any kinds of jobs and any kind of processor state. *)
+  (** Consider any kind of jobs and any kind of processor state. *)
   Context {Job : JobType} {PState : Type}.
   Context `{ProcessorState Job PState}.
 
diff --git a/restructuring/behavior/schedule.v b/restructuring/behavior/schedule.v
index ea6e9174946298ff8d79a7c04b0c6b993ae22278..2958f8754e8a31456997309092e9017e891f14a9 100644
--- a/restructuring/behavior/schedule.v
+++ b/restructuring/behavior/schedule.v
@@ -1,10 +1,24 @@
 From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
 From rt.restructuring.behavior Require Export arrival_sequence.
 
-(** We define the notion of a generic processor state. The processor state type
-   determines aspects of the execution environment are modeled (e.g., overheads, spinning).
-   In the most simple case (i.e., Ideal.processor_state), at any time,
-   either a particular job is either scheduled or it is idle. *)
+(** * Generic Processor State *)
+
+(** Rather than choosing a specific schedule representation up front, we define
+    the notion of a generic processor state, which allows us to state general
+    definitions of core concepts (such as "how much service has a job
+    received") that work across many possble scenarios (e.g., ideal
+    uniprocessor schedules, schedules with overheads, variable-speed
+    processors, multiprocessors, etc.).
+
+    A concrete processor state type precisely determines how all relevant
+    aspects of the execution environment are modeled (e.g., scheduled jobs,
+    overheads, spinning). Here, we define just the common interface of all
+    possible concrete processor states by means of a "type class", i.e., we
+    define a few generic predicates and an invariant that must be defined by
+    all concrete processor state types.
+
+    In the most simple case (i.e., an ideal uniprocessor state), at any time,
+    either a particular job is scheduled or the processor is idle. *)
 Class ProcessorState (Job : JobType) (State : Type) :=
   {
     (** A [ProcessorState] instance provides a finite set of cores on which
@@ -31,7 +45,13 @@ Class ProcessorState (Job : JobType) (State : Type) :=
       forall j s, ~~ scheduled_in j s -> service_in j s = 0
   }.
 
-(** A schedule maps an instant to a processor state *)
+(** * Schedule Representation *)
+
+(** In Prosa, schedules are represented as functions, which allows us to model
+    potentially infinite schedules. More specifically, a schedule simply maps
+    each instant to a processor state, which reflects state of the computing
+    platform at the specific time (e.g., which job is presently scheduled). *)
+
 Definition schedule (PState : Type) := instant -> PState.
 
 (** The following line instructs Coq to not let proofs use knowledge of how
diff --git a/restructuring/behavior/service.v b/restructuring/behavior/service.v
index e42f353ef4d4b04c4b11fb44bfdfc2e588a4bfe3..24bc0151def904392a68f6c920b3a9a5f9ecd676 100644
--- a/restructuring/behavior/service.v
+++ b/restructuring/behavior/service.v
@@ -2,58 +2,69 @@ From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
 From rt.restructuring.behavior Require Export schedule.
 
 Section Service.
+
+  (** * Service of a Job *)
+
+  (** Consider any kind of jobs and any kind of processor state. *)
   Context {Job : JobType} {PState : Type}.
   Context `{ProcessorState Job PState}.
 
+  (** Consider any schedule. *)
   Variable sched : schedule PState.
 
-  (** First, we define whether a job j is scheduled at time t, ... *)
+  (** First, we define whether a job [j] is scheduled at time [t], ... *)
   Definition scheduled_at (j : Job) (t : instant) := scheduled_in j (sched t).
 
-  (** ... and the instantaneous service received by
-           job j at time t. *)
+  (** ... and the instantaneous service received by job j at time t. *)
   Definition service_at (j : Job) (t : instant) := service_in j (sched t).
 
-  (** Based on the notion of instantaneous service, we define the
-           cumulative service received by job j during any interval [t1, t2). *)
+  (** Based on the notion of instantaneous service, we define the cumulative
+      service received by job j during any interval from [t1] until (but not
+      including) [t2]. *)
   Definition service_during (j : Job) (t1 t2 : instant) :=
     \sum_(t1 <= t < t2) service_at j t.
 
-  (** Using the previous definition, we define the cumulative service
-           received by job j up to time t, i.e., during interval [0, t). *)
+  (** Using the previous definition, we define the cumulative service received
+      by job [j] up to (but not including) time [t]. *)
   Definition service (j : Job) (t : instant) := service_during j 0 t.
 
+  (** * Job Completion and Response Time *)
+
+  (** In the following, consider jobs that have a cost, a deadline, and an
+      arbitrary arrival time. *)
   Context `{JobCost Job}.
   Context `{JobDeadline Job}.
   Context `{JobArrival Job}.
 
-  (** Next, we say that job j has completed by time t if it received enough
-           service in the interval [0, t). *)
+  (** We say that job [j] has completed by time [t] if it received all required
+      service in the interval from [0] until (but not including) [t]. *)
   Definition completed_by (j : Job) (t : instant) := service j t >= job_cost j.
 
-  (** We say that job j completes at time t if it has completed by time t but
-     not by time t - 1 *)
+  (** We say that job [j] completes at time [t] if it has completed by time [t] but
+      not by time [t - 1]. *)
   Definition completes_at (j : Job) (t : instant) := ~~ completed_by j t.-1 && completed_by j t.
 
-  (** We say that R is a response time bound of a job j if j has completed
-     by R units after its arrival *)
+  (** We say that a constant [R] is a response time bound of a job [j] if [j]
+      has completed by [R] units after its arrival. *)
   Definition job_response_time_bound (j : Job) (R : duration) :=
     completed_by j (job_arrival j + R).
 
-  (** We say that a job meets its deadline if it completes by its absolute deadline *)
+  (** We say that a job meets its deadline if it completes by its absolute deadline. *)
   Definition job_meets_deadline (j : Job) :=
     completed_by j (job_deadline j).
 
-  (** Job j is pending at time t iff it has arrived but has not yet completed. *)
+  (** * Pending or Incomplete Jobs *)
+
+  (** Job [j] is pending at time [t] iff it has arrived but has not yet completed. *)
   Definition pending (j : Job) (t : instant) := has_arrived j t && ~~ completed_by j t.
 
-  (** Job j is pending earlier and at time t iff it has arrived before time t
-           and has not been completed yet. *)
+  (** Job [j] is pending earlier and at time [t] iff it has arrived before time [t]
+      and has not been completed yet. *)
   Definition pending_earlier_and_at (j : Job) (t : instant) :=
     arrived_before j t && ~~ completed_by j t.
 
-  (** Let's define the remaining cost of job j as the amount of service
-     that has to be received for its completion. *)
+  (** Let's define the remaining cost of job [j] as the amount of service that
+      has yet to be received for it to complete. *)
   Definition remaining_cost j t :=
     job_cost j - service j t.
 
diff --git a/restructuring/behavior/time.v b/restructuring/behavior/time.v
index 662292c6f93135f27ff1182c9276d631f27a530f..54dd8b230189a797b8c7f3b3c2307595a19aeebd 100644
--- a/restructuring/behavior/time.v
+++ b/restructuring/behavior/time.v
@@ -1,4 +1,8 @@
-(** Time is defined as a natural number. *)
+(** * Model of Time *)
 
+(** Prosa is based on a discrete model of time. Thus, time is simply defined by
+    the natural numbers. To aid readability, we distinguish between time values
+    that represent durations and time values that represent specific
+    instants. *)
 Definition duration := nat.
 Definition instant  := nat.