diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 05b2aa2..609e676 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -15,7 +15,7 @@ jobs:
           - ubuntu-latest
           - macos-latest
         ocaml-compiler:
-          - ocaml-base-compiler.5.1.0
+          - ocaml-base-compiler.5.3.0+trunk
 
     runs-on: ${{ matrix.os }}
 
diff --git a/.ocamlformat b/.ocamlformat
index 0b240ee..0b457a3 100644
--- a/.ocamlformat
+++ b/.ocamlformat
@@ -1,2 +1,2 @@
 profile = default
-version = 0.26.0
\ No newline at end of file
+version = 0.26.2
diff --git a/Makefile b/Makefile
index ffd1a36..d489c3f 100644
--- a/Makefile
+++ b/Makefile
@@ -1,7 +1,7 @@
 EXE := concurrent.exe ref.exe transaction.exe echo.exe \
 	dyn_wind.exe generator.exe promises.exe reify_reflect.exe \
 	MVar_test.exe chameneos.exe eratosthenes.exe pipes.exe loop.exe \
-	fringe.exe algorithmic_differentiation.exe
+	fringe.exe algorithmic_differentiation.exe dynamic_state.exe
 
 all: $(EXE)
 
diff --git a/README.md b/README.md
index 512088b..b480b47 100644
--- a/README.md
+++ b/README.md
@@ -38,17 +38,15 @@ The original implementation of Multicore OCaml allowed a user to `Obj.clone_cont
 
 ## Running the examples
 
-To run the examples with Multicore OCaml, be sure to install [Opam with these instructions](https://opam.ocaml.org/doc/Install.html). If your version of Opam (`opam --version`) is greater than or equal to `2.1` then the following instructions will work:
+To run the examples with OCaml, be sure to install [Opam with these instructions](https://opam.ocaml.org/doc/Install.html).
 
 ```bash
-# After cloning this repository, create a 5.1.0 switch
+# After cloning this repository, create a 5.1 switch
 opam update
-# Add the alpha repository to get unreleased 5.1.0 compatible libraries
-opam switch create 5.1.0
+opam switch create 5.1.1
 opam install . --deps-only
 ```
 
-
 Running `make` will build all of the examples. If you want to run a single executable that is built with `dune` you can run:
 
 ```
diff --git a/algorithmic_differentiation.ml b/algorithmic_differentiation.ml
index 627f240..4355bd0 100644
--- a/algorithmic_differentiation.ml
+++ b/algorithmic_differentiation.ml
@@ -17,39 +17,24 @@ end = struct
 
   let mk v = { v; d = 0.0 }
 
-  type _ Effect.t += Add : t * t -> t Effect.t
-  type _ Effect.t += Mult : t * t -> t Effect.t
+  type _ eff += Add : t * t -> t eff
+  type _ eff += Mult : t * t -> t eff
 
   let run f =
-    ignore
-      (match_with f ()
-         {
-           retc =
-             (fun r ->
-               r.d <- 1.0;
-               r);
-           exnc = raise;
-           effc =
-             (fun (type a) (e : a Effect.t) ->
-               match e with
-               | Add (a, b) ->
-                   Some
-                     (fun (k : (a, _) continuation) ->
-                       let x = { v = a.v +. b.v; d = 0.0 } in
-                       ignore (continue k x);
-                       a.d <- a.d +. x.d;
-                       b.d <- b.d +. x.d;
-                       x)
-               | Mult (a, b) ->
-                   Some
-                     (fun k ->
-                       let x = { v = a.v *. b.v; d = 0.0 } in
-                       ignore (continue k x);
-                       a.d <- a.d +. (b.v *. x.d);
-                       b.d <- b.d +. (a.v *. x.d);
-                       x)
-               | _ -> None);
-         })
+    ignore (match f () with
+      | r -> r.d <- 1.0; r;
+      | effect (Add(a,b)), k ->
+          let x = {v = a.v +. b.v; d = 0.0} in
+          ignore (continue k x);
+          a.d <- a.d +. x.d;
+          b.d <- b.d +. x.d;
+          x
+      | effect (Mult(a,b)), k ->
+          let x = {v = a.v *. b.v; d = 0.0} in
+          ignore (continue k x);
+          a.d <- a.d +. (b.v *. x.d);
+          b.d <- b.d +. (a.v *. x.d);
+          x)
 
   let grad f x =
     let x = mk x in
diff --git a/dune b/dune
index 0a6526e..b5b50a9 100644
--- a/dune
+++ b/dune
@@ -19,6 +19,10 @@
  (names dyn_wind)
  (modules dyn_wind))
 
+(executables
+ (names dynamic_state)
+ (modules dynamic_state))
+
 (executables
  (names generator)
  (modules generator))
diff --git a/dyn_wind.ml b/dyn_wind.ml
index 809ffe9..5d63f8c 100644
--- a/dyn_wind.ml
+++ b/dyn_wind.ml
@@ -6,47 +6,27 @@ open Effect.Deep
 let dynamic_wind before_thunk thunk after_thunk =
   before_thunk ();
   let res =
