diff --git a/implementation/definitions/arrival_bound.v b/implementation/definitions/arrival_bound.v
new file mode 100644
index 0000000000000000000000000000000000000000..a4e9999ebbc7c0eb343bdaaab816fa67351f7fc6
--- /dev/null
+++ b/implementation/definitions/arrival_bound.v
@@ -0,0 +1,48 @@
+Require Export prosa.implementation.definitions.extrapolated_arrival_curve.
+
+(** * Implementation of a Task's Arrival Bound *)
+
+(** In this file, we define a reference implementation of the notion of a task's
+ arrival bound.
+
+ Note that its use is entirely optional: clients of Prosa may choose to use
+ this type or implement their own notion of arrival bounds. *)
+
+(** A task's arrival bound is an inductive type comprised of three types of
+ arrival patterns: (a) periodic, characterized by a period between consequent
+ activation of a task, (b) sporadic, characterized by a minimum inter-arrival
+ time, or (c) arrival-curve prefix, characterized by a finite prefix of an
+ arrival curve. *)
+Inductive task_arrivals_bound :=
+| Periodic : nat -> task_arrivals_bound
+| Sporadic : nat -> task_arrivals_bound
+| ArrivalPrefix : ArrivalCurvePrefix -> task_arrivals_bound.
+
+(** To make it compatible with ssreflect, we define a decidable
+ equality for arrival bounds. *)
+Definition task_arrivals_bound_eqdef (tb1 tb2 : task_arrivals_bound) :=
+ match tb1, tb2 with
+ | Periodic p1, Periodic p2 => p1 == p2
+ | Sporadic s1, Sporadic s2 => s1 == s2
+ | ArrivalPrefix s1, ArrivalPrefix s2 => s1 == s2
+ | _, _ => false
+ end.
+
+(** Next, we prove that [task_eqdef] is indeed an equality, ... *)
+Lemma eqn_task_arrivals_bound : Equality.axiom task_arrivals_bound_eqdef.
+Proof.
+ intros x y.
+ destruct (task_arrivals_bound_eqdef x y) eqn:EQ.
+ { apply ReflectT; destruct x, y.
+ all: try by move: EQ => /eqP EQ; subst.
+ }
+ { apply ReflectF; destruct x, y.
+ all: try by move: EQ => /eqP EQ.
+ all: by move: EQ => /neqP; intros NEQ1 NEQ2; apply NEQ1; inversion NEQ2.
+ }
+Qed.
+
+(** ..., which allows instantiating the canonical structure for [[eqType of task_arrivals_bound]]. *)
+Canonical task_arrivals_bound_eqMixin := EqMixin eqn_task_arrivals_bound.
+Canonical task_arrivals_bound_eqType := Eval hnf in EqType task_arrivals_bound task_arrivals_bound_eqMixin.
+
diff --git a/implementation/definitions/task.v b/implementation/definitions/task.v
new file mode 100644
index 0000000000000000000000000000000000000000..095daa5684db23a5423de5ae47f7c12862495528
--- /dev/null
+++ b/implementation/definitions/task.v
@@ -0,0 +1,131 @@
+Require Export prosa.implementation.definitions.arrival_bound.
+Require Export prosa.model.priority.numeric_fixed_priority.
+
+(** * Implementation of Tasks and Jobs *)
+
+(** This file provides reference implementations of the notions of "tasks" and
+ "jobs" that can be used to meet the hypotheses on which many of the analyses
+ in Prosa are based.
+
+ Note that their use is entirely optional: clients of Prosa may choose to use
+ these types or implement their own notions of "tasks" and "jobs". *)
+
+(** ** Implementation of a Concrete Task *)
+
+
+(** A task comprises of an id, a cost, an arrival bound, a deadline
+ and a priority. *)
+Structure concrete_task :=
+ { task_id: nat (* for uniqueness *)
+ ; task_cost: nat
+ ; task_arrival: task_arrivals_bound
+ ; task_deadline: instant
+ ; task_priority : nat
+ }.
+
+(** To make it compatible with ssreflect, we define a decidable
+ equality for concrete tasks. *)
+Definition task_eqdef (t1 t2: concrete_task) :=
+ (task_id t1 == task_id t2)
+ && (task_cost t1 == task_cost t2)
+ && (task_arrival t1 == task_arrival t2)
+ && (task_deadline t1 == task_deadline t2)
+ && (task_priority t1 == task_priority t2).
+
+(** Next, we prove that [task_eqdef] is indeed an equality, ... *)
+Lemma eqn_task : Equality.axiom task_eqdef.
+Proof.
+ unfold Equality.axiom; intros x y.
+ destruct (task_eqdef x y) eqn:EQ.
+ { apply ReflectT.
+ unfold task_eqdef in *.
+ move: EQ => /andP [/andP [/andP [/andP [/eqP ID /eqP COST] /eqP PER] /eqP DL] /eqP PRIO].
+ by destruct x, y; simpl in *; subst. }
+ { apply ReflectF.
+ unfold task_eqdef, not in * => BUG.
+ apply negbT in EQ.
+ repeat rewrite negb_and in EQ.
+ destruct x, y.
+ move: BUG => [ID COST PER DL PRIO].
+ rewrite ID COST PER DL PRIO //= in EQ.
+ by subst; rewrite !eq_refl in EQ.
+ }
+Qed.
+
+(** ..., which allows instantiating the canonical structure for [[eqType of concrete_task]]. *)
+Canonical concrete_task_eqMixin := EqMixin eqn_task.
+Canonical concrete_task_eqType := Eval hnf in EqType concrete_task concrete_task_eqMixin.
+
+
+(** ** Implementation of a Concrete Job *)
+
+
+(** A job comprises of an id, an arrival time, a cost, a deadline and the
+ task it belongs to. *)
+Record concrete_job :=
+ { job_id: nat
+ ; job_arrival: instant
+ ; job_cost: nat
+ ; job_deadline: instant
+ ; job_task: [eqType of concrete_task]
+ }.
+
+(** To make it compatible with ssreflect, we define a decidable
+ equality for concrete jobs. *)
+Definition job_eqdef (j1 j2: concrete_job) :=
+ (job_id j1 == job_id j2)
+ && (job_arrival j1 == job_arrival j2)
+ && (job_cost j1 == job_cost j2)
+ && (job_deadline j1 == job_deadline j2)
+ && (job_task j1 == job_task j2).
+
+(** Next, we prove that [job_eqdef] is indeed an equality, ... *)
+Lemma eqn_job : Equality.axiom job_eqdef.
+Proof.
+ unfold Equality.axiom; intros x y.
+ destruct (job_eqdef x y) eqn:EQ.
+ { apply ReflectT; unfold job_eqdef in *.
+ move: EQ => /andP [/andP [/andP [/andP [/eqP ID /eqP ARR] /eqP COST] /eqP DL] /eqP TASK].
+ by destruct x, y; simpl in *; subst. }
+ { apply ReflectF.
+ unfold job_eqdef, not in *; intro BUG.
+ apply negbT in EQ; rewrite negb_and in EQ.
+ destruct x, y.
+ rewrite negb_and in EQ.
+ move: EQ => /orP [EQ | /eqP TASK].
+ move: EQ => /orP [EQ | /eqP DL].
+ rewrite negb_and in EQ.
+ move: EQ => /orP [EQ | /eqP COST].
+ rewrite negb_and in EQ.
+ move: EQ => /orP [/eqP ID | /eqP ARR].
+ - by apply ID; inversion BUG.
+ - by apply ARR; inversion BUG.
+ - by apply COST; inversion BUG.
+ - by apply DL; inversion BUG.
+ - by apply TASK; inversion BUG. }
+Qed.
+
+(** ... which allows instantiating the canonical structure for [[eqType of concrete_job]].*)
+Canonical concrete_job_eqMixin := EqMixin eqn_job.
+Canonical concrete_job_eqType := Eval hnf in EqType concrete_job concrete_job_eqMixin.
+
+
+(** ** Instances for Concrete Jobs and Tasks. *)
+
+(** In the following, we connect the concrete task and job types defined above
+ to the generic Prosa interfaces for task and job parameters. *)
+Section Parameters.
+
+ (** First, we connect the above definition of tasks with the
+ generic Prosa task-parameter interfaces. *)
+ Let Task := [eqType of concrete_task].
+ #[global,program] Instance TaskCost : TaskCost Task := task_cost.
+ #[global,program] Instance TaskPriority : TaskPriority Task := task_priority.
+ #[global,program] Instance TaskDeadline : TaskDeadline Task := task_deadline.
+
+ (** Second, we do the same for the above definition of job. *)
+ Let Job := [eqType of concrete_job].
+ #[global,program] Instance JobTask : JobTask Job Task := job_task.
+ #[global,program] Instance JobArrival : JobArrival Job := job_arrival.
+ #[global,program] Instance JobCost : JobCost Job := job_cost.
+End Parameters.