diff --git a/_CoqProject b/_CoqProject
index 3bc088664ebc0c5293bd30f2f4cf0454a7b68b60..3eaad988924579c1a6a25342e10d2a6cc295a063 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -57,14 +57,13 @@ iris/viewshifts.v
 iris/wsat.v
 iris/ownership.v
 iris/weakestpre.v
-iris/language.v
 iris/pviewshifts.v
 iris/resources.v
 iris/hoare.v
-iris/parameter.v
+iris/language.v
+iris/functor.v
 iris/tests.v
 barrier/heap_lang.v
-barrier/parameter.v
 barrier/lifting.v
 barrier/sugar.v
 barrier/tests.v
diff --git a/barrier/heap_lang.v b/barrier/heap_lang.v
index 2d683c1f48a12873f43fa76366f2b6965b295c8c..f58ee88c04e71f01a659eeac16fe068d853c564b 100644
--- a/barrier/heap_lang.v
+++ b/barrier/heap_lang.v
@@ -390,8 +390,10 @@ Section Language.
   Definition ectx_step e1 σ1 e2 σ2 (ef: option expr) :=
     ∃ K e1' e2', e1 = fill K e1' ∧ e2 = fill K e2' ∧
                  prim_step e1' σ1 e2' σ2 ef.
-
-  Global Program Instance heap_lang : Language expr value state := {|
+  Program Canonical Structure heap_lang : language := {|
+    language.expr := expr;
+    language.val := value;
+    language.state := state;
     of_val := v2e;
     to_val := e2v;
     language.atomic := atomic;
diff --git a/barrier/lifting.v b/barrier/lifting.v
index 66be41ff08fd8993ad5630de6d6b918d62f39991..779caa434daef7d04e83bc6d8e76442a0b13da8a 100644
--- a/barrier/lifting.v
+++ b/barrier/lifting.v
@@ -1,10 +1,11 @@
 Require Import prelude.gmap iris.lifting.
-Require Export iris.weakestpre barrier.parameter.
+Require Export iris.weakestpre barrier.heap_lang.
 Import uPred.
 
 Section lifting.
-Implicit Types P : iProp Σ.
-Implicit Types Q : ival Σ → iProp Σ.
+Context {Σ : iFunctor}.
+Implicit Types P : iProp heap_lang Σ.
+Implicit Types Q : val heap_lang → iProp heap_lang Σ.
 
 (** Bind. *)
 Lemma wp_bind {E e} K Q :
@@ -162,7 +163,8 @@ Qed.
 (** Base axioms for core primitives of the language: Stateless reductions *)
 
 Lemma wp_fork E e :
-  ▷ wp coPset_all e (λ _, True) ⊑ wp E (Fork e) (λ v, ■(v = LitUnitV)).
+  ▷ wp coPset_all e (λ _, True : iProp heap_lang Σ)
+  ⊑ wp E (Fork e) (λ v, ■(v = LitUnitV)).
 Proof.
   etransitivity; last eapply wp_lift_pure_step with
     (φ := λ e' ef, e' = LitUnit ∧ ef = Some e);
@@ -178,7 +180,7 @@ Proof.
     apply forall_intro=>e2. apply forall_intro=>ef.
     apply impl_intro_l. apply const_elim_l. intros [-> ->].
     (* FIXME RJ This is ridicolous. *)
-    transitivity (True ★ wp coPset_all e (λ _ : ival Σ, True))%I;
+    transitivity (True ★ wp coPset_all e (λ _, True : iProp heap_lang Σ))%I;
       first by rewrite left_id.
     apply sep_mono; last reflexivity.
     rewrite -wp_value'; last reflexivity.
diff --git a/barrier/parameter.v b/barrier/parameter.v
deleted file mode 100644
index 9d2c14349df1d28eee363683967344bc4da03f86..0000000000000000000000000000000000000000
--- a/barrier/parameter.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Export barrier.heap_lang.
-Require Import iris.parameter.
-
-Canonical Structure Σ := iParam_const heap_lang unitRA.
diff --git a/barrier/sugar.v b/barrier/sugar.v
index 35c613901cae4b73d9da57ffaa61af2d58482802..d8fe3920f7050bc84ec8273341b3846ef15dc517 100644
--- a/barrier/sugar.v
+++ b/barrier/sugar.v
@@ -17,8 +17,9 @@ Definition LetCtx (K1 : ectx) (e2 : {bind expr}) := AppRCtx (LamV e2) K1.
 Definition SeqCtx (K1 : ectx) (e2 : expr) := LetCtx K1 (e2.[ren(+1)]).
 
 Section suger.
-Implicit Types P : iProp Σ.
-Implicit Types Q : ival Σ → iProp Σ.
+Context {Σ : iFunctor}.
+Implicit Types P : iProp heap_lang Σ.
+Implicit Types Q : val heap_lang → iProp heap_lang Σ.
 
 (** Proof rules for the sugar *)
 Lemma wp_lam E ef e v Q :
diff --git a/barrier/tests.v b/barrier/tests.v
index 4bbbcf90e5fc9ae481c822b0e0d56f45457564fd..fa6c63b041f4f735a009911d28eec901dfdc4838 100644
--- a/barrier/tests.v
+++ b/barrier/tests.v
@@ -25,19 +25,16 @@ Module LangTests.
   Qed.
 End LangTests.
 
-Module ParamTests.
-  Print Assumptions Σ.
-End ParamTests.
-
 Module LiftingTests.
-  Implicit Types P : iProp Σ.
-  Implicit Types Q : ival Σ → iProp Σ.
+  Context {Σ : iFunctor}.
+  Implicit Types P : iProp heap_lang Σ.
+  Implicit Types Q : val heap_lang → iProp heap_lang Σ.
 
   (* TODO RJ: Some syntactic sugar for language expressions would be nice. *)
   Definition e3 := Load (Var 0).
   Definition e2 := Seq (Store (Var 0) (Plus (Load $ Var 0) (LitNat 1))) e3.
   Definition e := Let (Alloc (LitNat 1)) e2.
-  Goal ∀ σ E, (ownP σ) ⊑ (wp E e (λ v, ■(v = LitNatV 2))).
+  Goal ∀ σ E, (ownP σ : iProp heap_lang Σ) ⊑ (wp E e (λ v, ■(v = LitNatV 2))).
   Proof.
     move=> σ E. rewrite /e.
     rewrite -wp_let. rewrite -wp_alloc_pst; last done.
@@ -121,7 +118,9 @@ Module LiftingTests.
       + done.
   Qed.
 
-  Goal ∀ E, True ⊑ wp E (Let (App Pred (LitNat 42)) (App Pred (Var 0))) (λ v, ■(v = LitNatV 40)).
+  Goal ∀ E,
+    (True : iProp heap_lang Σ)
+    ⊑ wp E (Let (App Pred (LitNat 42)) (App Pred (Var 0))) (λ v, ■(v = LitNatV 40)).
   Proof.
     intros E. rewrite -wp_let. rewrite -Pred_spec -!later_intro.
     asimpl. (* TODO RJ: Can we somehow make it so that Pred gets folded again? *)
diff --git a/iris/adequacy.v b/iris/adequacy.v
index 639e09a37cba459ccaff9b26074900ca9d208ae2..27d5ab13d304efdc35007edf55c3c541563845fd 100644
--- a/iris/adequacy.v
+++ b/iris/adequacy.v
@@ -7,9 +7,10 @@ Local Hint Extern 10 (✓{_} _) =>
   solve_validN.
 
 Section adequacy.
-Context {Σ : iParam}.
-Implicit Types e : iexpr Σ.
-Implicit Types Q : ival Σ → iProp Σ.
+Context {Λ : language} {Σ : iFunctor}.
+Implicit Types e : expr Λ.
+Implicit Types Q : val Λ → iProp Λ Σ.
+Implicit Types m : iGst Λ Σ.
 Transparent uPred_holds.
 
 Notation wptp n := (Forall3 (λ e Q r, uPred_holds (wp coPset_all e Q) n r)).
diff --git a/iris/functor.v b/iris/functor.v
new file mode 100644
index 0000000000000000000000000000000000000000..49c7a0dfe2b3ad1a6ba3557ed0150b55fea9d388
--- /dev/null
+++ b/iris/functor.v
@@ -0,0 +1,26 @@
+Require Export modures.cmra.
+
+Structure iFunctor := IFunctor {
+  ifunctor_car :> cofeT → cmraT;
+  ifunctor_empty A : Empty (ifunctor_car A);
+  ifunctor_identity A : CMRAIdentity (ifunctor_car A);
+  ifunctor_map {A B} (f : A -n> B) : ifunctor_car A -n> ifunctor_car B;
+  ifunctor_map_ne {A B} n : Proper (dist n ==> dist n) (@ifunctor_map A B);
+  ifunctor_map_id {A : cofeT} (x : ifunctor_car A) : ifunctor_map cid x ≡ x;
+  ifunctor_map_compose {A B C} (f : A -n> B) (g : B -n> C) x :
+    ifunctor_map (g ◎ f) x ≡ ifunctor_map g (ifunctor_map f x);
+  ifunctor_map_mono {A B} (f : A -n> B) : CMRAMonotone (ifunctor_map f)
+}.
+Existing Instances ifunctor_empty ifunctor_identity.
+Existing Instances ifunctor_map_ne ifunctor_map_mono.
+
+Lemma ifunctor_map_ext (Σ : iFunctor) {A B} (f g : A -n> B) m :
+  (∀ x, f x ≡ g x) → ifunctor_map Σ f m ≡ ifunctor_map Σ g m.
+Proof.
+  by intros; apply equiv_dist=> n; apply ifunctor_map_ne=> ?; apply equiv_dist.
+Qed.
+
+Program Definition iFunctor_const (icmra : cmraT) {icmra_empty : Empty icmra}
+    {icmra_identity : CMRAIdentity icmra} : iFunctor :=
+  {| ifunctor_car A := icmra; ifunctor_map A B f := cid |}.
+Solve Obligations with done.
\ No newline at end of file
diff --git a/iris/hoare.v b/iris/hoare.v
index 1f3885b4eb1971476fa7120cbd32ffc1e217ecf1..edfc9e54f9e8068f2fe32a20be73aea776db7cef 100644
--- a/iris/hoare.v
+++ b/iris/hoare.v
@@ -1,9 +1,9 @@
 Require Export iris.weakestpre iris.viewshifts.
 
-Definition ht {Σ} (E : coPset) (P : iProp Σ)
-    (e : iexpr Σ) (Q : ival Σ → iProp Σ) : iProp Σ :=
+Definition ht {Λ Σ} (E : coPset) (P : iProp Λ Σ)
+    (e : expr Λ) (Q : val Λ → iProp Λ Σ) : iProp Λ Σ :=
   (□ (P → wp E e (λ v, pvs E E (Q v))))%I.
-Instance: Params (@ht) 2.
+Instance: Params (@ht) 3.
 
 Notation "{{ P } } e @ E {{ Q } }" := (ht E P e Q)
   (at level 74, format "{{  P  } }  e  @  E  {{  Q  } }") : uPred_scope.
@@ -11,27 +11,27 @@ Notation "{{ P } } e @ E {{ Q } }" := (True ⊑ ht E P e Q)
   (at level 74, format "{{  P  } }  e  @  E  {{  Q  } }") : C_scope.
 
 Section hoare.
-Context {Σ : iParam}.
-Implicit Types P : iProp Σ.
-Implicit Types Q : ival Σ → iProp Σ.
-Implicit Types v : ival Σ.
+Context {Λ : language} {Σ : iFunctor}.
+Implicit Types P : iProp Λ Σ.
+Implicit Types Q : val Λ → iProp Λ Σ.
+Implicit Types v : val Λ.
 Import uPred.
 
 Global Instance ht_ne E n :
-  Proper (dist n ==> eq ==> pointwise_relation _ (dist n) ==> dist n) (@ht Σ E).
+  Proper (dist n ==> eq==>pointwise_relation _ (dist n) ==> dist n) (@ht Λ Σ E).
 Proof. by intros P P' HP e ? <- Q Q' HQ; rewrite /ht HP; setoid_rewrite HQ. Qed.
 Global Instance ht_proper E :
-  Proper ((≡) ==> eq ==> pointwise_relation _ (≡) ==> (≡)) (@ht Σ E).
+  Proper ((≡) ==> eq ==> pointwise_relation _ (≡) ==> (≡)) (@ht Λ Σ E).
 Proof. by intros P P' HP e ? <- Q Q' HQ; rewrite /ht HP; setoid_rewrite HQ. Qed.
 Lemma ht_mono E P P' Q Q' e :
   P ⊑ P' → (∀ v, Q' v ⊑ Q v) → {{ P' }} e @ E {{ Q' }} ⊑ {{ P }} e @ E {{ Q }}.
 Proof. by intros HP HQ; rewrite /ht -HP; setoid_rewrite HQ. Qed.
 Global Instance ht_mono' E :
-  Proper (flip (⊑) ==> eq ==> pointwise_relation _ (⊑) ==> (⊑)) (@ht Σ E).
+  Proper (flip (⊑) ==> eq ==> pointwise_relation _ (⊑) ==> (⊑)) (@ht Λ Σ E).
 Proof. by intros P P' HP e ? <- Q Q' HQ; apply ht_mono. Qed.
 
 Lemma ht_val E v :
-  {{ True }} of_val v @ E {{ λ v', ■ (v = v') }}.
+  {{ True : iProp Λ Σ }} of_val v @ E {{ λ v', ■ (v = v') }}.
 Proof.
   apply (always_intro' _ _), impl_intro_l.
   by rewrite -wp_value -pvs_intro; apply const_intro.
diff --git a/iris/hoare_lifting.v b/iris/hoare_lifting.v
index df791cf698fcadf6006316c7308155bdb2f08962..5e5467f1bf64845cbabbc80207557367d4f3c045 100644
--- a/iris/hoare_lifting.v
+++ b/iris/hoare_lifting.v
@@ -8,12 +8,14 @@ Local Notation "{{ P } } ef ?@ E {{ Q } }" :=
   (at level 74, format "{{  P  } }  ef  ?@  E  {{  Q  } }") : C_scope.
 
 Section lifting.
-Context {Σ : iParam}.
-Implicit Types e : iexpr Σ.
+Context {Λ : language} {Σ : iFunctor}.
+Implicit Types e : expr Λ.
+Implicit Types P : iProp Λ Σ.
+Implicit Types R : val Λ → iProp Λ Σ.
 Import uPred.
 
 Lemma ht_lift_step E1 E2
-    (φ : iexpr Σ → istate Σ → option (iexpr Σ) → Prop) P P' Q1 Q2 R e1 σ1 :
+    (φ : expr Λ → state Λ → option (expr Λ) → Prop) P P' Q1 Q2 R e1 σ1 :
   E1 ⊆ E2 → to_val e1 = None →
   reducible e1 σ1 →
   (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
@@ -42,8 +44,7 @@ Proof.
   rewrite {1}/ht -always_wand_impl always_elim wand_elim_r; apply wp_mono=>v.
   by apply const_intro.
 Qed.
-Lemma ht_lift_atomic E
-    (φ : iexpr Σ → istate Σ → option (iexpr Σ) → Prop) P e1 σ1 :
+Lemma ht_lift_atomic E (φ : expr Λ → state Λ → option (expr Λ) → Prop) P e1 σ1 :
   atomic e1 →
   reducible e1 σ1 →
   (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
@@ -68,7 +69,7 @@ Proof.
     rewrite -(exist_intro σ2) -(exist_intro ef) (of_to_val e2) //.
     by rewrite -always_and_sep_r'; apply and_intro; try apply const_intro.
 Qed.
-Lemma ht_lift_pure_step E (φ : iexpr Σ → option (iexpr Σ) → Prop) P P' Q e1 :
+Lemma ht_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) P P' Q e1 :
   to_val e1 = None →
   (∀ σ1, reducible e1 σ1) →
   (∀ σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → σ1 = σ2 ∧ φ e2 ef) →
@@ -94,7 +95,7 @@ Proof.
   by apply const_intro.
 Qed.
 Lemma ht_lift_pure_determistic_step E
-    (φ : iexpr Σ → option (iexpr Σ) → Prop) P P' Q e1 e2 ef :
+    (φ : expr Λ → option (expr Λ) → Prop) P P' Q e1 e2 ef :
   to_val e1 = None →
   (∀ σ1, reducible e1 σ1) →
   (∀ σ1 e2' σ2 ef', prim_step e1 σ1 e2' σ2 ef' → σ1 = σ2 ∧ e2 = e2' ∧ ef = ef')→
diff --git a/iris/language.v b/iris/language.v
index b3aa860f254bf8a0c7183223058e5d463688657b..9bb0fca56ebfd3a6092dd85cd768831d782e10ac 100644
--- a/iris/language.v
+++ b/iris/language.v
@@ -1,10 +1,13 @@
-Require Export modures.base.
+Require Export modures.cmra.
 
-Class Language (E V St : Type) := {
-  of_val : V → E;
-  to_val : E → option V;
-  atomic : E → Prop;
-  prim_step : E → St → E → St → option E → Prop;
+Structure language := Language {
+  expr : Type;
+  val : Type;
+  state : Type;
+  of_val : val → expr;
+  to_val : expr → option val;
+  atomic : expr → Prop;
+  prim_step : expr → state → expr → state → option expr → Prop;
   to_of_val v : to_val (of_val v) = Some v;
   of_to_val e v : to_val e = Some v → of_val v = e;
   values_stuck e σ e' σ' ef : prim_step e σ e' σ' ef → to_val e = None;
@@ -14,31 +17,43 @@ Class Language (E V St : Type) := {
     prim_step e1 σ1 e2 σ2 ef →
     is_Some (to_val e2)
 }.
+Arguments of_val {_} _.
+Arguments to_val {_} _.
+Arguments atomic {_} _.
+Arguments prim_step {_} _ _ _ _ _.
+Arguments to_of_val {_} _.
+Arguments of_to_val {_} _ _ _.
+Arguments values_stuck {_} _ _ _ _ _ _.
+Arguments atomic_not_value {_} _ _.
+Arguments atomic_step {_} _ _ _ _ _ _ _.
+
+Canonical Structure istateC Σ := leibnizC (state Σ).
+
+Definition cfg (Λ : language) := (list (expr Λ) * state Λ)%type.
 
 Section language.
-  Context `{Language E V St}.
+  Context {Λ : language}.
+  Implicit Types v : val Λ.
 
-  Definition reducible (e : E) (σ : St) :=
+  Definition reducible (e : expr Λ) (σ : state Λ) :=
     ∃ e' σ' ef, prim_step e σ e' σ' ef.
+  Inductive step (ρ1 ρ2 : cfg Λ) : Prop :=
+    | step_atomic e1 σ1 e2 σ2 ef t1 t2 :
+       ρ1 = (t1 ++ e1 :: t2, σ1) →
+       ρ2 = (t1 ++ e2 :: t2 ++ option_list ef, σ2) →
+       prim_step e1 σ1 e2 σ2 ef →
+       step ρ1 ρ2.
+
   Lemma reducible_not_val e σ : reducible e σ → to_val e = None.
   Proof. intros (?&?&?&?); eauto using values_stuck. Qed.
-
   Lemma atomic_of_val v : ¬atomic (of_val v).
   Proof.
     by intros Hat; apply atomic_not_value in Hat; rewrite to_of_val in Hat.
   Qed.
-  Global Instance: Injective (=) (=) of_val.
+  Global Instance: Injective (=) (=) (@of_val Λ).
   Proof. by intros v v' Hv; apply (injective Some); rewrite -!to_of_val Hv. Qed.
 
-  Definition cfg : Type := (list E * St)%type.
-  Inductive step (ρ1 ρ2 : cfg) : Prop :=
-    | step_atomic e1 σ1 e2 σ2 ef t1 t2 :
-       ρ1 = (t1 ++ e1 :: t2, σ1) →
-       ρ2 = (t1 ++ e2 :: t2 ++ option_list ef, σ2) →
-       prim_step e1 σ1 e2 σ2 ef →
-       step ρ1 ρ2.
-
-  Record is_ctx (K : E → E) := IsCtx {
+  Record is_ctx (K : expr Λ → expr Λ) := IsCtx {
     is_ctx_value e : to_val e = None → to_val (K e) = None;
     is_ctx_step_preserved e1 σ1 e2 σ2 ef :
       prim_step e1 σ1 e2 σ2 ef → prim_step (K e1) σ1 (K e2) σ2 ef;
diff --git a/iris/lifting.v b/iris/lifting.v
index c94eda289e988da9ac0c8ea2dd2298a147a9437d..6e8c632bb5601dd2221f5ba79f17d6c84a9be2d7 100644
--- a/iris/lifting.v
+++ b/iris/lifting.v
@@ -7,14 +7,15 @@ Local Hint Extern 10 (✓{_} _) =>
   solve_validN.
 
 Section lifting.
-Context {Σ : iParam}.
-Implicit Types v : ival Σ.
-Implicit Types e : iexpr Σ.
-Implicit Types σ : istate Σ.
+Context {Λ : language} {Σ : iFunctor}.
+Implicit Types v : val Λ.
+Implicit Types e : expr Λ.
+Implicit Types σ : state Λ.
+Implicit Types Q : val Λ → iProp Λ Σ.
 Transparent uPred_holds.
 
 Lemma wp_lift_step E1 E2
-    (φ : iexpr Σ → istate Σ → option (iexpr Σ) → Prop) Q e1 σ1 :
+    (φ : expr Λ → state Λ → option (expr Λ) → Prop) Q e1 σ1 :
   E1 ⊆ E2 → to_val e1 = None →
   reducible e1 σ1 →
   (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
@@ -35,7 +36,7 @@ Proof.
   { rewrite (commutative _ r2) -(associative _); eauto using wsat_le. }
   by exists r1', r2'; split_ands; [| |by intros ? ->].
 Qed.
-Lemma wp_lift_pure_step E (φ : iexpr Σ → option (iexpr Σ) → Prop) Q e1 :
+Lemma wp_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) Q e1 :
   to_val e1 = None →
   (∀ σ1, reducible e1 σ1) →
   (∀ σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → σ1 = σ2 ∧ φ e2 ef) →
diff --git a/iris/model.v b/iris/model.v
index f6d146a2b03325f97ad927af83e67d331169c1b5..6fde393bbf486b06a72d169c73c9378c281371d4 100644
--- a/iris/model.v
+++ b/iris/model.v
@@ -2,15 +2,17 @@ Require Export modures.logic iris.resources.
 Require Import modures.cofe_solver.
 
 Module iProp.
-Definition F (Σ : iParam) (A B : cofeT) : cofeT := uPredC (resRA Σ (laterC A)).
-Definition map {Σ : iParam} {A1 A2 B1 B2 : cofeT}
-    (f : (A2 -n> A1) * (B1 -n> B2)) : F Σ A1 B1 -n> F Σ A2 B2 :=
+Definition F (Λ : language) (Σ : iFunctor) (A B : cofeT) : cofeT :=
+  uPredC (resRA Λ Σ (laterC A)).
+Definition map {Λ : language} {Σ : iFunctor} {A1 A2 B1 B2 : cofeT}
+    (f : (A2 -n> A1) * (B1 -n> B2)) : F Λ Σ A1 B1 -n> F Λ Σ A2 B2 :=
   uPredC_map (resRA_map (laterC_map (f.1))).
-Definition result Σ : solution (F Σ).
+Definition result Λ Σ : solution (F Λ Σ).
 Proof.
-  apply (solver.result _ (@map Σ)).
-  * intros A B P. rewrite /map /= -{2}(uPred_map_id P). apply uPred_map_ext=>r {P} /=.
-    rewrite -{2}(res_map_id r). apply res_map_ext=>{r} r /=. by rewrite later_map_id.
+  apply (solver.result _ (@map Λ Σ)).
+  * intros A B P. rewrite /map /= -{2}(uPred_map_id P). apply uPred_map_ext=> r.
+    rewrite /= -{2}(res_map_id r); apply res_map_ext=>{r} r /=.
+    by rewrite later_map_id.
   * intros A1 A2 A3 B1 B2 B3 f g f' g' P. rewrite /map /=.
     rewrite -uPred_map_compose. apply uPred_map_ext=>{P} r /=.
     rewrite -res_map_compose. apply res_map_ext=>{r} r /=.
@@ -21,22 +23,24 @@ Qed.
 End iProp.
 
 (* Solution *)
-Definition iPreProp (Σ : iParam) : cofeT := iProp.result Σ.
-Notation iRes Σ := (res Σ (laterC (iPreProp Σ))).
-Notation iResRA Σ := (resRA Σ (laterC (iPreProp Σ))).
-Notation iWld Σ := (mapRA positive (agreeRA (laterC (iPreProp Σ)))).
-Notation iPst Σ := (exclRA (istateC Σ)).
-Notation iGst Σ := (icmra Σ (laterC (iPreProp Σ))).
-Definition iProp (Σ : iParam) : cofeT := uPredC (iResRA Σ).
-Definition iProp_unfold {Σ} : iProp Σ -n> iPreProp Σ := solution_fold _.
-Definition iProp_fold {Σ} : iPreProp Σ -n> iProp Σ := solution_unfold _.
-Lemma iProp_fold_unfold {Σ} (P : iProp Σ) : iProp_fold (iProp_unfold P) ≡ P.
+Definition iPreProp (Λ : language) (Σ : iFunctor) : cofeT := iProp.result Λ Σ.
+Notation iRes Λ Σ := (res Λ Σ (laterC (iPreProp Λ Σ))).
+Notation iResRA Λ Σ := (resRA Λ Σ (laterC (iPreProp Λ Σ))).
+Notation iWld Λ Σ := (mapRA positive (agreeRA (laterC (iPreProp Λ Σ)))).
+Notation iPst Λ := (exclRA (istateC Λ)).
+Notation iGst Λ Σ := (ifunctor_car Σ (laterC (iPreProp Λ Σ))).
+Definition iProp (Λ : language) (Σ : iFunctor) : cofeT := uPredC (iResRA Λ Σ).
+Definition iProp_unfold {Λ Σ} : iProp Λ Σ -n> iPreProp Λ Σ := solution_fold _.
+Definition iProp_fold {Λ Σ} : iPreProp Λ Σ -n> iProp Λ Σ := solution_unfold _.
+Lemma iProp_fold_unfold {Λ Σ} (P : iProp Λ Σ) : iProp_fold (iProp_unfold P) ≡ P.
 Proof. apply solution_unfold_fold. Qed.
-Lemma iProp_unfold_fold {Σ} (P : iPreProp Σ) : iProp_unfold (iProp_fold P) ≡ P.
+Lemma iProp_unfold_fold {Λ Σ} (P : iPreProp Λ Σ) :
+  iProp_unfold (iProp_fold P) ≡ P.
 Proof. apply solution_fold_unfold. Qed.
 Bind Scope uPred_scope with iProp.
 
-Instance iProp_fold_inj n Σ : Injective (dist n) (dist n) (@iProp_fold Σ).
+Instance iProp_fold_inj n Λ Σ : Injective (dist n) (dist n) (@iProp_fold Λ Σ).
 Proof. by intros X Y H; rewrite -(iProp_unfold_fold X) H iProp_unfold_fold. Qed.
-Instance iProp_unfold_inj n Σ : Injective (dist n) (dist n) (@iProp_unfold Σ).
+Instance iProp_unfold_inj n Λ Σ :
+  Injective (dist n) (dist n) (@iProp_unfold Λ Σ).
 Proof. by intros X Y H; rewrite -(iProp_fold_unfold X) H iProp_fold_unfold. Qed.
diff --git a/iris/ownership.v b/iris/ownership.v
index a42e3de4985702d9a2c1a3a8334f1b3a6b69ddb0..fc168f419792c322719e1cefe6c7ff03827f102c 100644
--- a/iris/ownership.v
+++ b/iris/ownership.v
@@ -1,25 +1,25 @@
 Require Export iris.model.
 
-Definition inv {Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
+Definition inv {Λ Σ} (i : positive) (P : iProp Λ Σ) : iProp Λ Σ :=
   uPred_own (Res {[ i ↦ to_agree (Later (iProp_unfold P)) ]} ∅ ∅).
-Arguments inv {_} _ _%I.
-Definition ownP {Σ} (σ : istate Σ) : iProp Σ := uPred_own (Res ∅ (Excl σ) ∅).
-Definition ownG {Σ} (m : iGst Σ) : iProp Σ := uPred_own (Res ∅ ∅ m).
-Instance: Params (@inv) 2.
-Instance: Params (@ownP) 1.
-Instance: Params (@ownG) 1.
+Arguments inv {_ _} _ _%I.
+Definition ownP {Λ Σ} (σ: state Λ) : iProp Λ Σ := uPred_own (Res ∅ (Excl σ) ∅).
+Definition ownG {Λ Σ} (m : iGst Λ Σ) : iProp Λ Σ := uPred_own (Res ∅ ∅ m).
+Instance: Params (@inv) 3.
+Instance: Params (@ownP) 2.
+Instance: Params (@ownG) 2.
 
 Typeclasses Opaque inv ownG ownP.
 
 Section ownership.
-Context {Σ : iParam}.
-Implicit Types r : iRes Σ.
-Implicit Types σ : istate Σ.
-Implicit Types P : iProp Σ.
-Implicit Types m : iGst Σ.
+Context {Λ : language} {Σ : iFunctor}.
+Implicit Types r : iRes Λ Σ.
+Implicit Types σ : state Λ.
+Implicit Types P : iProp Λ Σ.
+Implicit Types m : iGst Λ Σ.
 
 (* Invariants *)
-Global Instance inv_contractive i : Contractive (@inv Σ i).
+Global Instance inv_contractive i : Contractive (@inv Λ Σ i).
 Proof.
   intros n P Q HPQ.
   apply (_: Proper (_ ==> _) iProp_unfold), Later_contractive in HPQ.
@@ -36,18 +36,18 @@ Lemma inv_sep_dup i P : inv i P ≡ (inv i P ★ inv i P)%I.
 Proof. apply (uPred.always_sep_dup' _). Qed.
 
 (* physical state *)
-Lemma ownP_twice σ1 σ2 : (ownP σ1 ★ ownP σ2 : iProp Σ) ⊑ False.
+Lemma ownP_twice σ1 σ2 : (ownP σ1 ★ ownP σ2 : iProp Λ Σ) ⊑ False.
 Proof.
   rewrite /ownP -uPred.own_op Res_op.
   by apply uPred.own_invalid; intros (_&?&_).
 Qed.
-Global Instance ownP_timeless σ : TimelessP (ownP σ).
+Global Instance ownP_timeless σ : TimelessP (@ownP Λ Σ σ).
 Proof. rewrite /ownP; apply _. Qed.
 
 (* ghost state *)
-Global Instance ownG_ne n : Proper (dist n ==> dist n) (@ownG Σ).
+Global Instance ownG_ne n : Proper (dist n ==> dist n) (@ownG Λ Σ).
 Proof. by intros m m' Hm; unfold ownG; rewrite Hm. Qed.
-Global Instance ownG_proper : Proper ((≡) ==> (≡)) (@ownG Σ) := ne_proper _.
+Global Instance ownG_proper : Proper ((≡) ==> (≡)) (@ownG Λ Σ) := ne_proper _.
 Lemma ownG_op m1 m2 : ownG (m1 ⋅ m2) ≡ (ownG m1 ★ ownG m2)%I.
 Proof. by rewrite /ownG -uPred.own_op Res_op !(left_id _ _). Qed.
 Lemma always_ownG_unit m : (□ ownG (unit m))%I ≡ ownG (unit m).
diff --git a/iris/parameter.v b/iris/parameter.v
deleted file mode 100644
index d59a9186f12690be8e1375a3de64a343523eefb9..0000000000000000000000000000000000000000
--- a/iris/parameter.v
+++ /dev/null
@@ -1,37 +0,0 @@
-Require Export modures.cmra iris.language.
-
-Structure iParam := IParam {
-  iexpr : Type;
-  ival : Type;
-  istate : Type;
-  ilanguage : Language iexpr ival istate;
-  icmra : cofeT → cmraT;
-  icmra_empty A : Empty (icmra A);
-  icmra_identity A : CMRAIdentity (icmra A);
-  icmra_map {A B} (f : A -n> B) : icmra A -n> icmra B;
-  icmra_map_ne {A B} n : Proper (dist n ==> dist n) (@icmra_map A B);
-  icmra_map_id {A : cofeT} (x : icmra A) : icmra_map cid x ≡ x;
-  icmra_map_compose {A B C} (f : A -n> B) (g : B -n> C) x :
-    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)
-}.
-Existing Instances ilanguage.
-Existing Instances icmra_empty icmra_identity.
-Existing Instances icmra_map_ne icmra_map_mono.
-Canonical Structure istateC Σ := leibnizC (istate Σ).
-
-Lemma icmra_map_ext (Σ : iParam) {A B} (f g : A -n> B) m :
-  (∀ x, f x ≡ g x) → icmra_map Σ f m ≡ icmra_map Σ g m.
-Proof.
-  by intros ?; apply equiv_dist=> n; apply icmra_map_ne=> ?; apply equiv_dist.
-Qed.
-
-Program Definition iParam_const {iexpr ival istate : Type}
-  (ilanguage : Language iexpr ival istate)
-  (icmra : cmraT)
-  {icmra_empty : Empty icmra} {icmra_identity : CMRAIdentity icmra} : iParam :=
-{|
-  iexpr := iexpr; ival := ival; istate := istate;
-  icmra A := icmra; icmra_map A B f := cid
-|}.
-Solve Obligations with done.
\ No newline at end of file
diff --git a/iris/pviewshifts.v b/iris/pviewshifts.v
index ad3ac04c7110076ff64fdf21421b9fcebb89c26a..e84941e58d86e5bff8977822c14bacf9fd1249b7 100644
--- a/iris/pviewshifts.v
+++ b/iris/pviewshifts.v
@@ -7,38 +7,38 @@ Local Hint Extern 10 (✓{_} _) =>
   repeat match goal with H : wsat _ _ _ _ |- _ => apply wsat_valid in H end;
   solve_validN.
 
-Program Definition pvs {Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
+Program Definition pvs {Λ Σ} (E1 E2 : coPset) (P : iProp Λ Σ) : iProp Λ Σ :=
   {| uPred_holds n r1 := ∀ rf k Ef σ,
        1 < k ≤ n → (E1 ∪ E2) ∩ Ef = ∅ →
        wsat k (E1 ∪ Ef) σ (r1 ⋅ rf) →
        ∃ r2, P k r2 ∧ wsat k (E2 ∪ Ef) σ (r2 ⋅ rf) |}.
 Next Obligation.
-  intros Σ E1 E2 P r1 r2 n HP Hr rf k Ef σ ?? Hwsat; simpl in *.
+  intros Λ Σ E1 E2 P r1 r2 n HP Hr rf k Ef σ ?? Hwsat; simpl in *.
   apply HP; auto. by rewrite (dist_le _ _ _ _ Hr); last lia.
 Qed.
-Next Obligation. intros Σ E1 E2 P r rf k Ef σ; simpl in *; lia. Qed.
+Next Obligation. intros Λ Σ E1 E2 P r rf k Ef σ; simpl in *; lia. Qed.
 Next Obligation.
-  intros Σ E1 E2 P r1 r2 n1 n2 HP [r3 ?] Hn ? rf k Ef σ ?? Hws; setoid_subst.
+  intros Λ Σ E1 E2 P r1 r2 n1 n2 HP [r3 ?] Hn ? rf k Ef σ ?? Hws; setoid_subst.
   destruct (HP (r3⋅rf) k Ef σ) as (r'&?&Hws'); rewrite ?(associative op); auto.
   exists (r' â‹… r3); rewrite -(associative _); split; last done.
   apply uPred_weaken with r' k; eauto using cmra_included_l.
 Qed.
-Arguments pvs {_} _ _ _%I : simpl never.
-Instance: Params (@pvs) 3.
+Arguments pvs {_ _} _ _ _%I : simpl never.
+Instance: Params (@pvs) 4.
 
 Section pvs.
-Context {Σ : iParam}.
-Implicit Types P Q : iProp Σ.
-Implicit Types m : iGst Σ.
+Context {Λ : language} {Σ : iFunctor}.
+Implicit Types P Q : iProp Λ Σ.
+Implicit Types m : iGst Λ Σ.
 Transparent uPred_holds.
 
-Global Instance pvs_ne E1 E2 n : Proper (dist n ==> dist n) (@pvs Σ E1 E2).
+Global Instance pvs_ne E1 E2 n : Proper (dist n ==> dist n) (@pvs Λ Σ E1 E2).
 Proof.
   intros P Q HPQ r1 n' ??; simpl; split; intros HP rf k Ef σ ???;
     destruct (HP rf k Ef σ) as (r2&?&?); auto;
     exists r2; split_ands; auto; apply HPQ; eauto.
 Qed.
-Global Instance pvs_proper E1 E2 : Proper ((≡) ==> (≡)) (@pvs Σ E1 E2).
+Global Instance pvs_proper E1 E2 : Proper ((≡) ==> (≡)) (@pvs Λ Σ E1 E2).
 Proof. apply ne_proper, _. Qed.
 
 Lemma pvs_intro E P : P ⊑ pvs E E P.
@@ -96,7 +96,7 @@ Proof.
   * by rewrite -(left_id_L ∅ (∪) Ef).
   * apply uPred_weaken with r n; auto.
 Qed.
-Lemma pvs_updateP E m (P : iGst Σ → Prop) :
+Lemma pvs_updateP E m (P : iGst Λ Σ → Prop) :
   m ⇝: P → ownG m ⊑ pvs E E (∃ m', ■ P m' ∧ ownG m').
 Proof.
   intros Hup r [|n] ? Hinv%ownG_spec rf [|k] Ef σ ???; try lia.
@@ -116,7 +116,7 @@ Qed.
 (* Derived rules *)
 Opaque uPred_holds.
 Import uPred.
-Global Instance pvs_mono' E1 E2 : Proper ((⊑) ==> (⊑)) (@pvs Σ E1 E2).
+Global Instance pvs_mono' E1 E2 : Proper ((⊑) ==> (⊑)) (@pvs Λ Σ E1 E2).
 Proof. intros P Q; apply pvs_mono. Qed.
 Lemma pvs_trans' E P : pvs E E (pvs E E P) ⊑ pvs E E P.
 Proof. apply pvs_trans; solve_elem_of. Qed.
diff --git a/iris/resources.v b/iris/resources.v
index a8a37647d5907bf064be6d2df757446e3b8a05d8..d2692b7daf05efa57f3cc8c74d80f58a099fd789 100644
--- a/iris/resources.v
+++ b/iris/resources.v
@@ -1,56 +1,57 @@
-Require Export modures.fin_maps modures.agree modures.excl iris.parameter.
+Require Export modures.fin_maps modures.agree modures.excl.
+Require Export iris.language iris.functor.
 
-Record res (Σ : iParam) (A : cofeT) := Res {
+Record res (Λ : language) (Σ : iFunctor) (A : cofeT) := Res {
   wld : mapRA positive (agreeRA A);
-  pst : exclRA (istateC Σ);
-  gst : icmra Σ A;
+  pst : exclRA (istateC Λ);
+  gst : Σ A;
 }.
 Add Printing Constructor res.
-Arguments Res {_ _} _ _ _.
-Arguments wld {_ _} _.
-Arguments pst {_ _} _.
-Arguments gst {_ _} _.
-Instance: Params (@Res) 2.
-Instance: Params (@wld) 2.
-Instance: Params (@pst) 2.
-Instance: Params (@gst) 2.
+Arguments Res {_ _ _} _ _ _.
+Arguments wld {_ _ _} _.
+Arguments pst {_ _ _} _.
+Arguments gst {_ _ _} _.
+Instance: Params (@Res) 3.
+Instance: Params (@wld) 3.
+Instance: Params (@pst) 3.
+Instance: Params (@gst) 3.
 
 Section res.
-Context {Σ : iParam} {A : cofeT}.
-Implicit Types r : res Σ A.
+Context {Λ : language} {Σ : iFunctor} {A : cofeT}.
+Implicit Types r : res Λ Σ A.
 
-Inductive res_equiv' (r1 r2 : res Σ A) := Res_equiv :
+Inductive res_equiv' (r1 r2 : res Λ Σ A) := Res_equiv :
   wld r1 ≡ wld r2 → pst r1 ≡ pst r2 → gst r1 ≡ gst r2 → res_equiv' r1 r2.
-Instance res_equiv : Equiv (res Σ A) := res_equiv'.
-Inductive res_dist' (n : nat) (r1 r2 : res Σ A) := Res_dist :
+Instance res_equiv : Equiv (res Λ Σ A) := res_equiv'.
+Inductive res_dist' (n : nat) (r1 r2 : res Λ Σ A) := Res_dist :
   wld r1 ={n}= wld r2 → pst r1 ={n}= pst r2 → gst r1 ={n}= gst r2 →
   res_dist' n r1 r2.
-Instance res_dist : Dist (res Σ A) := res_dist'.
+Instance res_dist : Dist (res Λ Σ A) := res_dist'.
 Global Instance Res_ne n :
-  Proper (dist n ==> dist n ==> dist n ==> dist n) (@Res Σ A).
+  Proper (dist n ==> dist n ==> dist n ==> dist n) (@Res Λ Σ A).
 Proof. done. Qed.
-Global Instance Res_proper : Proper ((≡) ==> (≡) ==> (≡) ==> (≡)) (@Res Σ A).
+Global Instance Res_proper : Proper ((≡) ==> (≡) ==> (≡) ==> (≡)) (@Res Λ Σ A).
 Proof. done. Qed.
-Global Instance wld_ne n : Proper (dist n ==> dist n) (@wld Σ A).
+Global Instance wld_ne n : Proper (dist n ==> dist n) (@wld Λ Σ A).
 Proof. by destruct 1. Qed.
-Global Instance wld_proper : Proper ((≡) ==> (≡)) (@wld Σ A).
+Global Instance wld_proper : Proper ((≡) ==> (≡)) (@wld Λ Σ A).
 Proof. by destruct 1. Qed.
-Global Instance pst_ne n : Proper (dist n ==> dist n) (@pst Σ A).
+Global Instance pst_ne n : Proper (dist n ==> dist n) (@pst Λ Σ A).
 Proof. by destruct 1. Qed.
-Global Instance pst_ne' n : Proper (dist (S n) ==> (≡)) (@pst Σ A).
+Global Instance pst_ne' n : Proper (dist (S n) ==> (≡)) (@pst Λ Σ A).
 Proof.
   intros σ σ' [???]; apply (timeless _), dist_le with (S n); auto with lia.
 Qed.
-Global Instance pst_proper : Proper ((≡) ==> (=)) (@pst Σ A).
+Global Instance pst_proper : Proper ((≡) ==> (=)) (@pst Λ Σ A).
 Proof. by destruct 1; unfold_leibniz. Qed.
-Global Instance gst_ne n : Proper (dist n ==> dist n) (@gst Σ A).
+Global Instance gst_ne n : Proper (dist n ==> dist n) (@gst Λ Σ A).
 Proof. by destruct 1. Qed.
-Global Instance gst_proper : Proper ((≡) ==> (≡)) (@gst Σ A).
+Global Instance gst_proper : Proper ((≡) ==> (≡)) (@gst Λ Σ A).
 Proof. by destruct 1. Qed.
-Instance res_compl : Compl (res Σ A) := λ c,
+Instance res_compl : Compl (res Λ Σ A) := λ c,
   Res (compl (chain_map wld c))
       (compl (chain_map pst c)) (compl (chain_map gst c)).
-Definition res_cofe_mixin : CofeMixin (res Σ A).
+Definition res_cofe_mixin : CofeMixin (res Λ Σ A).
 Proof.
   split.
   * intros w1 w2; split.
@@ -72,30 +73,30 @@ Global Instance res_timeless r :
   Timeless (wld r) → Timeless (gst r) → Timeless r.
 Proof. by destruct 3; constructor; try apply (timeless _). Qed.
 
-Instance res_op : Op (res Σ A) := λ r1 r2,
+Instance res_op : Op (res Λ Σ A) := λ r1 r2,
   Res (wld r1 â‹… wld r2) (pst r1 â‹… pst r2) (gst r1 â‹… gst r2).
-Global Instance res_empty : Empty (res Σ A) := Res ∅ ∅ ∅.
-Instance res_unit : Unit (res Σ A) := λ r,
+Global Instance res_empty : Empty (res Λ Σ A) := Res ∅ ∅ ∅.
+Instance res_unit : Unit (res Λ Σ A) := λ r,
   Res (unit (wld r)) (unit (pst r)) (unit (gst r)).
-Instance res_validN : ValidN (res Σ A) := λ n r,
+Instance res_validN : ValidN (res Λ Σ A) := λ n r,
   ✓{n} (wld r) ∧ ✓{n} (pst r) ∧ ✓{n} (gst r).
-Instance res_minus : Minus (res Σ A) := λ r1 r2,
+Instance res_minus : Minus (res Λ Σ A) := λ r1 r2,
   Res (wld r1 ⩪ wld r2) (pst r1 ⩪ pst r2) (gst r1 ⩪ gst r2).
-Lemma res_included (r1 r2 : res Σ A) :
+Lemma res_included (r1 r2 : res Λ Σ A) :
   r1 ≼ r2 ↔ wld r1 ≼ wld r2 ∧ pst r1 ≼ pst r2 ∧ gst r1 ≼ gst r2.
 Proof.
   split; [|by intros ([w ?]&[σ ?]&[m ?]); exists (Res w σ m)].
   intros [r Hr]; split_ands;
     [exists (wld r)|exists (pst r)|exists (gst r)]; apply Hr.
 Qed.
-Lemma res_includedN (r1 r2 : res Σ A) n :
+Lemma res_includedN (r1 r2 : res Λ Σ A) n :
   r1 ≼{n} r2 ↔ wld r1 ≼{n} wld r2 ∧ pst r1 ≼{n} pst r2 ∧ gst r1 ≼{n} gst r2.
 Proof.
   split; [|by intros ([w ?]&[σ ?]&[m ?]); exists (Res w σ m)].
   intros [r Hr]; split_ands;
     [exists (wld r)|exists (pst r)|exists (gst r)]; apply Hr.
 Qed.
-Definition res_cmra_mixin : CMRAMixin (res Σ A).
+Definition res_cmra_mixin : CMRAMixin (res Λ Σ A).
 Proof.
   split.
   * by intros n x [???] ? [???]; constructor; simpl in *; cofe_subst.
@@ -116,7 +117,7 @@ Proof.
   * intros n r1 r2; rewrite res_includedN; intros (?&?&?).
     by constructor; apply cmra_op_minus.
 Qed.
-Definition res_cmra_extend_mixin : CMRAExtendMixin (res Σ A).
+Definition res_cmra_extend_mixin : CMRAExtendMixin (res Λ Σ A).
 Proof.
   intros n r r1 r2 (?&?&?) [???]; simpl in *.
   destruct (cmra_extend_op n (wld r) (wld r1) (wld r2)) as ([w w']&?&?&?),
@@ -134,13 +135,13 @@ Proof.
   * apply _.
 Qed.
 
-Definition update_pst (σ : istate Σ) (r : res Σ A) : res Σ A :=
+Definition update_pst (σ : state Λ) (r : res Λ Σ A) : res Λ Σ A :=
   Res (wld r) (Excl σ) (gst r).
-Definition update_gst (m : icmra Σ A) (r : res Σ A) : res Σ A :=
+Definition update_gst (m : Σ A) (r : res Λ Σ A) : res Λ Σ A :=
   Res (wld r) (pst r) m.
 
 Lemma wld_validN n r : ✓{n} r → ✓{n} (wld r).
-Proof. by intros (?&?&?). Qed. 
+Proof. by intros (?&?&?). Qed.
 Lemma gst_validN n r : ✓{n} r → ✓{n} (gst r).
 Proof. by intros (?&?&?). Qed.
 Lemma Res_op w1 w2 σ1 σ2 m1 m2 :
@@ -165,49 +166,50 @@ Proof. by intros ? ? [???]; constructor; apply (timeless _). Qed.
 End res.
 Arguments resRA : clear implicits.
 
-Definition res_map {Σ A B} (f : A -n> B) (r : res Σ A) : res Σ B :=
+Definition res_map {Λ Σ A B} (f : A -n> B) (r : res Λ Σ A) : res Λ Σ B :=
   Res (agree_map f <$> (wld r))
       (pst r)
-      (icmra_map Σ f (gst r)).
-Instance res_map_ne Σ (A B : cofeT) (f : A -n> B) :
+      (ifunctor_map Σ f (gst r)).
+Instance res_map_ne Λ Σ (A B : cofeT) (f : A -n> B) :
   (∀ n, Proper (dist n ==> dist n) f) →
-  ∀ n, Proper (dist n ==> dist n) (@res_map Σ _ _ f).
+  ∀ n, Proper (dist n ==> dist n) (@res_map Λ Σ _ _ f).
 Proof. by intros Hf n [] ? [???]; constructor; simpl in *; cofe_subst. Qed.
-Lemma res_map_id {Σ A} (r : res Σ A) : res_map cid r ≡ r.
+Lemma res_map_id {Λ Σ A} (r : res Λ Σ A) : res_map cid r ≡ r.
 Proof.
   constructor; simpl; [|done|].
   * rewrite -{2}(map_fmap_id (wld r)); apply map_fmap_setoid_ext=> i y ? /=.
     by rewrite -{2}(agree_map_id y); apply agree_map_ext=> y' /=.
-  * by rewrite -{2}(icmra_map_id Σ (gst r)); apply icmra_map_ext=> m /=.
+  * by rewrite -{2}(ifunctor_map_id Σ (gst r)); apply ifunctor_map_ext=> m /=.
 Qed.
-Lemma res_map_compose {Σ A B C} (f : A -n> B) (g : B -n> C) (r : res Σ A) :
+Lemma res_map_compose {Λ Σ A B C} (f : A -n> B) (g : B -n> C) (r : res Λ Σ A) :
   res_map (g ◎ f) r ≡ res_map g (res_map f r).
 Proof.
   constructor; simpl; [|done|].
   * rewrite -map_fmap_compose; apply map_fmap_setoid_ext=> i y _ /=.
     by rewrite -agree_map_compose; apply agree_map_ext=> y' /=.
-  * by rewrite -icmra_map_compose; apply icmra_map_ext=> m /=.
+  * by rewrite -ifunctor_map_compose; apply ifunctor_map_ext=> m /=.
 Qed.
-Lemma res_map_ext {Σ A B} (f g : A -n> B) (r : res Σ A) :
+Lemma res_map_ext {Λ Σ A B} (f g : A -n> B) (r : res Λ Σ A) :
   (∀ x, f x ≡ g x) → res_map f r ≡ res_map g r.
 Proof.
   intros Hfg; split; simpl; auto.
   * by apply map_fmap_setoid_ext=>i x ?; apply agree_map_ext.
-  * by apply icmra_map_ext.
+  * by apply ifunctor_map_ext.
 Qed.
-Definition resRA_map {Σ A B} (f : A -n> B) : resRA Σ A -n> resRA Σ B :=
-  CofeMor (res_map f : resRA Σ A → resRA Σ B).
-Instance res_map_cmra_monotone {Σ} {A B : cofeT} (f : A -n> B) :
-  CMRAMonotone (@res_map Σ _ _ f).
+Definition resRA_map {Λ Σ A B} (f : A -n> B) : resRA Λ Σ A -n> resRA Λ Σ B :=
+  CofeMor (res_map f : resRA Λ Σ A → resRA Λ Σ B).
+Instance res_map_cmra_monotone {Λ Σ} {A B : cofeT} (f : A -n> B) :
+  CMRAMonotone (@res_map Λ Σ _ _ f).
 Proof.
   split.
   * by intros n r1 r2; rewrite !res_includedN;
       intros (?&?&?); split_ands'; simpl; try apply includedN_preserving.
   * by intros n r (?&?&?); split_ands'; simpl; try apply validN_preserving.
 Qed.
-Instance resRA_map_ne {Σ A B} n : Proper (dist n ==> dist n) (@resRA_map Σ A B).
+Instance resRA_map_ne {Λ Σ A B} n :
+  Proper (dist n ==> dist n) (@resRA_map Λ Σ A B).
 Proof.
   intros f g Hfg r; split; simpl; auto.
   * by apply (mapRA_map_ne _ (agreeRA_map f) (agreeRA_map g)), agreeRA_map_ne.
-  * by apply icmra_map_ne.
+  * by apply ifunctor_map_ne.
 Qed.
diff --git a/iris/tests.v b/iris/tests.v
index 77b46203ca40e7aec1a09b1574417c93c70b759f..6c03babaa8e1bc7ed78de3fea7e3ee6a6d5ed798 100644
--- a/iris/tests.v
+++ b/iris/tests.v
@@ -2,5 +2,6 @@
 Require Import iris.model.
 
 Module ModelTest. (* Make sure we got the notations right. *)
-  Definition iResTest (Σ : iParam) (w : iWld Σ) (p : iPst Σ) (g : iGst Σ) : iRes Σ := Res w p g.
+  Definition iResTest {Λ : language} {Σ : iFunctor}
+    (w : iWld Λ Σ) (p : iPst Λ) (g : iGst Λ Σ) : iRes Λ Σ := Res w p g.
 End ModelTest.
diff --git a/iris/viewshifts.v b/iris/viewshifts.v
index 79f2e4d46efe29322b5bc5b1aab9d38410fa8aa2..7e6b3640f8ffd1f0e4b77c9c73a7a7e303b201bf 100644
--- a/iris/viewshifts.v
+++ b/iris/viewshifts.v
@@ -1,9 +1,9 @@
 Require Export iris.pviewshifts.
 
-Definition vs {Σ} (E1 E2 : coPset) (P Q : iProp Σ) : iProp Σ :=
+Definition vs {Λ Σ} (E1 E2 : coPset) (P Q : iProp Λ Σ) : iProp Λ Σ :=
   (□ (P → pvs E1 E2 Q))%I.
-Arguments vs {_} _ _ _%I _%I.
-Instance: Params (@vs) 3.
+Arguments vs {_ _} _ _ _%I _%I.
+Instance: Params (@vs) 4.
 Notation "P >{ E1 , E2 }> Q" := (vs E1 E2 P%I Q%I)
   (at level 69, E1 at level 1, format "P  >{ E1 , E2 }>  Q") : uPred_scope.
 Notation "P >{ E1 , E2 }> Q" := (True ⊑ vs E1 E2 P%I Q%I)
@@ -14,9 +14,9 @@ Notation "P >{ E }> Q" := (True ⊑ vs E E P%I Q%I)
   (at level 69, E at level 1, format "P  >{ E }>  Q") : C_scope.
 
 Section vs.
-Context {Σ : iParam}.
-Implicit Types P Q : iProp Σ.
-Implicit Types m : iGst Σ.
+Context {Λ : language} {Σ : iFunctor}.
+Implicit Types P Q : iProp Λ Σ.
+Implicit Types m : iGst Λ Σ.
 Import uPred.
 
 Lemma vs_alt E1 E2 P Q : (P ⊑ pvs E1 E2 Q) → P >{E1,E2}> Q.
@@ -25,14 +25,15 @@ Proof.
   by rewrite always_const (right_id _ _).
 Qed.
 Global Instance vs_ne E1 E2 n :
-  Proper (dist n ==> dist n ==> dist n) (@vs Σ E1 E2).
+  Proper (dist n ==> dist n ==> dist n) (@vs Λ Σ E1 E2).
 Proof. by intros P P' HP Q Q' HQ; rewrite /vs HP HQ. Qed.
-Global Instance vs_proper E1 E2 : Proper ((≡) ==> (≡) ==> (≡)) (@vs Σ E1 E2).
+Global Instance vs_proper E1 E2 : Proper ((≡) ==> (≡) ==> (≡)) (@vs Λ Σ E1 E2).
 Proof. apply ne_proper_2, _. Qed.
 Lemma vs_mono E1 E2 P P' Q Q' :
   P ⊑ P' → Q' ⊑ Q → P' >{E1,E2}> Q' ⊑ P >{E1,E2}> Q.
 Proof. by intros HP HQ; rewrite /vs -HP HQ. Qed.
-Global Instance vs_mono' E1 E2: Proper (flip (⊑) ==> (⊑) ==> (⊑)) (@vs Σ E1 E2).
+Global Instance vs_mono' E1 E2 :
+  Proper (flip (⊑) ==> (⊑) ==> (⊑)) (@vs Λ Σ E1 E2).
 Proof. by intros until 2; apply vs_mono. Qed.
 
 Lemma vs_false_elim E1 E2 P : False >{E1,E2}> P.
@@ -85,7 +86,7 @@ Proof.
   intros; rewrite -{1}(left_id_L ∅ (∪) E) -vs_mask_frame; last solve_elem_of.
   apply vs_close.
 Qed.
-Lemma vs_updateP E m (P : iGst Σ → Prop) :
+Lemma vs_updateP E m (P : iGst Λ Σ → Prop) :
   m ⇝: P → ownG m >{E}> (∃ m', ■ P m' ∧ ownG m').
 Proof. by intros; apply vs_alt, pvs_updateP. Qed.
 Lemma vs_update E m m' : m ⇝ m' → ownG m >{E}> ownG m'.
diff --git a/iris/weakestpre.v b/iris/weakestpre.v
index b898dd059a91d701bb6c822b8e879b599863a8b8..8acb0c293e52bf5418b902ff8bf7b240a0a2e66e 100644
--- a/iris/weakestpre.v
+++ b/iris/weakestpre.v
@@ -7,8 +7,8 @@ Local Hint Extern 10 (✓{_} _) =>
   repeat match goal with H : wsat _ _ _ _ |- _ => apply wsat_valid in H end;
   solve_validN.
 
-Record wp_go {Σ} (E : coPset) (Q Qfork : iexpr Σ → nat → iRes Σ → Prop)
-    (k : nat) (rf : iRes Σ) (e1 : iexpr Σ) (σ1 : istate Σ) := {
+Record wp_go {Λ Σ} (E : coPset) (Q Qfork : expr Λ → nat → iRes Λ Σ → Prop)
+    (k : nat) (rf : iRes Λ Σ) (e1 : expr Λ) (σ1 : state Λ) := {
   wf_safe : reducible e1 σ1;
   wp_step e2 σ2 ef :
     prim_step e1 σ1 e2 σ2 ef →
@@ -17,8 +17,8 @@ Record wp_go {Σ} (E : coPset) (Q Qfork : iexpr Σ → nat → iRes Σ → Prop)
       Q e2 k r2 ∧
       ∀ e', ef = Some e' → Qfork e' k r2'
 }.
-CoInductive wp_pre {Σ} (E : coPset)
-     (Q : ival Σ → iProp Σ) : iexpr Σ → nat → iRes Σ → Prop :=
+CoInductive wp_pre {Λ Σ} (E : coPset)
+     (Q : val Λ → iProp Λ Σ) : expr Λ → nat → iRes Λ Σ → Prop :=
   | wp_pre_value n r v : Q v n r → wp_pre E Q (of_val v) n r
   | wp_pre_step n r1 e1 :
      to_val e1 = None →
@@ -28,20 +28,20 @@ CoInductive wp_pre {Σ} (E : coPset)
        wp_go (E ∪ Ef) (wp_pre E Q)
                       (wp_pre coPset_all (λ _, True%I)) k rf e1 σ1) →
      wp_pre E Q e1 n r1.
-Program Definition wp {Σ} (E : coPset) (e : iexpr Σ)
-  (Q : ival Σ → iProp Σ) : iProp Σ := {| uPred_holds := wp_pre E Q e |}.
+Program Definition wp {Λ Σ} (E : coPset) (e : expr Λ)
+  (Q : val Λ → iProp Λ Σ) : iProp Λ Σ := {| uPred_holds := wp_pre E Q e |}.
 Next Obligation.
-  intros Σ E e Q r1 r2 n Hwp Hr.
+  intros Λ Σ E e Q r1 r2 n Hwp Hr.
   destruct Hwp as [|n r1 e2 ? Hgo]; constructor; rewrite -?Hr; auto.
   intros rf k Ef σ1 ?; rewrite -(dist_le _ _ _ _ Hr); naive_solver.
 Qed.
 Next Obligation.
-  intros Σ E e Q r; destruct (to_val e) as [v|] eqn:?.
+  intros Λ Σ E e Q r; destruct (to_val e) as [v|] eqn:?.
   * by rewrite -(of_to_val e v) //; constructor.
   * constructor; auto with lia.
 Qed.
 Next Obligation.
-  intros Σ E e Q r1 r2 n1; revert Q E e r1 r2.
+  intros Λ Σ E e Q r1 r2 n1; revert Q E e r1 r2.
   induction n1 as [n1 IH] using lt_wf_ind; intros Q E e r1 r1' n2.
   destruct 1 as [|n1 r1 e1 ? Hgo].
   * constructor; eauto using uPred_weaken.
@@ -52,14 +52,14 @@ Next Obligation.
     exists r2, (r2' â‹… rf'); split_ands; eauto 10 using (IH k), cmra_included_l.
     by rewrite -!associative (associative _ r2).
 Qed.
-Instance: Params (@wp) 3.
+Instance: Params (@wp) 4.
 
 Section wp.
-Context {Σ : iParam}.
-Implicit Types P : iProp Σ.
-Implicit Types Q : ival Σ → iProp Σ.
-Implicit Types v : ival Σ.
-Implicit Types e : iexpr Σ.
+Context {Λ : language} {Σ : iFunctor}.
+Implicit Types P : iProp Λ Σ.
+Implicit Types Q : val Λ → iProp Λ Σ.
+Implicit Types v : val Λ.
+Implicit Types e : expr Λ.
 Transparent uPred_holds.
 
 Lemma wp_weaken E1 E2 e Q1 Q2 r n n' :
@@ -77,10 +77,10 @@ Proof.
   exists r2, r2'; split_ands; [rewrite HE'|eapply IH|]; eauto.
 Qed.
 Global Instance wp_ne E e n :
-  Proper (pointwise_relation _ (dist n) ==> dist n) (wp E e).
+  Proper (pointwise_relation _ (dist n) ==> dist n) (@wp Λ Σ E e).
 Proof. by intros Q Q' HQ; split; apply wp_weaken with n; try apply HQ. Qed.
 Global Instance wp_proper E e :
-  Proper (pointwise_relation _ (≡) ==> (≡)) (wp E e).
+  Proper (pointwise_relation _ (≡) ==> (≡)) (@wp Λ Σ E e).
 Proof.
   by intros Q Q' ?; apply equiv_dist=>n; apply wp_ne=>v; apply equiv_dist.
 Qed.
@@ -180,7 +180,7 @@ Qed.
 Opaque uPred_holds.
 Import uPred.
 Global Instance wp_mono' E e :
-  Proper (pointwise_relation _ (⊑) ==> (⊑)) (wp E e).
+  Proper (pointwise_relation _ (⊑) ==> (⊑)) (@wp Λ Σ E e).
 Proof. by intros Q Q' ?; apply wp_mono. Qed.
 Lemma wp_value' E Q e v : to_val e = Some v → Q v ⊑ wp E e Q.
 Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value. Qed.
diff --git a/iris/wsat.v b/iris/wsat.v
index 69e82df1cf007c2d4bdf1f2fc8b2d55833c6e6f7..6281065b6a427ef6deea4d4c9dcc4e99f2338b80 100644
--- a/iris/wsat.v
+++ b/iris/wsat.v
@@ -5,8 +5,8 @@ Local Hint Extern 10 (✓{_} _) => solve_validN.
 Local Hint Extern 1 (✓{_} (gst _)) => apply gst_validN.
 Local Hint Extern 1 (✓{_} (wld _)) => apply wld_validN.
 
-Record wsat_pre {Σ} (n : nat) (E : coPset)
-    (σ : istate Σ) (rs : gmap positive (iRes Σ)) (r : iRes Σ) := {
+Record wsat_pre {Λ Σ} (n : nat) (E : coPset)
+    (σ : state Λ) (rs : gmap positive (iRes Λ Σ)) (r : iRes Λ Σ) := {
   wsat_pre_valid : ✓{S n} r;
   wsat_pre_state : pst r ≡ Excl σ;
   wsat_pre_dom i : is_Some (rs !! i) → i ∈ E ∧ is_Some (wld r !! i);
@@ -15,31 +15,33 @@ Record wsat_pre {Σ} (n : nat) (E : coPset)
     wld r !! i ={S n}= Some (to_agree (Later (iProp_unfold P))) →
     ∃ r', rs !! i = Some r' ∧ P n r'
 }.
-Arguments wsat_pre_valid {_ _ _ _ _ _} _.
-Arguments wsat_pre_state {_ _ _ _ _ _} _.
-Arguments wsat_pre_dom {_ _ _ _ _ _} _ _ _.
-Arguments wsat_pre_wld {_ _ _ _ _ _} _ _ _ _ _.
+Arguments wsat_pre_valid {_ _ _ _ _ _ _} _.
+Arguments wsat_pre_state {_ _ _ _ _ _ _} _.
+Arguments wsat_pre_dom {_ _ _ _ _ _ _} _ _ _.
+Arguments wsat_pre_wld {_ _ _ _ _ _ _} _ _ _ _ _.
 
-Definition wsat {Σ} (n : nat) (E : coPset) (σ : istate Σ) (r : iRes Σ) : Prop :=
+Definition wsat {Λ Σ}
+  (n : nat) (E : coPset) (σ : state Λ) (r : iRes Λ Σ) : Prop :=
   match n with 0 => True | S n => ∃ rs, wsat_pre n E σ rs (r ⋅ big_opM rs) end.
-Instance: Params (@wsat) 4.
+Instance: Params (@wsat) 5.
 Arguments wsat : simpl never.
 
 Section wsat.
-Context {Σ : iParam}.
-Implicit Types σ : istate Σ.
-Implicit Types r : iRes Σ.
-Implicit Types rs : gmap positive (iRes Σ).
-Implicit Types P : iProp Σ.
+Context {Λ : language} {Σ : iFunctor}.
+Implicit Types σ : state Λ.
+Implicit Types r : iRes Λ Σ.
+Implicit Types rs : gmap positive (iRes Λ Σ).
+Implicit Types P : iProp Λ Σ.
+Implicit Types m : iGst Λ Σ.
 
-Instance wsat_ne' : Proper (dist n ==> impl) (wsat (Σ:=Σ) n E σ).
+Instance wsat_ne' : Proper (dist n ==> impl) (@wsat Λ Σ n E σ).
 Proof.
   intros [|n] E σ r1 r2 Hr; first done; intros [rs [Hdom Hv Hs Hinv]].
   exists rs; constructor; intros until 0; setoid_rewrite <-Hr; eauto.
 Qed.
-Global Instance wsat_ne n : Proper (dist n ==> iff) (wsat (Σ:=Σ) n E σ) | 1.
+Global Instance wsat_ne n : Proper (dist n ==> iff) (@wsat Λ Σ n E σ) | 1.
 Proof. by intros E σ w1 w2 Hw; split; apply wsat_ne'. Qed.
-Global Instance wsat_proper n : Proper ((≡) ==> iff) (wsat (Σ:=Σ) n E σ) | 1.
+Global Instance wsat_proper n : Proper ((≡) ==> iff) (@wsat Λ Σ n E σ) | 1.
 Proof. by intros E σ w1 w2 Hw; apply wsat_ne, equiv_dist. Qed.
 Lemma wsat_le n n' E σ r : wsat n E σ r → n' ≤ n → wsat n' E σ r.
 Proof.
@@ -122,7 +124,7 @@ Proof.
   split; [done|exists rs].
   by constructor; split_ands'; try (rewrite /= -associative Hpst').
 Qed.
-Lemma wsat_update_gst n E σ r rf m1 (P : iGst Σ → Prop) :
+Lemma wsat_update_gst n E σ r rf m1 (P : iGst Λ Σ → Prop) :
   m1 ≼{S n} gst r → m1 ⇝: P →
   wsat (S n) E σ (r ⋅ rf) → ∃ m2, wsat (S n) E σ (update_gst m2 r ⋅ rf) ∧ P m2.
 Proof.