-    match_with thunk ()
-      {
-        retc = Fun.id;
-        exnc =
-          (fun e ->
-            after_thunk ();
-            raise e);
-        effc =
-          (fun (type a) (e : a Effect.t) ->
-            Some
-              (fun (k : (a, _) continuation) ->
-                after_thunk ();
-                let res' = perform e in
-                before_thunk ();
-                continue k res'));
-      }
+    match thunk () with
+    | v -> v
+    | exception e -> after_thunk (); raise e
+    | effect e, k ->
+        after_thunk ();
+        let res' = perform e in
+        before_thunk ();
+        continue k res'
   in
   after_thunk ();
   res
 
-type _ Effect.t += E : unit Effect.t
+type _ eff += E : unit eff
 
 let () =
   let bt () = Printf.printf "IN\n" in
   let at () = Printf.printf "OUT\n" in
   let foo () =
-    Printf.printf "peform E\n";
-    perform E;
-    Printf.printf "peform E\n";
-    perform E;
+    Printf.printf "perform E\n"; perform E;
+    Printf.printf "perform E\n"; perform E;
     Printf.printf "done\n"
   in
-  try_with (dynamic_wind bt foo) at
-    {
-      effc =
-        (fun (type a) (e : a Effect.t) ->
-          match e with
-          | E ->
-              Some
-                (fun (k : (a, _) continuation) ->
-                  Printf.printf "handled E\n";
-                  continue k ())
-          | _ -> None);
-    }
+  try dynamic_wind bt foo at with
+  | effect E, k -> Printf.printf "handled E\n"; continue k ()
diff --git a/dynamic_state.ml b/dynamic_state.ml
new file mode 100644
index 0000000..80ba2bf
--- /dev/null
+++ b/dynamic_state.ml
@@ -0,0 +1,181 @@
+open Effect
+open Effect.Deep
+
+(* This file contains a collection of attempts at replicating ML-style
+   references using algebraic effects and handlers. The difficult thing
+   to do is the dynamic creation of new reference cells at arbitrary
+   types, without needing some kind of universal type or dynamic type
+   checking. *)
+
+module type Type = sig type t end
+module Int = struct type t = int let compare = compare end
+
+module LocalState (R : sig type t end) = struct
+  type reff = R.t
+  type _ eff += New : int -> R.t eff
+  type _ eff += Get : R.t -> int eff
+  type _ eff += Put : R.t * int -> unit eff
+end
+
+module type StateOps = sig
+  type reff
+  type _ eff += New : int -> reff eff
+  type _ eff += Get : reff -> int eff
+  type _ eff += Put : reff * int -> unit eff
+end
+
+(**********************************************************************)
+(* version 1 : doesn't work, because declaration of new effect names
+   is generative, so the handler and the client get different versions of
+   the 'New', 'Get' and 'Put' effects. *)
+
+let run main =
+  let module S = LocalState (Int) in 
+  let module IM = Map.Make (Int) in
+  let comp =
+    match main (module Int : Type) with
+      | effect (S.New i), k ->
+          fun s -> let r = fst (IM.max_binding s) + 1
+                   in continue k r (IM.add r i s) 
+      | effect (S.Get r), k ->
+          fun s -> continue k (IM.find r s) s
+      | effect (S.Put (r, i)), k ->
+          fun s -> continue k () (IM.add r i s)
+      | x -> fun s -> x
+  in
+  comp IM.empty
+
+let main (module T : Type) =
+  let module S = LocalState(T) in
+  let x = perform (S.New 1) in
+  perform (S.Put (x, 5));
+  perform (S.Get x)
+
+(**********************************************************************)
+(* version 2 : working creation of freshly generated state cells, but
+   only an int type. *)
+
+let run2 main =
+  let module S  = LocalState (Int) in
+  let module IM = Map.Make (Int) in
+  let comp =
+    match main (module S : StateOps) with
+      | effect (S.New i), k ->
+          fun s ->
+            let r = if IM.is_empty s then 0 else fst (IM.max_binding s) + 1
+            in continue k r (IM.add r i s) 
+      | effect (S.Get r), k ->
+          fun s -> continue k (IM.find r s) s
+      | effect (S.Put (r, i)), k ->
+          fun s -> continue k () (IM.add r i s)
+      | x -> fun s -> x
+  in
+  comp IM.empty
+
+let main2 (module S : StateOps) =
+  let open S in
+  let x = perform (New 1) in
+  perform (Put (x, 5));
+  perform (Get x)
+
+(**********************************************************************)
+(* version 3, static creation of new state cells, requiring nested
+   handlers. Similar to the example in "state.ml". *)
+module type GetPutOps = sig
+  type t
+  type _ eff += Get : t eff
+  type _ eff += Put : t -> unit eff
+end
+
+module MakeGetPut (T : sig type t end) () = struct
+  type t = T.t
+  type _ eff += Get : t eff
+  type _ eff += Put : t -> unit eff
+end
+
+let run3 (type a) (module S : GetPutOps with type t = a) (s : a) main =
+  let module IM = Map.Make (Int) in
+  let comp =
+    match main () with
+      | effect S.Get, k ->
+          fun (s : S.t) -> continue k s s
+      | effect (S.Put i), k ->
+          fun s -> continue k () i
+      | x -> fun s -> x
+  in
+  comp s
+
+module S1 = MakeGetPut (struct type t = int end) ()
+module S2 = MakeGetPut (struct type t = string end) ()
+
+let test3 () =
+  perform (S1.Put 5);
+  let x = perform (S1.Get) in
+  perform (S2.Put (string_of_int x ^ "xx"));
+  perform S2.Get
+
+(* XXX avsm: disabled pending port to multicont (uses clone_continuation)
+
+(**********************************************************************)
+(* version 4. Uses dynamic creation of new effect names to simulate
+   the creation of new reference cells. Initially, there is only one
+   effect 'New', which can be used to dynamically create new effect
+   names. The handler for 'New' wraps the continuation in a new
+   handler that handles the freshly generated effect names. This setup
+   yields the same interface as ML refs, except that there is no way
+   to compare references for equality. This is because cells are
+   represeted as objects with a pair of a 'write' method and a 'read'
+   method, so it is possible to create new references that reference
+   the same underlying data without the access objects being
+   equal. This is similar to the situation in Idealised Algol, where
+   variables are ways to affect the state, but have no independent
+   existence of their own.
+
+   Compared to the example in "ref.ml", this implementation does not
+   require a universal type, nor does it have "impossible" cases.
+
+   This example also includes an unneccessary extra 'Choice' effect to
+   demonstrate the combination of other effects with state in the same
+   handler. This uses the experimental Obj.clone_continuation function to clone
+   continuations. *)
+type 'a reff = < get : 'a; put : 'a -> unit; internals : (module GetPutOps with type t = 'a) >
+
+effect New : 'a -> 'a rEffect.t
+effect Choice : bool
+
+let run4 main =
+  let donew : type a b. (a reff, b) continuation -> a -> b = fun k ->
+      let module Ops = MakeGetPut (struct type t = a end) () in
+      let cell = object
+                   method get   = perform Ops.Get
+                   method put x = perform (Ops.Put x)
+                   method internals = (module Ops : GetPutOps with type t = a)
+                 end
+      in
+      match continue k cell with
+        | effect Ops.Get      k -> fun s -> continue k s s
+        | effect (Ops.Put v)  k -> fun s -> continue k () v
+        | x                     -> fun s -> x
+  in
+  match main () with
+    | effect (New v) k -> donew k v
+    | effect (Choice) k -> let k' = Obj.clone_continuation k in continue k true; continue k' false
+    | x                -> x
+
+let newref i = perform (New i)
+
+let (:=) r x = r#put x
+
+let (!) r = r#get
+
+let test4 () =
+  let a = newref 0 in
+  let b = newref "str" in
+  if perform Choice then
+    begin a := String.length !b;
+          b := string_of_int !a;
+          print_endline !b
+    end
+  else
+    print_endline !b
+*)
diff --git a/eratosthenes.ml b/eratosthenes.ml
index 82d7706..c1719ef 100644
--- a/eratosthenes.ml
+++ b/eratosthenes.ml
@@ -13,22 +13,20 @@ let string_of_msg = function
 type pid = int
 (** Process primitives **)
 
-type _ Effect.t += Spawn : (pid -> unit) -> pid Effect.t
-
+type _ eff += Spawn : (pid -> unit) -> pid eff
 let spawn p = perform (Spawn p)
 
-type _ Effect.t += Yield : unit Effect.t
-
+type _ eff += Yield : unit eff
 let yield () = perform Yield
 
 (** Communication primitives **)
-type _ Effect.t += Send : pid * message -> unit Effect.t
+type _ eff += Send : pid * message -> unit eff
 
 let send pid data =
   perform (Send (pid, data));
   yield ()
 
-type _ Effect.t += Recv : pid -> message option Effect.t
+type _ eff += Recv : pid -> message option eff
 
 let rec recv pid =
   match perform (Recv pid) with
@@ -77,23 +75,14 @@ let mailbox f =
     mailbox := mb;
     msg
   in
-  try_with f ()
-    {
-      effc =
-        (fun (type a) (e : a Effect.t) ->
-          match e with
-          | Send (pid, msg) ->
-              Some
-                (fun (k : (a, _) continuation) ->
-                  mailbox := Mailbox.push pid msg !mailbox;
-                  continue k ())
-          | Recv who ->
-              Some
-                (fun k ->
-                  let msg = lookup who in
-                  continue k msg)
-          | _ -> None);
-    }
+  match f () with
+  | v -> v
+  | effect (Send (pid, msg)), k ->
+     mailbox := Mailbox.push pid msg !mailbox;
+     continue k ()
+  | effect (Recv who), k ->
+     let msg = lookup who in
+     continue k msg
 
 (** Process handler
     Slightly modified version of sched.ml **)
@@ -104,25 +93,12 @@ let run main () =
   let pid = ref (-1) in
   let rec spawn f =
     pid := 1 + !pid;
-    match_with f !pid
-      {
-        retc = (fun () -> dequeue ());
-        exnc = (fun e -> raise e);
-        effc =
-          (fun (type a) (e : a Effect.t) ->
-            match e with
-            | Yield ->
-                Some
-                  (fun (k : (a, _) continuation) ->
-                    enqueue (fun () -> continue k ());
-                    dequeue ())
-            | Spawn p ->
-                Some
-                  (fun k ->
-                    enqueue (fun () -> continue k !pid);
-                    spawn p)
-            | _ -> None);
-      }
+    match f !pid with
+    | () -> dequeue ()
+    | effect Yield, k ->
+       enqueue (fun () -> continue k ()); dequeue ()
+    | effect (Spawn p), k ->
+       enqueue (fun () -> continue k !pid); spawn p
   in
   spawn main
 
diff --git a/fringe.ml b/fringe.ml
index c186ee6..2be0f13 100644
--- a/fringe.ml
+++ b/fringe.ml
@@ -23,7 +23,7 @@ module SameFringe (E : EQUATABLE) = struct
   type nonrec tree = E.t tree
 
   (* Yielding control *)
-  type _ Effect.t += Yield : E.t -> unit Effect.t
+  type _ eff += Yield : E.t -> unit eff
 
   let yield e = perform (Yield e)
 
@@ -40,16 +40,9 @@ module SameFringe (E : EQUATABLE) = struct
 
   (* Reifies `Yield' effects *)
   let step f =
-    match_with f ()
-      {
-        retc = (fun _ -> Done);
-        exnc = (fun e -> raise e);
-        effc =
-          (fun (type a) (e : a Effect.t) ->
-            match e with
-            | Yield e -> Some (fun (k : (a, _) continuation) -> Yielded (e, k))
-            | _ -> None);
-      }
+    match f () with
+    | _ -> Done
+    | effect Yield e, k -> Yielded (e, k)
 
   (* The comparator "step walks" two given trees simultaneously *)
   let comparator ltree rtree =
diff --git a/generator.ml b/generator.ml
index eca6031..6bba813 100644
--- a/generator.ml
+++ b/generator.ml
@@ -54,28 +54,15 @@ module Tree : TREE = struct
 
   (* val to_gen : 'a t -> (unit -> 'a option) *)
   let to_gen (type a) (t : a t) =
-    let module M = struct
-      type _ Effect.t += Next : a -> unit Effect.t
-    end in
+    let module M = struct type _ eff += Next : a -> unit eff end in
     let open M in
-    let rec step =
-      ref (fun () ->
-          try_with
-            (fun t ->
-              iter (fun x -> perform (Next x)) t;
-              None)
-            t
-            {
-              effc =
-                (fun (type a) (e : a Effect.t) ->
-                  match e with
-                  | Next v ->
-                      Some
-                        (fun (k : (a, _) continuation) ->
-                          (step := fun () -> continue k ());
-                          Some v)
-                  | _ -> None);
-            })
+    let rec step = ref (fun () ->
+      try
+        iter (fun x -> perform (Next x)) t;
+        None
+      with effect (Next v), k ->
+        step := (fun () -> continue k ());
+        Some v)
     in
     fun () -> !step ()
 
diff --git a/loop.ml b/loop.ml
index 4e3fb4a..003ada9 100644
--- a/loop.ml
+++ b/loop.ml
@@ -1,19 +1,12 @@
 open Effect
 open Effect.Deep
 
-type _ Effect.t += Foo : (unit -> 'a) Effect.t
+type _ eff += Foo : (unit -> 'a) eff
 
 let f () = perform Foo ()
 
 let res : type a. a =
-  try_with f ()
-    {
-      effc =
-        (fun (type a) (e : a Effect.t) ->
-          match e with
-          | Foo ->
-              Some
-                (fun (k : (a, _) continuation) ->
-                  continue k (fun () -> perform Foo ()))
-          | _ -> None);
-    }
+  match f () with
+  | x -> x
+  | effect Foo, k ->
+     continue k (fun () -> perform Foo ())
diff --git a/mvar/MVar.ml b/mvar/MVar.ml
index 70bc88c..b727737 100644
--- a/mvar/MVar.ml
+++ b/mvar/MVar.ml
@@ -9,8 +9,8 @@ end
 
 module type SCHED = sig
   type 'a cont
-  type _ Effect.t += Suspend : ('a cont -> unit) -> 'a Effect.t
-  type _ Effect.t += Resume : ('a cont * 'a) -> unit Effect.t
+  type _ eff += Suspend : ('a cont -> unit) -> 'a eff
+  type _ eff += Resume : 'a cont * 'a -> unit eff
 end
 
 module Make (S : SCHED) : S = struct
diff --git a/mvar/MVar.mli b/mvar/MVar.mli
index 5faef5d..e948192 100644
--- a/mvar/MVar.mli
+++ b/mvar/MVar.mli
@@ -22,14 +22,14 @@ module type SCHED = sig
   type 'a cont
   (** Represents a blocked computation that waits for a value of type 'a. *)
 
-  type _ Effect.t +=
-    | Suspend : ('a cont -> unit) -> 'a Effect.t
+  type _ eff +=
+    | Suspend : ('a cont -> unit) -> 'a eff
           (** [perform @@ Suspend f] applies [f] to the current continuation, and suspends the
       execution of the current thread, and switches to the next thread in the
       scheduler's queue. *)
 
-  type _ Effect.t +=
-    | Resume : ('a cont * 'a) -> unit Effect.t
+  type _ eff +=
+    | Resume : 'a cont * 'a -> unit eff
           (** [Perform @@ Resume (k,v)] prepares the suspended continuation [k] with value [v] and
       enqueues it to the scheduler queue. *)
 end
diff --git a/mvar/sched.ml b/mvar/sched.ml
index 0f5397d..dc29a59 100644
--- a/mvar/sched.ml
+++ b/mvar/sched.ml
@@ -1,11 +1,11 @@
 open Effect
 open Effect.Deep
 
-type _ Effect.t += Fork : (unit -> unit) -> unit Effect.t
-type _ Effect.t += Yield : unit Effect.t
+type _ eff += Fork : (unit -> unit) -> unit eff
+type _ eff += Yield : unit eff
 type 'a cont = ('a, unit) continuation
-type _ Effect.t += Suspend : ('a cont -> unit) -> 'a Effect.t
-type _ Effect.t += Resume : ('a cont * 'a) -> unit Effect.t
+type _ eff += Suspend : ('a cont -> unit) -> 'a eff
+type _ eff += Resume : 'a cont * 'a -> unit eff
 
 let run main =
   let run_q = Queue.create () in
diff --git a/mvar/sched.mli b/mvar/sched.mli
index 33c38e3..80476c9 100644
--- a/mvar/sched.mli
+++ b/mvar/sched.mli
@@ -1,23 +1,23 @@
 type 'a cont
 (** Represents a blocked computation that waits for a value of type 'a. *)
 
-type _ Effect.t +=
-  | Suspend : ('a cont -> unit) -> 'a Effect.t
+type _ eff +=
+  | Suspend : ('a cont -> unit) -> 'a eff
         (** [Perform @@ Suspend f] applies [f] to the current continuation, and suspends the
     execution of the current thread, and switches to the next thread in the
     scheduler's queue. *)
 
-type _ Effect.t +=
-  | Resume : ('a cont * 'a) -> unit Effect.t
+type _ eff +=
+  | Resume : 'a cont * 'a -> unit eff
         (** [perform @@ Resume (k,v)] prepares the suspended continuation [k] with value [v] and
     enqueues it to the scheduler queue. *)
 
-type _ Effect.t +=
-  | Fork : (unit -> unit) -> unit Effect.t
+type _ eff +=
+  | Fork : (unit -> unit) -> unit eff
         (** [perform @@ Fork f] forks [f] as a new thread to which control immediately switches to. *)
 
-type _ Effect.t +=
-  | Yield : unit Effect.t
+type _ eff +=
+  | Yield : unit eff
         (** [perform Yield] suspends the current thread and switches to the next thread from
     the run queue. *)
 
diff --git a/pipes.ml b/pipes.ml
index e952fc0..188b4e3 100644
--- a/pipes.ml
+++ b/pipes.ml
@@ -1,16 +1,13 @@
 open Effect
+
 (** Deep encoding of pipes.
     The example is adapted from Kammar et al. (2013) **)
 
-open Effect.Deep
-
 (* We specialise our pipes to work only with integers *)
-type _ Effect.t += Await : int Effect.t
-
+type _ eff += Await : int eff
 let await () = perform Await
 
-type _ Effect.t += Yield : int -> unit Effect.t
-
+type _ eff += Yield : int -> unit eff
 let yield s = perform (Yield s)
 
 type prod = Prod of (unit -> cons -> unit)
@@ -20,19 +17,11 @@ let flip f y x = f x y
 
 (* Parameterised handler that takes a consumer as parameter *)
 let up m =
-  match_with m ()
-    {
-      retc = (fun v _ -> v);
-      exnc = raise;
-      effc =
-        (fun (type a) (e : a Effect.t) ->
-          match e with
-          | Yield s ->
-              Some
-                (fun (k : (a, _) continuation) (Cons cons) ->
-                  cons s (Prod (fun () -> continue k ())))
-          | _ -> None);
-    }
+  match m () with
+  | v -> fun _ -> v
+  | effect (Yield s), k ->
+     fun (Cons cons) ->
+       cons s (Prod (fun () -> Effect.Deep.continue k ()))
 
 (* Refine up to accept the parameter first rather than the computation. It's
    more convenient when combining handlers. *)
@@ -40,19 +29,11 @@ let up = flip up
 
 (* Parameterised handler that takes a producer as parameter *)
 let down m =
-  match_with m ()
-    {
-      retc = (fun v _ -> v);
-      exnc = raise;
-      effc =
-        (fun (type a) (e : a Effect.t) ->
-          match e with
-          | Await ->
-              Some
-                (fun (k : (a, _) continuation) (Prod prod) ->
-                  prod () (Cons (fun s -> continue k s)))
-          | _ -> None);
-    }
+  match m () with
+  | v -> fun _ -> v
+  | effect Await, k ->
+     fun (Prod prod) ->
+       prod () (Cons (fun s -> Effect.Deep.continue k s))
 
 let down = flip down
 
diff --git a/promises.ml b/promises.ml
index 8c0d0b2..9bd9866 100644
--- a/promises.ml
+++ b/promises.ml
@@ -25,8 +25,10 @@ module Promise : Promise = struct
 
   type 'a status = Done of 'a | Cancelled of exn | Waiting of tvar list
   type 'a t = 'a status ref
-  type _ Effect.t += Fork : (unit -> 'a) -> 'a t Effect.t
-  type _ Effect.t += Wait : 'a t -> unit Effect.t
+
+  type _ eff +=
+   | Fork : (unit -> 'a) -> 'a t eff
+   | Wait : 'a t -> unit eff
 
   let fork f = perform (Fork f)
   let enqueue run_q k v = Queue.push (fun () -> ignore @@ continue k v) run_q
@@ -103,33 +105,14 @@ module Promise : Promise = struct
   let run main =
     let run_q = Queue.create () in
     let rec spawn : 'a. 'a status ref -> (unit -> 'a) -> unit =
-     fun sr f ->
-      match_with f ()
-        {
-          retc =
-            (fun v ->
-              finish run_q sr v;
-              dequeue run_q);
-          exnc =
-            (fun e ->
-              abort run_q sr e;
-              dequeue run_q);
-          effc =
-            (fun (type a) (e : a Effect.t) ->
-              match e with
-              | Wait sr ->
-                  Some
-                    (fun (k : (a, _) continuation) ->
-                      wait sr k;
-                      dequeue run_q)
-              | Fork f ->
-                  Some
-                    (fun k ->
-                      let sr = mk_status () in
-                      enqueue run_q k sr;
-                      spawn sr f)
-              | _ -> None);
-        }
+      fun sr f ->
+        match f () with
+        | v -> finish run_q sr v; dequeue run_q
+        | exception e -> abort run_q sr e; dequeue run_q
+        | effect (Wait sr), k -> wait sr k; dequeue run_q
+        | effect (Fork f), k ->
+            let sr = mk_status () in
+            enqueue run_q k sr; spawn sr f
     in
     let sr = mk_status () in
     spawn sr main;
diff --git a/ref.ml b/ref.ml
index 22522c7..809af7b 100644
--- a/ref.ml
+++ b/ref.ml
@@ -47,74 +47,46 @@ module type HEAP = functor (_ : CELL) -> REF
    [get] and [set] obtained from a new instance of [Cell].
 *)
 
-module FCMBasedHeap : HEAP =
-functor
-  (Cell : CELL)
-  ->
-  struct
-    (* [EFF] declares a pair of effect names [Get] and [Set]. *)
-    module type EFF = sig
-      type t
-      type _ Effect.t += Get : t Effect.t
-      type _ Effect.t += Set : t -> unit Effect.t
-    end
-
-    (* ['a t] is the type of first-class [EFF] modules.
-       The effect-name declarations in [EFF] become first-class. *)
-    type 'a t = (module EFF with type t = 'a)
-    type _ Effect.t += Ref : 'a -> 'a t Effect.t
-
-    let ref init = perform (Ref init)
-    let ( ! ) : type a. a t -> a = fun (module E) -> perform E.Get
-
-    let ( := ) : type a. a t -> a -> unit =
-     fun (module E) y -> perform (E.Set y)
-
-    (* [fresh()] allocates fresh effect names [Get] and [Set],
-        and packs these names into a first-class module. *)
-    let fresh (type a) () : a t =
-      (module struct
-        type t = a
-        type _ Effect.t += Get : t Effect.t
-        type _ Effect.t += Set : t -> unit Effect.t
-      end)
-
-    let run main =
-      try_with main ()
-        {
-          effc =
-            (fun (type b) (e : b Effect.t) ->
-              match e with
-              | Ref init ->
-                  Some
-                    (fun (k : (b, _) continuation) ->
-                      (init, k)
-                      |>
-                      fun (type a) ((init, k) : a * (a t, _) continuation) ->
-                        let module E = (val (fresh () : a t)) in
-                        let module C = Cell (struct
-                          type t = a
-                        end) in
-                        let main () =
-                          try_with (continue k)
-                            (module E)
-                            {
-                              effc =
-                                (fun (type c) (e : c Effect.t) ->
-                                  match e with
-                                  | E.Get ->
-                                      Some
-                                        (fun (k : (c, _) continuation) ->
-                                          continue k (C.get () : a))
-                                  | E.Set y ->
-                                      Some (fun k -> continue k (C.set y))
-                                  | _ -> None);
-                            }
-                        in
-                        snd (C.run ~init main))
-              | _ -> None);
-        }
+module FCMBasedHeap : HEAP = functor (Cell : CELL) -> struct
+  (* [EFF] declares a pair of effect names [Get] and [Set]. *)
+  module type EFF = sig
+    type t
+    type _ eff += Get : t eff | Set : t -> unit eff
   end
+  (* ['a t] is the type of first-class [EFF] modules.
+     The effect-name declarations in [EFF] become first-class. *)
+  type 'a t = (module EFF with type t = 'a)
+
+  type _ eff += Ref : 'a -> ('a t) eff
+
+  let ref init = perform (Ref init)
+  let (!) : type a. a t -> a =
+    fun (module E) -> perform E.Get
+  let (:=) : type a. a t -> a -> unit =
+    fun (module E) y -> perform (E.Set y)
+
+  (* [fresh()] allocates fresh effect names [Get] and [Set],
+      and packs these names into a first-class module. *)
+  let fresh (type a) () : a t =
+    (module struct
+      type t = a
+      type _ eff += Get : t eff | Set : t -> unit eff
+    end)
+
+  let run main =
+   try main () with
+     effect (Ref init), k ->
+       (* trick to name the existential type introduced by the matching: *)
+       (init, k) |> fun (type a) (init, k : a * (a t, _) continuation) ->
+       let module E = (val (fresh (): a t)) in
+       let module C = Cell(struct type t = a end) in
+       let main () =
+         try continue k (module E) with
+         | effect E.Get, k -> continue k (C.get() : a)
+         | effect (E.Set y), k -> continue k (C.set y)
+       in
+       snd (C.run ~init main)
+end
 
 (* --------------------------------------------------------------------------- *)
 (** Heap Implementation Based on Records. *)
@@ -127,37 +99,24 @@ functor
    by this new cell.
 *)
 
-module RecordBasedHeap : HEAP =
-functor
-  (Cell : CELL)
-  ->
-  struct
-    type 'a t = { get : unit -> 'a; set : 'a -> unit }
-    type _ Effect.t += Ref : 'a -> 'a t Effect.t
-
-    let ref init = perform (Ref init)
-    let ( ! ) { get; _ } = get ()
-    let ( := ) { set; _ } y = set y
-
-    let run main =
-      try_with main ()
-        {
-          effc =
-            (fun (type b) (e : b Effect.t) ->
-              match e with
-              | Ref init ->
-                  Some
-                    (fun (k : (b, _) continuation) ->
-                      (init, k)
-                      |>
-                      fun (type a) ((init, k) : a * (a t, _) continuation) ->
-                        let open Cell (struct
-                          type t = a
-                        end) in
-                        snd (run ~init (fun _ -> continue k { get; set })))
-              | _ -> None);
-        }
-  end
+module RecordBasedHeap : HEAP = functor (Cell : CELL) -> struct
+  type 'a t = {
+    get : unit -> 'a;
+    set : 'a -> unit;
+  }
+  type _ eff += Ref : 'a -> 'a t eff
+
+  let ref init = perform (Ref init)
+  let (!) {get; _} = get()
+  let (:=) {set; _} y = set y
+
+  let run main =
+    try main () with
+    | effect (Ref init), k ->
+        (init, k) |> fun (type a) ((init, k) : a * (a t, _) continuation) ->
+        let open Cell(struct type t = a end) in
+        snd (run ~init (fun _ -> continue k {get; set}))
+end
 
 (* --------------------------------------------------------------------------- *)
 (** Examples. *)
diff --git a/reify_reflect.ml b/reify_reflect.ml
index 2da0cd2..aa77226 100644
--- a/reify_reflect.ml
+++ b/reify_reflect.ml
@@ -15,21 +15,12 @@ end
 module RR (M : MONAD) : sig
   val reify : (unit -> 'a) -> 'a M.t
   val reflect : 'a M.t -> 'a
-end = struct
-  type _ Effect.t += E : 'a M.t -> 'a Effect.t
-
-  let reify f =
-    match_with f ()
-      {
-        retc = (fun x -> M.return x);
-        exnc = raise;
-        effc =
-          (fun (type a) (e : a Effect.t) ->
-            match e with
-            | E m -> Some (fun k -> M.bind m (continue k))
-            | _ -> None);
-      }
-
+end =
+struct
+  type _ eff += E : 'a M.t -> 'a eff
+  let reify f = match f () with
+      x -> M.return x
+    | effect (E m), k -> M.bind m (continue k)
   let reflect m = perform (E m)
 end
 
diff --git a/sched.ml b/sched.ml
index 40691ed..d8c305a 100644
--- a/sched.ml
+++ b/sched.ml
@@ -1,42 +1,26 @@
-open Effect
-open Effect.Deep
+type _ eff += Fork  : (unit -> unit) -> unit eff
+type _ eff += Yield : unit eff
 
-type _ Effect.t += Fork : (unit -> unit) -> unit Effect.t
-type _ Effect.t += Yield : unit Effect.t
-
-let fork f = perform (Fork f)
-let yield () = perform Yield
+let fork f = Effect.perform (Fork f)
+let yield () = Effect.perform Yield
 
 (* A concurrent round-robin scheduler *)
 let run main =
   let run_q = Queue.create () in
   let enqueue k = Queue.push k run_q in
   let dequeue () =
-    if Queue.is_empty run_q then () else continue (Queue.pop run_q) ()
+    if Queue.is_empty run_q then () else Effect.Deep.continue (Queue.pop run_q) ()
   in
   let rec spawn f =
     (* Effect handler => instantiates fiber *)
-    match_with f ()
-      {
-        retc = (fun () -> dequeue ());
-        exnc =
-          (fun e ->
-            print_string (Printexc.to_string e);
-            dequeue ());
-        effc =
-          (fun (type a) (e : a Effect.t) ->
-            match e with
-            | Yield ->
-                Some
-                  (fun (k : (a, unit) continuation) ->
-                    enqueue k;
-                    dequeue ())
-            | Fork f ->
-                Some
-                  (fun (k : (a, unit) continuation) ->
-                    enqueue k;
-                    spawn f)
-            | _ -> None);
-      }
+    match f () with
+    | () -> dequeue ()
+    | exception e ->
+        ( print_string (Printexc.to_string e);
+          dequeue () )
+    | effect Yield, k ->
+        ( enqueue k; dequeue () )
+    | effect (Fork f), k ->
+        ( enqueue k; spawn f )
   in
   spawn main
diff --git a/state.ml b/state.ml
index 7b62877..89dc093 100644
--- a/state.ml
+++ b/state.ml
@@ -136,38 +136,20 @@ functor
    of [get] and [set], there is no interference among these instances,
    because effect names are immutable.
 *)
-module LocalMutVar : CELL =
-functor
-  (T : TYPE)
-  ->
-  struct
-    type t = T.t
-    type _ Effect.t += Get : t Effect.t
-    type _ Effect.t += Set : t -> unit Effect.t
-
-    let get () = perform Get
-    let set y = perform (Set y)
-
-    let run (type a) ~init main : t * a =
-      let var = ref init in
-      match_with main ()
-        {
-          retc = (fun res -> (!var, res));
-          exnc = raise;
-          effc =
-            (fun (type b) (e : b Effect.t) ->
-              match e with
-              | Get ->
-                  Some
-                    (fun (k : (b, t * a) continuation) -> continue k (!var : t))
-              | Set y ->
-                  Some
-                    (fun k ->
-                      var := y;
-                      continue k ())
-              | _ -> None);
-        }
-  end
+module LocalMutVar : CELL = functor (T : TYPE) -> struct
+  type t = T.t
+  type _ eff += Get : t eff | Set : t -> unit eff
+
+  let get () = perform Get
+  let set y = perform (Set y)
+
+  let run (type a) ~init main : t * a=
+    let var = ref init in
+    match main () with
+    | res -> !var, res
+    | effect Get, k -> continue k (!var : t)
+    | effect (Set y), k -> var := y; continue k ()
+end
 
 (* --------------------------------------------------------------------------- *)
 (** State-Passing Style. *)
@@ -194,35 +176,29 @@ functor
    separate stacks are safe. The same remarks as for the functor [LocalMutVar]
    apply.
 *)
-module StPassing : CELL =
-functor
-  (T : TYPE)
-  ->
-  struct
-    type t = T.t
-    type _ Effect.t += Get : t Effect.t
-    type _ Effect.t += Set : t -> unit Effect.t
-
-    let get () = perform Get
-    let set y = perform (Set y)
-
-    let run (type a) ~init (main : unit -> a) : t * a =
-      match_with main ()
-        {
-          retc = (fun res x -> (x, res));
-          exnc = raise;
-          effc =
-            (fun (type b) (e : b Effect.t) ->
-              match e with
-              | Get ->
-                  Some
-                    (fun (k : (b, t -> t * a) continuation) (x : t) ->
-                      continue k x x)
-              | Set y -> Some (fun k (_x : t) -> continue k () y)
-              | _ -> None);
-        }
-        init
-  end
+module StPassing : CELL = functor (T : TYPE) -> struct
+  type t = T.t
+  type _ eff += Get : t eff | Set : t -> unit eff
+
+  let get () = perform Get
+  let set y = perform (Set y)
+
+  let run (type a) ~init (main : unit -> a) : t * a =
+    (* In this case the lower-level syntax is less verbose
+       since we have to rebind the existentials anyway if using
+       the concrete effect syntax. *)
+    match_with main () {
+      retc = (fun res x -> (x, res));
+      exnc = raise;
+      effc = fun (type b) (e : b eff) ->
+        match e with
+        | Get -> Some (fun (k : (b, t -> (t * a)) continuation) ->
+            fun (x : t) -> continue k x x)
+        | Set y -> Some (fun k ->
+            fun (_x : t) -> continue k () y)
+        | _ -> None
+    } init
+end
 
 (* --------------------------------------------------------------------------- *)
 (** Examples. *)
diff --git a/transaction.ml b/transaction.ml
index 5d4341f..448fdad 100644
--- a/transaction.ml
+++ b/transaction.ml
@@ -15,32 +15,19 @@ end
 
 module Txn : TXN = struct
   type 'a t = 'a ref
-  type _ Effect.t += Update : 'a t * 'a -> unit Effect.t
+
+  type _ eff += Update : 'a t * 'a -> unit eff
 
   let atomically f =
     let comp =
-      match_with f ()
-        {
-          retc = (fun x _ -> x);
-          exnc =
-            (fun e rb ->
-              rb ();
-              raise e);
-          effc =
-            (fun (type a) (e : a Effect.t) ->
-              match e with
-              | Update (r, v) ->
-                  Some
-                    (fun (k : (a, _) continuation) rb ->
-                      let old_v = !r in
-                      r := v;
-                      continue k () (fun () ->
-                          r := old_v;
-                          rb ()))
-              | _ -> None);
-        }
-    in
-    comp (fun () -> ())
+      match f () with
+      | x -> (fun _ -> x)
+      | exception e -> (fun rb -> rb (); raise e)
+      | effect (Update (r,v)), k -> (fun rb ->
+          let old_v = !r in
+          r := v;
+          continue k () (fun () -> r := old_v; rb ()))
+    in comp (fun () -> ())
 
   let ref = ref
   let ( ! ) = ( ! )