diff --git a/restructuring/behavior/job.v b/restructuring/behavior/job.v
index 9743d13fcce92666006530cb689a1c22cf919385..8c28f72e84b8376713cd2184a0255858b2d78076 100644
--- a/restructuring/behavior/job.v
+++ b/restructuring/behavior/job.v
@@ -4,8 +4,12 @@ From mathcomp Require Export eqtype ssrnat.
 (* Throughout the library we assume that jobs have decidable equality. *)
 Definition JobType := eqType.
 
+(* 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.
+
 (* Definition of a generic type of parameter relating jobs to a discrete cost. *)
-Class JobCost (Job : JobType) := job_cost : Job -> duration.
+Class JobCost (Job : JobType) := job_cost : Job -> work.
 
 (* Definition of a generic type of parameter for job_arrival. *)
 Class JobArrival (Job : JobType) := job_arrival : Job -> instant.
diff --git a/restructuring/behavior/schedule.v b/restructuring/behavior/schedule.v
index b61d05cbd1e5122d32e55ab00d84fb14935e9a88..71d4153f5b8fef064a048ab9125a7ad4669983fc 100644
--- a/restructuring/behavior/schedule.v
+++ b/restructuring/behavior/schedule.v
@@ -12,7 +12,7 @@ Class ProcessorState (Job : JobType) (State : Type) :=
     scheduled_in: Job -> State -> bool;
     (* For a given processor state, the [service_in] function determines how much
        service a given job receives in that state. *)
-    service_in: Job -> State -> nat;
+    service_in: Job -> State -> work;
     (* For a given processor state, a job does not receive service if it is not scheduled
        in that state *)
     service_implies_scheduled :