diff --git a/SConstruct b/SConstruct
index 2662e84beee955d6befa19dcf5ab2dc7327e3eca..b55ee77e3b3cb4e3543e87aa37af27e8649ef7ab 100644
--- a/SConstruct
+++ b/SConstruct
@@ -2,7 +2,7 @@
 # This file is distributed under the terms of the BSD license.
 import os, glob, string
 
-modules = ["prelude", "modures", "iris"]
+modules = ["prelude", "modures", "iris", "barrier"]
 Rs = '-Q . ""'
 env = DefaultEnvironment(ENV = os.environ,tools=['default', 'Coq'], COQFLAGS=Rs)
 
diff --git a/channel/heap_lang.v b/barrier/heap_lang.v
similarity index 97%
rename from channel/heap_lang.v
rename to barrier/heap_lang.v
index bd73b6656c221c7726f56a91ad903d486fcd62f4..f67a22da5c0d6db82acce3404ed8a884ec77696e 100644
--- a/channel/heap_lang.v
+++ b/barrier/heap_lang.v
@@ -1,5 +1,5 @@
 Require Import Autosubst.Autosubst.
-Require Import prelude.option prelude.gmap iris.language.
+Require Import prelude.option prelude.gmap iris.language iris.parameter.
 
 Set Bullet Behavior "Strict Subproofs".
 
@@ -318,7 +318,7 @@ Proof.
     exists K''; by eauto using f_equal, f_equal2, f_equal3, v2e_inj.
 
   intros Hfill Hred Hnval. 
-  Time revert K' Hfill; induction K=>K' /= Hfill;
+  revert K' Hfill; induction K=>K' /= Hfill;
     first (now eexists; reflexivity);
     (destruct K'; simpl;
       (* The first case is: K' is EmpyCtx. *)
@@ -408,12 +408,7 @@ Section Language.
   Definition ectx_step e1 σ1 e2 σ2 (ef: option expr) :=
     exists K e1' e2', e1 = fill K e1' /\ e2 = fill K e2' /\ prim_step e1' σ1 e2' σ2 ef.
 
-  Instance heap_lang : Language expr value state := {|
-    of_val := v2e;
-    to_val := e2v;
-    atomic := atomic;
-    prim_step := ectx_step
-  |}.
+  Instance heap_lang : Language expr value state := Build_Language v2e e2v atomic ectx_step.
   Proof.
     - exact v2v.
     - exact e2e.
@@ -431,7 +426,7 @@ Section Language.
   Lemma fill_is_ctx K: is_ctx (fill K).
   Proof.
     split.
-    - intros ? [v Hval]. eapply fill_value. eassumption.
+    - intros ? Hnval. by eapply fill_not_value.
     - intros ? ? ? ? ? (K' & e1' & e2' & Heq1 & Heq2 & Hstep).
       exists (comp_ctx K K'), e1', e2'. rewrite -!fill_comp Heq1 Heq2.
       split; last split; reflexivity || assumption.
@@ -445,3 +440,9 @@ Section Language.
   Qed.
 
 End Language.
+
+(* This is just to demonstrate that we can instantiate IParam. *)
+Module IParam.
+  Definition Σ := IParamConst heap_lang unitRA.
+  Print Assumptions Σ.
+End IParam.
diff --git a/iris/language.v b/iris/language.v
index b3aa860f254bf8a0c7183223058e5d463688657b..09c9aee60741e217cb7bb73cf17f86bf8dca1bce 100644
--- a/iris/language.v
+++ b/iris/language.v
@@ -14,6 +14,7 @@ Class Language (E V St : Type) := {
     prim_step e1 σ1 e2 σ2 ef →
     is_Some (to_val e2)
 }.
+Arguments Build_Language {_ _ _} _ _ _ _ {_ _ _ _ _}.
 
 Section language.
   Context `{Language E V St}.
diff --git a/iris/parameter.v b/iris/parameter.v
index c3973232f6557816854e42644f858eee052efbd3..66a71493cf75d0d9aa6729a4c114c2578821f04f 100644
--- a/iris/parameter.v
+++ b/iris/parameter.v
@@ -1,11 +1,13 @@
 Require Export modures.cmra iris.language.
 
+Set Bullet Behavior "Strict Subproofs".
+
 Record iParam := IParam {
   iexpr : Type;
   ival : Type;
   istate : Type;
-  icmra : cofeT → cmraT;
   ilanguage : Language iexpr ival istate;
+  icmra : cofeT → cmraT;
   icmra_empty A : Empty (icmra A);
   icmra_empty_spec A : RAIdentity (icmra A);
   icmra_empty_timeless A : Timeless (∅ : icmra A);
@@ -16,6 +18,7 @@ Record iParam := IParam {
     icmra_map (g ◎ f) x ≡ icmra_map g (icmra_map f x);
   icmra_map_mono {A B} (f : A -n> B) : CMRAMonotone (icmra_map f)
 }.
+Arguments IParam {_ _ _} ilanguage icmra {_ _ _} _ {_ _ _ _}.
 Existing Instances ilanguage.
 Existing Instances icmra_empty icmra_empty_spec icmra_empty_timeless.
 Existing Instances icmra_map_ne icmra_map_mono.
@@ -26,4 +29,15 @@ Proof.
   by intros ?; apply equiv_dist=> n; apply icmra_map_ne=> ?; apply equiv_dist.
 Qed.
 
-Canonical Structure istateC Σ := leibnizC (istate Σ).
\ No newline at end of file
+Definition IParamConst {iexpr ival istate : Type}
+           (ilanguage : Language iexpr ival istate)
+           (icmra : cmraT) {icmra_empty : Empty icmra}
+           {icmra_empty_spec : RAIdentity icmra} {icmra_empty_timeless: Timeless (∅ : icmra)}:
+  iParam.
+eapply (IParam ilanguage (fun _ => icmra) (fun _ _ _ => cid)).
+Unshelve.
+- by intros.
+- by intros.
+Defined.
+
+Canonical Structure istateC Σ := leibnizC (istate Σ).
diff --git a/modures/cmra.v b/modures/cmra.v
index 6c3430f8aae452c30507c6a2d33be90088986f5a..7b2b4127583f87d7990ccb5bda87ff74641e719b 100644
--- a/modures/cmra.v
+++ b/modures/cmra.v
@@ -307,6 +307,9 @@ Section discrete.
 End discrete.
 Arguments discreteRA _ {_ _ _ _ _ _}.
 
+(** CMRA for the unit type *)
+Canonical Structure unitRA : cmraT := discreteRA ().
+
 (** Product *)
 Section prod.
   Context {A B : cmraT}.
diff --git a/modures/ra.v b/modures/ra.v
index 8525136bb51506454cc98e832f793935f13ae87b..4401556a103147cac4987d9922a35fda7972e785 100644
--- a/modures/ra.v
+++ b/modures/ra.v
@@ -238,3 +238,21 @@ Ltac solve_included :=
   ra_reflection.quote;
   apply ra_reflection.flatten_correct, (bool_decide_unpack _);
   vm_compute; apply I.
+
+(** An RA for the unit type *)
+Instance unit_valid : Valid () := λ x, True.
+Instance unit_unit : Unit () := λ x, x.
+Instance unit_op : Op () := λ x y, tt.
+Instance unit_minus : Minus () := λ x y, tt.
+
+Instance unit_ra : RA ().
+Proof.
+  split; done.
+Qed.
+
+
+Instance unit_empty : Empty () := tt.
+Instance unit_empty_ra : RAIdentity().
+Proof.
+  split; done.
+Qed.