diff --git a/interpreter/binary/decode.ml b/interpreter/binary/decode.ml
index 9f815f7e..0d7ec86c 100644
--- a/interpreter/binary/decode.ml
+++ b/interpreter/binary/decode.ml
@@ -144,15 +144,8 @@ let sized f s =
 
 open Types
 
-let var s = vu32 s
 let zero s = expect 0x00 s "zero byte expected"
 
-let var_type s =
-  let pos = pos s in
-  match vs33 s with
-  | i when i >= 0l -> SynVar i
-  | _ -> error s pos "malformed type index"
-
 let num_type s =
   match s7 s with
   | -0x01 -> I32T
@@ -208,12 +201,12 @@ let func_type s =
   FuncT (ts1, ts2)
 
 let cont_type s =
-  ContType (var_type s)
+  ContT (Stat (var_type s))
 
 let def_type s =
   match s7 s with
   | -0x20 -> DefFuncT (func_type s)
-  | -0x21 -> ContDefType (cont_type s)
+  | -0x21 -> DefContT (cont_type s)
   | _ -> error s (pos s - 1) "malformed definition type"
 
 
@@ -234,8 +227,8 @@ let memory_type s =
 
 let tag_type s =
   zero s;
-  let x = var_type s in
-  TagType x
+  let x = Stat (var_type s) in
+  TagT x
 
 let mutability s =
   match byte s with
@@ -329,7 +322,7 @@ let rec instr s =
     let ct = catch_list s in
     let ca =
       if peek s = Some 0x19 then begin
-        ignore (u8 s);
+        ignore (byte s);
         Some (instr_block s)
       end else
         None
@@ -372,13 +365,11 @@ let rec instr s =
   | 0x14 -> call_ref (at var s)
   | 0x15 -> return_call_ref (at var s)
 
-  | 0x16 as b -> illegal s pos b
+  | (0x16 | 0x17) as b -> illegal s pos b
 
   | 0x18 -> error s pos "misplaced DELEGATE opcode"
   | 0x19 -> error s pos "misplaced CATCH_ALL opcode"
 
-  | 0x17 | 0x19 as b -> illegal s pos b
-
   | 0x1a -> drop
   | 0x1b -> select None
   | 0x1c -> select (Some (vec val_type s))
@@ -900,7 +891,7 @@ and instr_block' s es =
     instr_block' s (Source.(e' @@ region s pos pos) :: es)
 and catch_list s =
   if peek s = Some 0x07 then begin
-    ignore (u8 s);
+    ignore (byte s);
     let tag = at var s in
     let instrs = instr_block s in
     (tag, instrs) :: catch_list s
@@ -1244,7 +1235,7 @@ let module_ s =
     s (len s) "data count section required";
   let funcs =
     List.map2 (fun t f -> {f.it with ftype = t} @@ f.at) func_types func_bodies
-  in {types; tables; memories; globals; funcs; imports; exports; elems; datas; start}
+  in {types; tables; memories; tags; globals; funcs; imports; exports; elems; datas; start}
 
 
 let decode name bs = at module_ (stream name bs)
diff --git a/interpreter/binary/encode.ml b/interpreter/binary/encode.ml
index 26d4cfca..abe07f75 100644
--- a/interpreter/binary/encode.ml
+++ b/interpreter/binary/encode.ml
@@ -130,11 +130,11 @@ struct
     | FuncT (ts1, ts2) -> vec val_type ts1; vec val_type ts2
 
   let cont_type = function
-    | ContType x -> var_type x
+    | ContT x -> var_type x
 
   let def_type = function
     | DefFuncT ft -> s7 (-0x20); func_type ft
-    | ContDefType ct -> vs7 (-0x21); cont_type ct
+    | DefContT ct -> s7 (-0x21); cont_type ct (* TODO(dhil): I think the GC proposal claims opcode -0x21 for one of the struct/array types. *)
 
   let limits vu {min; max} =
     bool (max <> None); vu min; opt vu max
@@ -152,8 +152,8 @@ struct
   let global_type = function
     | GlobalT (mut, t) -> val_type t; mutability mut
 
-  let tag_type (TagType x) =
-    vu32 0x00l; var_type x
+  let tag_type (TagT x) =
+    u32 0x00l; var_type x
 
   (* Instructions *)
 
diff --git a/interpreter/exec/eval.ml b/interpreter/exec/eval.ml
index 253df15b..aa6c9999 100644
--- a/interpreter/exec/eval.ml
+++ b/interpreter/exec/eval.ml
@@ -64,9 +64,8 @@ and admin_instr' =
   | Plain of instr'
   | Refer of ref_
   | Invoke of func_inst
-  | Label of int * instr list * code
-  | Frame of int * frame * code
-  | Local of int32 * value list * code
+  | Label of int32 * instr list * code
+  | Frame of int32 * frame * code
   | Handle of (tag_inst * idx) list option * code
   | Trapping of string
   | Throwing of tag_inst * value stack
@@ -88,7 +87,7 @@ type ref_ += ContRef of cont option ref
 let () =
   let type_of_ref' = !Value.type_of_ref' in
   Value.type_of_ref' := function
-    | ContRef _ -> BotHeapType  (* TODO *)
+    | ContRef _ -> BotHT  (* TODO *)
     | r -> type_of_ref' r
 
 let () =
@@ -199,7 +198,7 @@ let rec step (c : config) : config =
     match e.it, vs with
     | Plain e', vs ->
       (match e', vs with
-      | Unreachable, vs ->
+       | Unreachable, vs ->
         vs, [Trapping "unreachable executed" @@ e.at]
 
       | Nop, vs ->
@@ -207,14 +206,14 @@ let rec step (c : config) : config =
 
       | Block (bt, es'), vs ->
         let InstrT (ts1, ts2, _xs) = block_type c.frame.inst bt e.at in
-        let n1 = List.length ts1 in
-        let n2 = List.length ts2 in
+        let n1 = Lib.List32.length ts1 in
+        let n2 = Lib.List32.length ts2 in
         let args, vs' = take n1 vs e.at, drop n1 vs e.at in
         vs', [Label (n2, [], (args, List.map plain es')) @@ e.at]
 
       | Loop (bt, es'), vs ->
         let InstrT (ts1, ts2, _xs) = block_type c.frame.inst bt e.at in
-        let n1 = List.length ts1 in
+        let n1 = Lib.List32.length ts1 in
         let args, vs' = take n1 vs e.at, drop n1 vs e.at in
         vs', [Label (n1, [e' @@ e.at], (args, List.map plain es')) @@ e.at]
 
@@ -227,7 +226,7 @@ let rec step (c : config) : config =
       | Throw x, vs ->
         let tagt = tag c.frame.inst x in
         let TagT x' = Tag.type_of tagt in
-        let FuncT (ts, _) = as_func_def_type (def_of (as_sem_var x')) in
+        let FuncT (ts, _) = as_func_def_type (def_of (as_dyn_var x')) in
         let vs0, vs' = split (Lib.List32.length ts) vs e.at in
         vs', [Throwing (tagt, vs0) @@ e.at]
 
@@ -235,7 +234,7 @@ let rec step (c : config) : config =
         vs, [Rethrowing (x.it, fun e -> e) @@ e.at]
 
       | TryCatch (bt, es', cts, ca), vs ->
-        let FuncType (ts1, ts2) = block_type c.frame.inst bt e.at in
+        let InstrT (ts1, ts2, _xs) = block_type c.frame.inst bt e.at in
         let n1 = Lib.List32.length ts1 in
         let n2 = Lib.List32.length ts2 in
         let args, vs' = take n1 vs e.at, drop n1 vs e.at in
@@ -243,7 +242,7 @@ let rec step (c : config) : config =
         vs', [Label (n2, [], ([], [Catch (n2, cts', ca, (args, List.map plain es')) @@ e.at])) @@ e.at]
 
       | TryDelegate (bt, es', x), vs ->
-        let FuncType (ts1, ts2) = block_type c.frame.inst bt e.at in
+        let InstrT (ts1, ts2, _xs) = block_type c.frame.inst bt e.at in
         let n1 = Lib.List32.length ts1 in
         let n2 = Lib.List32.length ts2 in
         let args, vs' = take n1 vs e.at, drop n1 vs e.at in
@@ -315,7 +314,7 @@ let rec step (c : config) : config =
         vs, [Trapping "null function reference" @@ e.at]
 
       | ContNew x, Ref (FuncRef f) :: vs ->
-        let FuncType (ts, _) = Func.type_of f in
+        let FuncT (ts, _) = Func.type_of f in
         let ctxt code = compose code ([], [Invoke f @@ e.at]) in
         Ref (ContRef (ref (Some (Lib.List32.length ts, ctxt)))) :: vs, []
 
@@ -326,8 +325,8 @@ let rec step (c : config) : config =
         vs, [Trapping "continuation already consumed" @@ e.at]
 
       | ContBind x, Ref (ContRef ({contents = Some (n, ctxt)} as cont)) :: vs ->
-        let ContType z = cont_type c.frame.inst x in
-        let FuncType (ts', _) = as_func_def_type (def_of (as_sem_var z)) in
+        let ContT z = cont_type c.frame.inst x in
+        let FuncT (ts', _) = as_func_def_type (def_of (as_dyn_var z)) in
         let args, vs' =
           try split (Int32.sub n (Lib.List32.length ts')) vs e.at
           with Failure _ -> Crash.error e.at "type mismatch at continuation bind"
@@ -339,7 +338,7 @@ let rec step (c : config) : config =
       | Suspend x, vs ->
         let tagt = tag c.frame.inst x in
         let TagT x' = Tag.type_of tagt in
-        let FuncT (ts, _) = as_func_def_type (def_of (as_sem_var x')) in
+        let FuncT (ts, _) = as_func_def_type (def_of (as_dyn_var x')) in
         let args, vs' = split (Lib.List32.length ts) vs e.at in
         vs', [Suspending (tagt, args, fun code -> code) @@ e.at]
 
@@ -364,14 +363,14 @@ let rec step (c : config) : config =
       | ResumeThrow x, Ref (ContRef ({contents = Some (n, ctxt)} as cont)) :: vs ->
         let tagt = tag c.frame.inst x in
         let TagT x' = Tag.type_of tagt in
-        let FuncType (ts, _) = as_func_def_type (def_of (as_sem_var x')) in
+        let FuncT (ts, _) = as_func_def_type (def_of (as_dyn_var x')) in
         let args, vs' = split (Lib.List32.length ts) vs e.at in
         let vs1', es1' = ctxt (args, [Plain (Throw x) @@ e.at]) in
         cont := None;
         vs1' @ vs', es1'
 
       | Barrier (bt, es'), vs ->
-        let FuncType (ts1, _) = block_type c.frame.inst bt e.at in
+        let InstrT (ts1, _, _xs) = block_type c.frame.inst bt e.at in
         let args, vs' = split (Lib.List32.length ts1) vs e.at in
         vs', [
           Handle (None,
@@ -821,6 +820,12 @@ let rec step (c : config) : config =
     | Frame (n, frame', (vs', [])), vs ->
       vs' @ vs, []
 
+    | Frame (n, frame', (vs', {it = Trapping msg; at} :: es')), vs ->
+      vs, [Trapping msg @@ at]
+
+    | Frame (n, frame', (vs', {it = Throwing (a, vs0); at} :: es')), vs ->
+      vs, [Throwing (a, vs0) @@ at]
+
     | Frame (n, frame', (vs', {it = Suspending (tagt, vs1, ctxt); at} :: es')), vs ->
       let ctxt' code = [], [Frame (n, frame', compose (ctxt code) (vs', es')) @@ e.at] in
       vs, [Suspending (tagt, vs1, ctxt') @@ at]
@@ -830,7 +835,7 @@ let rec step (c : config) : config =
 
     | Frame (n, frame', (vs', {it = ReturningInvoke (vs0, f); at} :: es')), vs ->
       let FuncT (ts1, _ts2) = Func.type_of f in
-      take (List.length ts1) vs0 e.at @ vs, [Invoke f @@ at]
+      take (Lib.List32.length ts1) vs0 e.at @ vs, [Invoke f @@ at]
 
     | Frame (n, frame', code'), vs ->
       let c' = step {frame = frame'; code = code'; budget = c.budget - 1} in
@@ -895,10 +900,10 @@ let rec step (c : config) : config =
 
     | Invoke f, vs ->
       let FuncT (ts1, ts2) = Func.type_of f in
-      let n1, n2 = List.length ts1, List.length ts2 in
+      let n1, n2 = Lib.List32.length ts1, Lib.List32.length ts2 in
       let args, vs' = split n1 vs e.at in
       (match f with
-      | Func.AstFunc (_, inst', func) ->
+       | Func.AstFunc (_, inst', func) ->
         let {locals; body; _} = func.it in
         let m = Lib.Promise.value inst' in
         let ts = List.map (fun loc -> Types.dyn_val_type m.types loc.it.ltype) locals in
@@ -921,7 +926,7 @@ let rec step (c : config) : config =
     | Handle (Some hs, (vs', {it = Suspending (tagt, vs1, ctxt); at} :: es')), vs
       when List.mem_assq tagt hs ->
       let TagT x' = Tag.type_of tagt in
-      let FuncT (_, ts) = as_func_def_type (def_of (as_sem_var x')) in
+      let FuncT (_, ts) = as_func_def_type (def_of (as_dyn_var x')) in
       let ctxt' code = compose (ctxt code) (vs', es') in
       [Ref (ContRef (ref (Some (Lib.List32.length ts, ctxt'))))] @ vs1 @ vs,
       [Plain (Br (List.assq tagt hs)) @@ e.at]
@@ -1025,7 +1030,7 @@ let create_global (inst : module_inst) (glob : global) : global_inst =
 
 let create_tag (inst : module_inst) (tag : tag) : tag_inst =
   let {tagtype} = tag.it in
-  Tag.alloc (Types.sem_tag_type inst.types tagtype)
+  Tag.alloc (Types.dyn_tag_type inst.types tagtype)
 
 let create_export (inst : module_inst) (ex : export) : export_inst =
   let {name; edesc} = ex.it in
diff --git a/interpreter/host/spectest.ml b/interpreter/host/spectest.ml
index 6c13c8bb..598ec05e 100644
--- a/interpreter/host/spectest.ml
+++ b/interpreter/host/spectest.ml
@@ -26,11 +26,11 @@ let memory = Memory.alloc (MemoryT {min = 1l; max = Some 2l})
 let func f ft = Func.alloc_host (Types.alloc (DefFuncT ft)) (f ft)
 
 let tag =
-  let p = Types.alloc (FuncDefType (FuncType ([NumType I32Type], [NumType I32Type]))) in
-  Tag.alloc (TagType (SemVar p))
+  let p = Types.alloc (DefFuncT (FuncT ([NumT I32T], [NumT I32T]))) in
+  Tag.alloc (TagT (Dyn p))
 let except =
-  let p = Types.alloc (FuncDefType (FuncType ([NumType I32Type], []))) in
-  Tag.alloc (TagType (SemVar p))
+  let p = Types.alloc (DefFuncT (FuncT ([NumT I32T], []))) in
+  Tag.alloc (TagT (Dyn p))
 
 let print_value v =
   Printf.printf "%s : %s\n"
diff --git a/interpreter/runtime/instance.ml b/interpreter/runtime/instance.ml
index e6bf0920..8ab5fffc 100644
--- a/interpreter/runtime/instance.ml
+++ b/interpreter/runtime/instance.ml
@@ -66,7 +66,7 @@ let extern_type_of c = function
   | ExternTable tab -> ExternTableT (Table.type_of tab)
   | ExternMemory mem -> ExternMemoryT (Memory.type_of mem)
   | ExternGlobal glob -> ExternGlobalT (Global.type_of glob)
-  | ExternTag tag -> ExternTagType (Tag.type_of tag)
+  | ExternTag tag -> ExternTagT (Tag.type_of tag)
 
 let export inst name =
   try Some (List.assoc name inst.exports) with Not_found -> None
diff --git a/interpreter/script/js.ml b/interpreter/script/js.ml
index f0200302..7f660b74 100644
--- a/interpreter/script/js.ml
+++ b/interpreter/script/js.ml
@@ -288,6 +288,7 @@ let null_heap_type_of = function
   | Types.DefHT (Dyn a) ->
     match Types.def_of a with
     | Types.DefFuncT _ -> FuncHT
+    | Types.DefContT _ -> assert false
 
 let value v =
   match v.it with
diff --git a/interpreter/syntax/free.ml b/interpreter/syntax/free.ml
index ce0c5a94..dd22343c 100644
--- a/interpreter/syntax/free.ml
+++ b/interpreter/syntax/free.ml
@@ -90,11 +90,11 @@ let val_type = function
   | BotT -> empty
 
 let func_type (FuncT (ins, out)) = list val_type ins ++ list val_type out
-let cont_type (ContType x) = var_type x
+let cont_type (ContT x) = var_type x
 let global_type (GlobalT (_mut, t)) = val_type t
 let table_type (TableT (_lim, t)) = ref_type t
 let memory_type (MemoryT (_lim)) = empty
-let tag_type (TagType x) = var_type x
+let tag_type (TagT x) = var_type x
 
 let def_type = function
   | DefFuncT ft -> func_type ft
diff --git a/interpreter/syntax/types.ml b/interpreter/syntax/types.ml
index d76dd2e5..c93089d1 100644
--- a/interpreter/syntax/types.ml
+++ b/interpreter/syntax/types.ml
@@ -70,30 +70,6 @@ let defaultable : val_type -> bool = function
   | BotT -> assert false
 
 
-(* Projections *)
-
-let as_syn_var = function
-  | SynVar x -> x
-  | SemVar _ -> assert false
-
-let as_sem_var = function
-  | SynVar _ -> assert false
-  | SemVar x -> x
-
-let as_func_def_type (dt : def_type) : func_type =
-  match dt with
-  | DefFuncT ft -> ft
-  | _ -> assert false
-
-let as_cont_def_type (dt : def_type) : cont_type =
-  match dt with
-  | DefContT ct -> ct
-  | _ -> assert false
-
-let extern_type_of_import_type (ImportT (et, _, _)) = et
-let extern_type_of_export_type (ExportT (et, _)) = et
-
-
 (* Filters *)
 
 let funcs (ets : extern_type list) : func_type list =
@@ -107,6 +83,96 @@ let globals (ets : extern_type list) : global_type list =
 let tags (ets : extern_type list) : tag_type list =
   Lib.List.map_filter (function ExternTagT t -> Some t | _ -> None) ets
 
+(* String conversion *)
+
+let string_of_idx x =
+  I32.to_string_u x
+
+let string_of_name n =
+  let b = Buffer.create 16 in
+  let escape uc =
+    if uc < 0x20 || uc >= 0x7f then
+      Buffer.add_string b (Printf.sprintf "\\u{%02x}" uc)
+    else begin
+      let c = Char.chr uc in
+      if c = '\"' || c = '\\' then Buffer.add_char b '\\';
+      Buffer.add_char b c
+    end
+  in
+  List.iter escape n;
+  Buffer.contents b
+
+let string_of_null : null -> string = function
+  | NoNull -> ""
+  | Null -> "null "
+
+let string_of_addr' = ref (fun (a : type_addr) -> assert false)
+let string_of_addr a = !string_of_addr' a
+
+let string_of_var : var -> string = function
+  | Stat x -> I32.to_string_u x
+  | Dyn a -> string_of_addr a
+
+let string_of_num_type : num_type -> string = function
+  | I32T -> "i32"
+  | I64T -> "i64"
+  | F32T -> "f32"
+  | F64T -> "f64"
+
+let string_of_vec_type : vec_type -> string = function
+  | V128T -> "v128"
+
+let string_of_heap_type : heap_type -> string = function
+  | FuncHT -> "func"
+  | ExternHT -> "extern"
+  | DefHT x -> string_of_var x
+  | BotHT -> "something"
+
+let string_of_ref_type : ref_type -> string = function
+  | (nul, t) ->
+    "(ref " ^ string_of_null nul ^ string_of_heap_type t ^ ")"
+
+let string_of_val_type : val_type -> string = function
+  | NumT t -> string_of_num_type t
+  | VecT t -> string_of_vec_type t
+  | RefT t -> string_of_ref_type t
+  | BotT -> "(something)"
+
+let string_of_result_type : result_type -> string = function
+  | ts -> "[" ^ String.concat " " (List.map string_of_val_type ts) ^ "]"
+
+let string_of_func_type : func_type -> string = function
+  | FuncT (ts1, ts2) ->
+    string_of_result_type ts1 ^ " -> " ^ string_of_result_type ts2
+
+let string_of_cont_type = function
+  | ContT x -> string_of_var x
+
+let string_of_def_type : def_type -> string = function
+  | DefFuncT ft -> "func " ^ string_of_func_type ft
+  | DefContT ct -> "cont " ^ string_of_cont_type ct
+
+let string_of_tag_type (TagT x) = string_of_var x
+
+let string_of_limits : I32.t limits -> string = function
+  | {min; max} ->
+    I32.to_string_u min ^
+    (match max with None -> "" | Some n -> " " ^ I32.to_string_u n)
+
+let string_of_memory_type : memory_type -> string = function
+  | MemoryT lim -> string_of_limits lim
+
+let string_of_table_type : table_type -> string = function
+  | TableT (lim, t) -> string_of_limits lim ^ " " ^ string_of_ref_type t
+
+let string_of_global_type : global_type -> string = function
+  | GlobalT (Cons, t) -> string_of_val_type t
+  | GlobalT (Var, t) -> "(mut " ^ string_of_val_type t ^ ")"
+
+let string_of_local_type : local_type -> string = function
+  | LocalT (Set, t) -> string_of_val_type t
+  | LocalT (Unset, t) -> "(unset " ^ string_of_val_type t ^ ")"
+
 let string_of_extern_type : extern_type -> string = function
   | ExternFuncT ft -> "func " ^ string_of_func_type ft
   | ExternTableT tt -> "table " ^ string_of_table_type tt
@@ -132,11 +198,6 @@ let string_of_module_type : module_type -> string = function
       List.map (fun et -> "export " ^ string_of_export_type et ^ "\n") ets
     )
 
-let string_of_tag_type (TagT x) = string_of_var x
-
-let string_of_cont_type = function
-  | ContT x -> string_of_var x
-
 (* Dynamic Types *)
 
 type type_addr += Addr of def_type Lib.Promise.t
@@ -238,3 +299,25 @@ let dyn_module_type = function
     let its = List.map (dyn_import_type c) its in
     let ets = List.map (dyn_export_type c) ets in
     ModuleT ([], its, ets)
+
+(* Projections *)
+let as_stat_var = function
+  | Stat x -> x
+  | Dyn _ -> assert false
+
+let as_dyn_var = function
+  | Dyn a -> a
+  | Stat _ -> assert false
+
+let as_func_def_type (dt : def_type) : func_type =
+  match dt with
+  | DefFuncT ft -> ft
+  | _ -> assert false
+
+let as_cont_def_type (dt : def_type) : cont_type =
+  match dt with
+  | DefContT ct -> ct
+  | _ -> assert false
+
+let extern_type_of_import_type (ImportT (et, _, _)) = et
+let extern_type_of_export_type (ExportT (et, _)) = et
diff --git a/interpreter/text/arrange.ml b/interpreter/text/arrange.ml
index b4e6914e..2b2bfc43 100644
--- a/interpreter/text/arrange.ml
+++ b/interpreter/text/arrange.ml
@@ -576,7 +576,7 @@ let memory off i mem =
   Node ("memory $" ^ nat (off + i) ^ " " ^ limits nat32 lim, [])
 
 let tag off i tag =
-  let {tagtype = TagType x} = tag.it in
+  let {tagtype = TagT x} = tag.it in
   Node ("tag $" ^ nat (off + i),
     [Node ("type", [atom var_type x])]
   )
diff --git a/interpreter/text/lexer.mll b/interpreter/text/lexer.mll
index e985ca07..def5aeb9 100644
--- a/interpreter/text/lexer.mll
+++ b/interpreter/text/lexer.mll
@@ -154,6 +154,7 @@ rule token = parse
       | "ref" -> REF
       | "null" -> NULL
       | "mut" -> MUT
+      | "tag" -> TAG
       | "cont" -> CONT
 
       | "nop" -> NOP
@@ -711,6 +712,8 @@ rule token = parse
       | "assert_return" -> ASSERT_RETURN
       | "assert_trap" -> ASSERT_TRAP
       | "assert_exhaustion" -> ASSERT_EXHAUSTION
+      | "assert_exception" -> ASSERT_EXCEPTION
+      | "assert_suspension" -> ASSERT_SUSPENSION
       | "nan:canonical" -> NAN Script.CanonicalNan
       | "nan:arithmetic" -> NAN Script.ArithmeticNan
       | "input" -> INPUT
diff --git a/interpreter/text/parser.conflicts b/interpreter/text/parser.conflicts
deleted file mode 100644
index e69de29b..00000000
diff --git a/interpreter/text/parser.mly b/interpreter/text/parser.mly
index e974d0e6..b51ff684 100644
--- a/interpreter/text/parser.mly
+++ b/interpreter/text/parser.mly
@@ -163,7 +163,7 @@ let label (c : context) x = lookup "label " c.labels x
 let func_type (c : context) x =
   match (Lib.List32.nth c.types.list x.it).it with
   | DefFuncT ft -> ft
-  | DefContT ct -> ct
+  | _ -> error x.at ("non-function type " ^ Int32.to_string x.it)
   | exception Failure _ -> error x.at ("unknown type " ^ Int32.to_string x.it)
 
 let handlers (c : context) h =
@@ -263,7 +263,7 @@ let inline_func_type_explicit (c : context) x ft at =
 %token<Ast.instr'> VEC_SHIFT VEC_BITMASK VEC_SPLAT
 %token VEC_SHUFFLE
 %token<int -> Ast.instr'> VEC_EXTRACT VEC_REPLACE
-%token FUNC START TYPE PARAM RESULT LOCAL GLOBAL TAG
+%token FUNC START TYPE PARAM RESULT LOCAL GLOBAL TAG CONT
 %token TABLE ELEM MEMORY DATA DECLARE OFFSET ITEM IMPORT EXPORT
 %token MODULE BIN QUOTE
 %token SCRIPT REGISTER INVOKE GET
@@ -321,15 +321,15 @@ global_type :
 
 def_type :
   | LPAR FUNC func_type RPAR { fun c -> DefFuncT ($3 c) }
-  | LPAR CONT cont_type RPAR { fun c -> DefContT (ContT (SynVar ($3 c).it)) }
+  | LPAR CONT cont_type RPAR { fun c -> DefContT (ContT (Stat ($3 c).it)) }
 
 cont_type :
   | type_use cont_type_params
     { let at1 = ati 1 in
       fun c ->
       match $2 c with
-      | FuncType ([], []) -> $1 c type_
-      | ft -> inline_func_type_explicit c ($1 c type_) ft at1 }
+      | FuncT ([], []) -> $1 c
+      | ft -> inline_func_type_explicit c ($1 c) ft at1 }
   | cont_type_params
     /* TODO: the inline type is broken for now */
     { let at = at () in fun c -> inline_func_type c ($1 c) at }
@@ -337,19 +337,18 @@ cont_type :
     { fun c -> $1 c type_ }
 
 cont_type_params :
-  | LPAR PARAM value_type_list RPAR cont_type_params
-    { fun c -> let FuncType (ts1, ts2) = $5 c in
-      FuncType (snd $3 c @ ts1, ts2) }
+  | LPAR PARAM val_type_list RPAR cont_type_params
+    { fun c -> let FuncT (ts1, ts2) = $5 c in
+      FuncT (snd $3 c @ ts1, ts2) }
   | cont_type_results
-    { fun c -> FuncType ([], $1 c) }
+    { fun c -> FuncT ([], $1 c) }
 
 cont_type_results :
-  | LPAR RESULT value_type_list RPAR cont_type_results
+  | LPAR RESULT val_type_list RPAR cont_type_results
     { fun c -> snd $3 c @ $5 c }
   | /* empty */
     { fun c -> [] }
 
-
 func_type :
   | func_type_result
     { fun c -> FuncT ([], $1 c) }
@@ -368,9 +367,9 @@ func_type_result :
 
 tag_type :
   | type_use
-    { fun c -> TagType (SynVar ($1 c type_).it) }
+    { fun c -> TagT (Stat ($1 c).it) }
   | func_type
-    { let at = at () in fun c -> TagType (SynVar (inline_func_type c ($1 c) at).it) }
+    { let at = at () in fun c -> TagT (Stat (inline_func_type c ($1 c) at).it) }
 
 table_type :
   | limits ref_type { fun c -> TableT ($1, $2 c) }
@@ -631,16 +630,15 @@ catch :
 catch_all :
   | CATCH_ALL instr_list { $2 }
 
-resume_instr :
-  | RESUME resume_instr_handler
-    { let at = at () in fun c -> resume ($2 c) @@ at }
-
-resume_instr_handler :
-  | LPAR TAG var var RPAR resume_instr_handler
-    { fun c -> ($3 c tag, $4 c label) :: $6 c }
-  | /* empty */
-    { fun c -> [] }
+/* resume_instr : */
+/*   | RESUME resume_instr_handler */
+/*     { let at = at () in fun c -> resume ($2 c) @@ at } */
 
+/* resume_instr_handler : */
+/*   | LPAR TAG var var RPAR resume_instr_handler */
+/*     { fun c -> ($3 c tag, $4 c label) :: $6 c } */
+/*   | /\* empty *\/ */
+/*     { fun c -> [] } */
 
 resume_instr_instr :
   | RESUME resume_instr_handler_instr
@@ -650,10 +648,9 @@ resume_instr_instr :
 resume_instr_handler_instr :
   | LPAR TAG var var RPAR resume_instr_handler_instr
     { fun c -> let hs, es = $6 c in ($3 c tag, $4 c label) :: hs, es }
-  | instr
+  | instr1
     { fun c -> [], $1 c }
 
-
 block_instr :
   | BLOCK labeling_opt block END labeling_end_opt
     { fun c -> let c' = $2 c $5 in let bt, es = $3 c' in block bt es }
@@ -812,7 +809,7 @@ try_block :
     { let at = at () in
       fun c c' ->
       let body = $2 c in
-      let bt = VarBlockType (SynVar (inline_func_type_explicit c' ($1 c' type_) (fst body) at).it) in
+      let bt = VarBlockType (inline_func_type_explicit c' ($1 c') (fst body) at) in
       snd body bt c c' }
   | try_block_param_body  /* Sugar */
     { let at = at () in
@@ -822,19 +819,19 @@ try_block :
         match fst body with
         | FuncT ([], []) -> ValBlockType None
         | FuncT ([], [t]) -> ValBlockType (Some t)
-        | ft ->  VarBlockT (SynVar (inline_func_type c' ft at).it)
+        | ft ->  VarBlockType (inline_func_type c' ft at)
       in snd body bt c c' }
 
 try_block_param_body :
   | try_block_result_body { $1 }
-  | LPAR PARAM value_type_list RPAR try_block_param_body
+  | LPAR PARAM val_type_list RPAR try_block_param_body
     { fun c ->
       let FuncT (ins, out) = fst ($5 c) in
       FuncT ((snd $3) c @ ins, out), snd ($5 c) }
 
 try_block_result_body :
   | try_ { fun _c -> FuncT ([], []), $1 }
-  | LPAR RESULT value_type_list RPAR try_block_result_body
+  | LPAR RESULT val_type_list RPAR try_block_result_body
     { fun c ->
       let FuncT (ins, out) = fst ($5 c) in
       let vs = (snd $3) c in
diff --git a/interpreter/valid/match.ml b/interpreter/valid/match.ml
index b00adfd5..7bc1a0f5 100644
--- a/interpreter/valid/match.ml
+++ b/interpreter/valid/match.ml
@@ -64,7 +64,8 @@ and eq_cont_type c (ContT x1) (ContT x2) =
 and eq_def_type c dt1 dt2 =
   match dt1, dt2 with
   | DefFuncT ft1, DefFuncT ft2 -> eq_func_type c ft1 ft2
-  | DefContT ct1, ContDefT ct2 -> eq_cont_type c ct1 ct2
+  | DefContT ct1, DefContT ct2 -> eq_cont_type c ct1 ct2
+  | _, _ -> false
 
 and eq_var_type c x1 x2 =
   eq_var x1 x2 ||
@@ -80,7 +81,7 @@ let eq_memory_type c (MemoryT lim1) (MemoryT lim2) =
 let eq_global_type c (GlobalT (mut1, t1)) (GlobalT (mut2, t2)) =
   eq_mutability c mut1 mut2 && eq_val_type c t1 t2
 
-and eq_tag_type c (TagT x1) (TagT x2) =
+let eq_tag_type c (TagT x1) (TagT x2) =
   eq_var_type c x1 x2
 
 let eq_extern_type c et1 et2 =
@@ -147,6 +148,8 @@ and match_func_type c ft1 ft2 =
 and match_def_type c dt1 dt2 =
   match dt1, dt2 with
   | DefFuncT ft1, DefFuncT ft2 -> match_func_type c ft1 ft2
+  | DefContT ct1, DefContT ct2 -> match_cont_type c ct1 ct2
+  | _, _ -> false
 
 and match_var_type c x1 x2 =
   eq_var x1 x2 ||
@@ -167,8 +170,8 @@ let match_global_type c (GlobalT (mut1, t1)) (GlobalT (mut2, t2)) =
   | Cons -> match_val_type c t1 t2
   | Var -> eq_val_type c t1 t2
 
-and match_tag_type c (TagT x1) (TagT x2) =
-  match_var_type c x1 x2
+let match_tag_type c tt1 tt2 =
+  eq_tag_type c tt1 tt2
 
 let match_extern_type c et1 et2 =
   match et1, et2 with
diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml
index 3f81e49f..0eeb0bea 100644
--- a/interpreter/valid/valid.ml
+++ b/interpreter/valid/valid.ml
@@ -76,9 +76,6 @@ let cont_type (c : context) x =
   | DefContT ct -> ct
   | _ -> error x.at ("non-continuation type " ^ Int32.to_string x.it)
 
-
-let func (c : context) x = func_type c (func_var c x @@ x.at)
-
 let refer category (s : Free.Set.t) x =
   if not (Free.Set.mem x.it s) then
     error x.at
@@ -133,7 +130,7 @@ let check_func_type (c : context) (ft : func_type) at =
 
 let check_cont_type (c : context) (ct : cont_type) at =
   let ContT x = ct in
-  ignore (func_type c (as_syn_var x @@ at))
+  ignore (func_type c (as_stat_var x @@ at))
 
 let check_table_type (c : context) (tt : table_type) at =
   let TableT (lim, t) = tt in
@@ -146,8 +143,8 @@ let check_memory_type (c : context) (mt : memory_type) at =
     "memory size must be at most 65536 pages (4GiB)"
 
 let check_tag_type (c : context) (et : tag_type) at =
-  let TagType x = et in
-  ignore (func_type c (as_syn_var x @@ at))
+  let TagT x = et in
+  ignore (func_type c (as_stat_var x @@ at))
 
 let check_global_type (c : context) (gt : global_type) at =
   let GlobalT (_mut, t) = gt in
@@ -178,6 +175,7 @@ type infer_instr_type = infer_func_type * idx list
 
 let stack ts = (NoEllipses, ts)
 let (-->) ts1 ts2 = {ins = NoEllipses, ts1; outs = NoEllipses, ts2}
+let (-->..) ts1 ts2 = {ins = Ellipses, ts1; outs = NoEllipses, ts2}
 let (-->...) ts1 ts2 = {ins = Ellipses, ts1; outs = Ellipses, ts2}
 
 let check_stack (c : context) ts1 ts2 at =
@@ -360,72 +358,76 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_in
 
   | Block (bt, es) ->
     let InstrT (ts1, ts2, xs) as it = check_block_type c bt e.at in
-    check_block {c with labels = ts2 :: c.labels} es it e.at;
+    check_block {c with labels = (BlockLabel, ts2) :: c.labels} es it e.at;
     ts1 --> ts2, List.map (fun x -> x @@ e.at) xs
 
   | Loop (bt, es) ->
     let InstrT (ts1, ts2, xs) as it = check_block_type c bt e.at in
-    check_block {c with labels = ts1 :: c.labels} es it e.at;
+    check_block {c with labels = (BlockLabel, ts1) :: c.labels} es it e.at;
     ts1 --> ts2, List.map (fun x -> x @@ e.at) xs
 
   | If (bt, es1, es2) ->
     let InstrT (ts1, ts2, xs) as it = check_block_type c bt e.at in
-    check_block {c with labels = ts2 :: c.labels} es1 it e.at;
-    check_block {c with labels = ts2 :: c.labels} es2 it e.at;
+    check_block {c with labels = (BlockLabel, ts2) :: c.labels} es1 it e.at;
+    check_block {c with labels = (BlockLabel, ts2) :: c.labels} es2 it e.at;
     (ts1 @ [NumT I32T]) --> ts2, List.map (fun x -> x @@ e.at) xs
 
   | Throw x ->
-    let TagType y = tag c x in
-    let FuncType (ts1, _) = func_type c (as_syn_var y @@ e.at) in
-    ts1 -->... []
+    let TagT y = tag c x in
+    let FuncT (ts1, _) = func_type c (as_stat_var y @@ e.at) in
+    ts1 -->... [], []
 
   | Rethrow x ->
     let (kind, _) = label c x in
     require (kind = CatchLabel) e.at "invalid rethrow label";
-    [] -->... []
+    [] -->... [], []
 
   | TryCatch (bt, es, cts, ca) ->
-    let FuncType (ts1, ts2) as ft = check_block_type c bt e.at in
+    let InstrT (ts1, ts2, xs) as ft = check_block_type c bt e.at in
     let c_try = {c with labels = (BlockLabel, ts2) :: c.labels} in
     let c_catch = {c with labels = (CatchLabel, ts2) :: c.labels} in
     check_block c_try es ft e.at;
     List.iter (fun ct -> check_catch ct c_catch ft e.at) cts;
     Lib.Option.app (fun es -> check_block c_catch es ft e.at) ca;
-    ts1 --> ts2
+    ts1 --> ts2, List.map (fun x -> x @@ e.at) xs
 
   | TryDelegate (bt, es, x) ->
-    let FuncType (ts1, ts2) as ft = check_block_type c bt e.at in
+    let InstrT (ts1, ts2, xs) as ft = check_block_type c bt e.at in
     ignore (label c x);
     check_block {c with labels = (BlockLabel, ts2) :: c.labels} es ft e.at;
-    ts1 --> ts2
+    ts1 --> ts2, List.map (fun x -> x @@ e.at) xs
 
   | Br x ->
-    label c x -->... [], []
+    let (_, ts) = label c x in
+    ts -->... [], []
 
   | BrIf x ->
-    (label c x @ [NumT I32T]) --> label c x, []
+    let (_, ts) = label c x in
+    (ts @ [NumT I32T]) --> ts, []
 
   | BrTable (xs, x) ->
-    let n = List.length (label c x) in
+    let n = List.length (snd (label c x)) in
     let ts = Lib.List.table n (fun i -> peek (n - i) s) in
-    check_stack c ts (label c x) x.at;
-    List.iter (fun x' -> check_stack c ts (label c x') x'.at) xs;
+    check_stack c ts (snd (label c x)) x.at;
+    List.iter (fun x' -> check_stack c ts (snd (label c x')) x'.at) xs;
     (ts @ [NumT I32T]) -->... [], []
 
   | BrOnNull x ->
     let (_, ht) = peek_ref 0 s e.at in
-    (label c x @ [RefT (Null, ht)]) --> (label c x @ [RefT (NoNull, ht)]), []
+    let (_, ts) = label c x in
+    (ts @ [RefT (Null, ht)]) --> (ts @ [RefT (NoNull, ht)]), []
 
   | BrOnNonNull x ->
     let (_, ht) = peek_ref 0 s e.at in
     let t' = RefT (NoNull, ht) in
-    require (label c x <> []) e.at
+    let (_, ts) = label c x in
+    require (ts <> []) e.at
       ("type mismatch: instruction requires type " ^ string_of_val_type t' ^
-       " but label has " ^ string_of_result_type (label c x));
-    let ts0, t1 = Lib.List.split_last (label c x) in
+       " but label has " ^ string_of_result_type ts);
+    let ts0, t1 = Lib.List.split_last ts in
     require (match_val_type c.types t' t1) e.at
       ("type mismatch: instruction requires type " ^ string_of_val_type t' ^
-       " but label has " ^ string_of_result_type (label c x));
+       " but label has " ^ string_of_result_type ts);
     (ts0 @ [RefT (Null, ht)]) --> ts0, []
 
   | Return ->
@@ -474,86 +476,86 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_in
 
   | ContNew x ->
     let ContT y = cont_type c x in
-    [RefType (NonNullable, DefHeapType y)] -->
-    [RefType (NonNullable, DefHeapType (SynVar x.it))]
+    [RefT (NoNull, DefHT y)] -->
+    [RefT (NoNull, DefHT (Stat x.it))], []
 
   | ContBind x ->
     (match peek_ref 0 s e.at with
-    | nul, DefHeapType (SynVar y) ->
+    | nul, DefHT (Stat y) ->
       let ContT z = cont_type c (y @@ e.at) in
-      let FuncT (ts1, ts2) = func_type c (as_syn_var z @@ e.at) in
+      let FuncT (ts1, ts2) = func_type c (as_stat_var z @@ e.at) in
       let ContT z' = cont_type c x in
-      let FuncT (ts1', _) as ft' = func_type c (as_syn_var z' @@ x.at) in
+      let FuncT (ts1', _) as ft' = func_type c (as_stat_var z' @@ x.at) in
       require (List.length ts1 >= List.length ts1') x.at
         "type mismatch in continuation arguments";
       let ts11, ts12 = Lib.List.split (List.length ts1 - List.length ts1') ts1 in
-      require (match_func_type c.types [] (FuncType (ts12, ts2)) ft') e.at
+      require (match_func_type c.types (FuncT (ts12, ts2)) ft') e.at
         "type mismatch in continuation type";
-      (ts11 @ [RefType (nul, DefHeapType (SynVar y))]) -->
-        [RefType (NonNullable, DefHeapType (SynVar x.it))]
-    | (_, BotHeapType) as rt ->
-      [RefType rt] -->.. [RefType (NonNullable, DefHeapType (SynVar x.it))]
+      (ts11 @ [RefT (nul, DefHT (Stat y))]) -->
+        [RefT (NoNull, DefHT (Stat x.it))], []
+    | (_, BotHT) as rt ->
+      [RefT rt] -->.. [RefT (NoNull, DefHT (Stat x.it))], []
     | rt ->
       error e.at
         ("type mismatch: instruction requires continuation reference type" ^
-         " but stack has " ^ string_of_value_type (RefType rt))
+         " but stack has " ^ string_of_val_type (RefT rt))
     )
 
   | Suspend x ->
     let TagT x' = tag c x in
-    let FuncT (ts1, ts2) = func_type c (as_syn_var x' @@ x.at) in
-    ts1 --> ts2
+    let FuncT (ts1, ts2) = func_type c (as_stat_var x' @@ x.at) in
+    ts1 --> ts2, []
 
   | Resume xys ->
     (match peek_ref 0 s e.at with
-    | nul, DefHeapType (SynVar y) ->
+    | nul, DefHT (Stat y) ->
       let ContT z = cont_type c (y @@ e.at) in
-      let FuncT (ts1, ts2) = func_type c (as_syn_var z @@ e.at) in
+      let FuncT (ts1, ts2) = func_type c (as_stat_var z @@ e.at) in
       List.iter (fun (x1, x2) ->
         let TagT x1' = tag c x1 in
-        let FuncT (ts3, ts4) = func_type c (as_syn_var x1' @@ x1.at) in
+        let FuncT (ts3, ts4) = func_type c (as_stat_var x1' @@ x1.at) in
         let (_, ts') = label c x2 in
         match Lib.List.last_opt ts'  with
-        | Some (RefType (nul', DefHeapType (SynVar y'))) ->
+        | Some (RefT (nul', DefHT (Stat y'))) ->
           let ContT z' = cont_type c (y' @@ x2.at) in
-          let ft' = func_type c (as_syn_var z' @@ x2.at) in
-          require (match_func_type c.types [] (FuncType (ts4, ts2)) ft') x2.at
+          let ft' = func_type c (as_stat_var z' @@ x2.at) in
+          require (match_func_type c.types (FuncT (ts4, ts2)) ft') x2.at
             "type mismatch in continuation type";
-          check_stack c (ts3 @ [RefType (nul', DefHeapType (SynVar y'))]) ts' x2.at
+          check_stack c (ts3 @ [RefT (nul', DefHT (Stat y'))]) ts' x2.at
         | _ ->
          error e.at
            ("type mismatch: instruction requires continuation reference type" ^
             " but label has " ^ string_of_result_type ts')
       ) xys;
-      (ts1 @ [RefType (nul, DefHeapType (SynVar y))]) --> ts2
-    | _, BotHeapType ->
-      [] -->... []
+      (ts1 @ [RefT (nul, DefHT (Stat y))]) --> ts2, []
+    | _, BotHT ->
+      [] -->... [], []
     | rt ->
       error e.at
         ("type mismatch: instruction requires continuation reference type" ^
-         " but stack has " ^ string_of_value_type (RefType rt))
+         " but stack has " ^ string_of_val_type (RefT rt))
     )
 
   | ResumeThrow x ->
     let TagT x' = tag c x in
-    let FuncT (ts0, _) = func_type c (as_syn_var x' @@ x.at) in
+    let FuncT (ts0, _) = func_type c (as_stat_var x' @@ x.at) in
     (match peek_ref 0 s e.at with
-    | nul, DefHeapType (SynVar y) ->
+    | nul, DefHT (Stat y) ->
       let ContT z = cont_type c (y @@ e.at) in
-      let FuncT (ts1, ts2) = func_type c (as_syn_var z @@ e.at) in
-      (ts0 @ [RefType (nul, DefHeapType (SynVar y))]) --> ts2
-    | _, BotHeapType ->
-      [] -->... []
+      let FuncT (ts1, ts2) = func_type c (as_stat_var z @@ e.at) in
+      (ts0 @ [RefT (nul, DefHT (Stat y))]) --> ts2, []
+    | _, BotHT ->
+      [] -->... [], []
     | rt ->
       error e.at
         ("type mismatch: instruction requires continuation reference type" ^
-         " but stack has " ^ string_of_value_type (RefType rt))
+         " but stack has " ^ string_of_val_type (RefT rt))
     )
 
   | Barrier (bt, es) ->
-    let FuncT (ts1, ts2) as ft = check_block_type c bt e.at in
+    let InstrT (ts1, ts2, xs) as ft = check_block_type c bt e.at in
     check_block {c with labels = (BlockLabel, ts2) :: c.labels} es ft e.at;
-    ts1 --> ts2
+    ts1 --> ts2, List.map (fun x -> x @@ e.at) xs
 
   | LocalGet x ->
     let LocalT (init, t) = local c x in
@@ -799,12 +801,12 @@ and check_block (c : context) (es : instr list) (it : instr_type) at =
     ("type mismatch: block requires " ^ string_of_result_type ts2 ^
      " but stack has " ^ string_of_result_type (snd s))
 
-and check_catch (ct : idx * instr list) (c : context) (ft : func_type) at =
+and check_catch (ct : idx * instr list) (c : context) (ft : instr_type) at =
   let (x, es) = ct in
-  let TagType y = tag c x in
-  let FuncType (ts1, _) = func_type c (as_syn_var y @@ at) in
-  let FuncType (_, ts2) = ft in
-  check_block c es (FuncType (ts1, ts2)) at
+  let TagT y = tag c x in
+  let FuncT (ts1, _) = func_type c (as_stat_var y @@ at) in
+  let InstrT (_, ts2, xs) = ft in
+  check_block c es (InstrT (ts1, ts2, xs)) at
 
 (* Functions & Constants *)
 
@@ -933,7 +935,7 @@ let check_import (c : context) (im : import) : context =
     {c with globals = c.globals @ [gt]}
   | TagImport et ->
     check_tag_type c et idesc.at;
-    {c with tags = et :: c.tags}
+    {c with tags = c.tags @ [et]}
 
 module NameSet = Set.Make(struct type t = Ast.name let compare = compare end)
 
diff --git a/test/core/cont.wast b/test/core/cont.wast
index 6830c9e3..ae02ae2e 100644
--- a/test/core/cont.wast
+++ b/test/core/cont.wast
@@ -204,7 +204,7 @@
   (func $gen (export "start") (param $i i64)
     (loop $l
       (br_if 1 (suspend $yield (local.get $i)))
-      (call_ref (local.get $i) (global.get $hook))
+      (call_ref $gen (local.get $i) (global.get $hook))
       (local.set $i (i64.add (local.get $i) (i64.const 1)))
       (br $l)
     )