diff --git a/interpreter/binary/decode.ml b/interpreter/binary/decode.ml
index 2e66bfc8..9ab6ced8 100644
--- a/interpreter/binary/decode.ml
+++ b/interpreter/binary/decode.ml
@@ -249,10 +249,16 @@ let memop s =
   Int32.to_int align, offset
 
 let block_type s =
+  let xs =
+    either [
+      (fun s -> expect 0x41 s ""; vec (at var));
+      (fun s -> fun _ -> []);
+    ] s s
+  in
   either [
-    (fun s -> VarBlockType (var_type s));
-    (fun s -> expect 0x40 s ""; ValBlockType None);
-    (fun s -> ValBlockType (Some (value_type s)));
+    (fun s -> VarBlockType (var_type s, xs));
+    (fun s -> expect 0x40 s ""; ValBlockType (None, xs));
+    (fun s -> ValBlockType (Some (value_type s), xs));
   ] s
 
 let local s =
diff --git a/interpreter/binary/encode.ml b/interpreter/binary/encode.ml
index 1553dc71..656e6e00 100644
--- a/interpreter/binary/encode.ml
+++ b/interpreter/binary/encode.ml
@@ -165,10 +165,13 @@ struct
   let var x = u32 x.it
 
   let block_type = function
-    | ValBlockType None -> s33 (-0x40l)
-    | ValBlockType (Some t) -> value_type t
-    | VarBlockType (SynVar x) -> s33 x
-    | VarBlockType (SemVar _) -> assert false
+    | ValBlockType (None, []) -> s33 (-0x40l)
+    | ValBlockType (Some t, []) -> value_type t
+    | VarBlockType (SynVar x, []) -> s33 x
+    | ValBlockType (None, xs) -> s33 (-0x3fl); vec var xs; s33 (-0x40l)
+    | ValBlockType (Some t, xs) -> s33 (-0x3fl); vec var xs; value_type t
+    | VarBlockType (SynVar x, xs) -> s33 (-0x3fl); vec var xs; s33 x
+    | VarBlockType (SemVar _, _) -> assert false
 
   let local (t, n) = len n; value_type t.it
 
diff --git a/interpreter/exec/eval.ml b/interpreter/exec/eval.ml
index 57a714d9..2e6acfce 100644
--- a/interpreter/exec/eval.ml
+++ b/interpreter/exec/eval.ml
@@ -49,7 +49,7 @@ type 'a stack = 'a list
 type frame =
 {
   inst : module_inst;
-  locals : value ref list;
+  locals : value option ref list;
 }
 
 type code = value stack * admin_instr list
@@ -74,8 +74,8 @@ type config =
   budget : int;  (* to model stack overflow *)
 }
 
-let frame inst = {inst; locals = []}
-let config inst vs es = {frame = frame inst; code = vs, es; budget = 300}
+let frame inst locals = {inst; locals}
+let config inst vs es = {frame = frame inst []; code = vs, es; budget = 300}
 
 let plain e = Plain e.it @@ e.at
 
@@ -111,10 +111,10 @@ let func_ref inst x i at =
 
 let block_type inst bt at =
   match bt with
-  | ValBlockType None -> FuncType ([], [])
-  | ValBlockType (Some t) -> FuncType ([], [t])
-  | VarBlockType (SynVar x) -> func_type inst (x @@ at)
-  | VarBlockType (SemVar x) -> as_func_def_type (def_of x)
+  | ValBlockType (None, _) -> FuncType ([], [])
+  | ValBlockType (Some t, _) -> FuncType ([], [t])
+  | VarBlockType (SynVar x, _) -> func_type inst (x @@ at)
+  | VarBlockType (SemVar x, _) -> as_func_def_type (def_of x)
 
 let take n (vs : 'a stack) at =
   try Lib.List.take n vs with Failure _ -> Crash.error at "stack underflow"
@@ -279,14 +279,19 @@ let rec step (c : config) : config =
           v1 :: vs', []
 
       | LocalGet x, vs ->
-        !(local c.frame x) :: vs, []
+        (match !(local c.frame x) with
+        | Some v ->
+          v :: vs, []
+        | None ->
+          Crash.error e.at "read of uninitialized local"
+        )
 
       | LocalSet x, v :: vs' ->
-        local c.frame x := v;
+        local c.frame x := Some v;
         vs', []
 
       | LocalTee x, v :: vs' ->
-        local c.frame x := v;
+        local c.frame x := Some v;
         v :: vs', []
 
       | GlobalGet x, vs ->
@@ -655,7 +660,7 @@ let rec step (c : config) : config =
 
       | _ ->
         let s1 = string_of_values (List.rev vs) in
-        let s2 = string_of_result_type (List.map type_of_value (List.rev vs)) in
+        let s2 = string_of_value_types (List.map type_of_value (List.rev vs)) in
         Crash.error e.at
           ("missing or ill-typed operand on stack (" ^ s1 ^ " : " ^ s2 ^ ")")
       )
@@ -696,9 +701,11 @@ let rec step (c : config) : config =
       vs' @ vs, [e']
 
     | Local (n, vs0, code'), vs ->
-      let frame' = {c.frame with locals = List.map ref vs0 @ c.frame.locals} in
+      let locals = List.map (fun v -> ref (Some v)) vs0 in
+      let frame' = {c.frame with locals = locals @ c.frame.locals} in
       let c' = step {c with frame = frame'; code = code'} in
-      let vs0' = List.map (!) (take (List.length vs0) c'.frame.locals e.at) in
+      let vs0' = List.map (fun loc -> Option.get (!loc))
+        (take (List.length vs0) c'.frame.locals e.at) in
       vs, [Local (n, vs0', c'.code) @@ e.at]
 
     | Frame (n, frame', (vs', [])), vs ->
@@ -723,17 +730,17 @@ let rec step (c : config) : config =
 
     | Invoke f, vs ->
       let FuncType (ts1, ts2) = Func.type_of f in
-      let args, vs' = split (List.length ts1) vs e.at in
+      let n1, n2 = List.length ts1, List.length ts2 in
+      let args, vs' = split n1 vs e.at in
       (match f with
       | Func.AstFunc (_, inst', func) ->
         let {locals; body; _} = func.it in
         let m = Lib.Promise.value inst' in
         let ts = List.map (fun t -> Types.sem_value_type m.types t.it) locals in
-        let vs0 = List.rev args @ List.map default_value ts in
-        let locals' = List.map (fun t -> t @@ func.at) ts1 @ locals in
-        let bt = VarBlockType (SemVar (alloc (FuncDefType (FuncType ([], ts2))))) in
-        let es0 = [Plain (Let (bt, locals', body)) @@ func.at] in
-        vs', [Frame (List.length ts2, frame m, (List.rev vs0, es0)) @@ e.at]
+        let locals' = List.rev (List.map Option.some args) @ List.map default_value ts in
+        let frame' = {inst = m; locals = List.map ref locals'} in
+        let instr' = [Label (n2, [], ([], List.map plain body)) @@ func.at] in
+        vs', [Frame (n2, frame', ([], instr')) @@ e.at]
 
       | Func.HostFunc (_, f) ->
         (try List.rev (f (List.rev args)) @ vs', []
diff --git a/interpreter/host/spectest.ml b/interpreter/host/spectest.ml
index 309fa3d1..c76317bb 100644
--- a/interpreter/host/spectest.ml
+++ b/interpreter/host/spectest.ml
@@ -29,10 +29,10 @@ let print_value v =
   Printf.printf "%s : %s\n"
     (string_of_value v) (string_of_value_type (type_of_value v))
 
-let print (FuncType (_, out)) vs =
+let print _ vs =
   List.iter print_value vs;
   flush_all ();
-  List.map default_value out
+  []
 
 
 let lookup name t =
diff --git a/interpreter/runtime/value.ml b/interpreter/runtime/value.ml
index 48fe6463..e323a1ce 100644
--- a/interpreter/runtime/value.ml
+++ b/interpreter/runtime/value.ml
@@ -133,22 +133,22 @@ let eq v1 v2 =
 (* Defaults *)
 
 let default_num = function
-  | I32Type -> I32 I32.zero
-  | I64Type -> I64 I64.zero
-  | F32Type -> F32 F32.zero
-  | F64Type -> F64 F64.zero
+  | I32Type -> Some (Num (I32 I32.zero))
+  | I64Type -> Some (Num (I64 I64.zero))
+  | F32Type -> Some (Num (F32 F32.zero))
+  | F64Type -> Some (Num (F64 F64.zero))
 
 let default_vec = function
-  | V128Type -> V128 V128.zero
+  | V128Type -> Some (Vec (V128 V128.zero))
 
 let default_ref = function
-  | (Nullable, t) -> NullRef t
-  | (NonNullable, _) -> assert false
+  | (Nullable, t) -> Some (Ref (NullRef t))
+  | (NonNullable, _) -> None
 
 let default_value = function
-  | NumType t' -> Num (default_num t')
-  | VecType t' -> Vec (default_vec t')
-  | RefType t' -> Ref (default_ref t')
+  | NumType t' -> default_num t'
+  | VecType t' -> default_vec t'
+  | RefType t' -> default_ref t'
   | BotType -> assert false
 
 
diff --git a/interpreter/script/js.ml b/interpreter/script/js.ml
index 23f3bb65..854a9d22 100644
--- a/interpreter/script/js.ml
+++ b/interpreter/script/js.ml
@@ -427,7 +427,7 @@ let wrap item_name wrap_action wrap_assertion at =
   let edesc = FuncExport item @@ at in
   let exports = [{name = Utf8.decode "run"; edesc} @@ at] in
   let body =
-    [ Block (ValBlockType None, action @ assertion @ [Return @@ at]) @@ at;
+    [ Block (ValBlockType (None, []), action @ assertion @ [Return @@ at]) @@ at;
       Unreachable @@ at ]
   in
   let funcs = [{ftype = 0l @@ at; locals; body} @@ at] in
diff --git a/interpreter/script/run.ml b/interpreter/script/run.ml
index 98faf4c4..adbcc045 100644
--- a/interpreter/script/run.ml
+++ b/interpreter/script/run.ml
@@ -220,7 +220,7 @@ let print_module x_opt m =
 let print_values vs =
   let ts = List.map Value.type_of_value vs in
   Printf.printf "%s : %s\n%!"
-    (Value.string_of_values vs) (Types.string_of_result_type ts)
+    (Value.string_of_values vs) (Types.string_of_value_types ts)
 
 let string_of_nan = function
   | CanonicalNan -> "nan:canonical"
@@ -267,7 +267,7 @@ let string_of_results = function
 let print_results rs =
   let ts = List.map type_of_result rs in
   Printf.printf "%s : %s\n%!"
-    (string_of_results rs) (Types.string_of_result_type ts)
+    (string_of_results rs) (Types.string_of_value_types ts)
 
 
 (* Configuration *)
diff --git a/interpreter/syntax/ast.ml b/interpreter/syntax/ast.ml
index bba6d72c..f3aa0cdb 100644
--- a/interpreter/syntax/ast.ml
+++ b/interpreter/syntax/ast.ml
@@ -137,7 +137,9 @@ type name = Utf8.unicode
 type local = local' Source.phrase
 and local' = value_type
 
-type block_type = VarBlockType of var | ValBlockType of value_type option
+type block_type =
+  | VarBlockType of var * idx list
+  | ValBlockType of value_type option * idx list
 
 type instr = instr' Source.phrase
 and instr' =
diff --git a/interpreter/syntax/free.ml b/interpreter/syntax/free.ml
index f597b28f..ac31305f 100644
--- a/interpreter/syntax/free.ml
+++ b/interpreter/syntax/free.ml
@@ -95,8 +95,8 @@ let def_type = function
   | FuncDefType ft -> func_type ft
 
 let block_type = function
-  | VarBlockType x -> var_type x
-  | ValBlockType t -> opt value_type t
+  | VarBlockType (x, xs) -> var_type x ++ list (fun x -> locals (idx x)) xs
+  | ValBlockType (t, xs) -> opt value_type t ++ list (fun x -> locals (idx x)) xs
 
 let rec instr (e : instr) =
   match e.it with
diff --git a/interpreter/syntax/types.ml b/interpreter/syntax/types.ml
index 3e6c93b4..c42bb274 100644
--- a/interpreter/syntax/types.ml
+++ b/interpreter/syntax/types.ml
@@ -1,11 +1,14 @@
 (* Types *)
 
-type name = int list
+type type_idx = int32
+type local_idx = int32
+type name = Utf8.unicode
 
-and syn_var = int32
+and syn_var = type_idx
 and sem_var = def_type Lib.Promise.t
 and var = SynVar of syn_var | SemVar of sem_var
 
+and init = Initialized | Uninitialized
 and nullability = NonNullable | Nullable
 and num_type = I32Type | I64Type | F32Type | F64Type
 and vec_type = V128Type
@@ -15,8 +18,9 @@ and heap_type =
 and value_type =
   NumType of num_type | VecType of vec_type | RefType of ref_type | BotType
 
-and result_type = value_type list
-and func_type = FuncType of result_type * result_type
+and result_type = ResultType of value_type list * local_idx Source.phrase list
+and instr_type = InstrType of value_type list * value_type list * local_idx Source.phrase list
+and func_type = FuncType of value_type list * value_type list
 and def_type = FuncDefType of func_type
 
 type 'a limits = {min : 'a; max : 'a option}
@@ -24,6 +28,7 @@ type mutability = Immutable | Mutable
 type table_type = TableType of Int32.t limits * ref_type
 type memory_type = MemoryType of Int32.t limits
 type global_type = GlobalType of value_type * mutability
+type local_type = LocalType of value_type * init
 type extern_type =
   | ExternFuncType of func_type
   | ExternTableType of table_type
@@ -207,10 +212,13 @@ let string_of_name n =
   List.iter escape n;
   Buffer.contents b
 
+let string_of_idx x = I32.to_string_u x
+let string_of_local_idx x = string_of_idx x.Source.it
+
 let rec string_of_var =
   let inner = ref false in
   function
-  | SynVar x -> I32.to_string_u x
+  | SynVar x -> string_of_idx x
   | SemVar x ->
     if !inner then "..." else
     ( inner := true;
@@ -249,12 +257,22 @@ and string_of_value_type = function
   | RefType t -> string_of_ref_type t
   | BotType -> "(something)"
 
-and string_of_result_type ts =
+and string_of_value_types ts =
   "[" ^ String.concat " " (List.map string_of_value_type ts) ^ "]"
 
+and string_of_result_type = function
+  | ResultType (ts, xs) ->
+    String.concat " "
+      (string_of_value_types ts :: List.map string_of_local_idx xs)
+
+and stirng_of_instr_type = function
+  | InstrType (ts1, ts2, xs) ->
+    string_of_value_types ts1 ^ " -> " ^
+      string_of_result_type (ResultType (ts2, xs))
+
 and string_of_func_type = function
-  | FuncType (ins, out) ->
-    string_of_result_type ins ^ " -> " ^ string_of_result_type out
+  | FuncType (ts1, ts2) ->
+    string_of_value_types ts1 ^ " -> " ^ string_of_value_types ts2
 
 and string_of_def_type = function
   | FuncDefType ft -> "func " ^ string_of_func_type ft
diff --git a/interpreter/text/arrange.ml b/interpreter/text/arrange.ml
index 18a0a871..7ee1e858 100644
--- a/interpreter/text/arrange.ml
+++ b/interpreter/text/arrange.ml
@@ -429,10 +429,14 @@ let vec v = string_of_vec v.it
 let constop v = num_type (type_of_num v) ^ ".const"
 let vec_constop v = vec_type (type_of_vec v) ^ ".const i32x4"
 
+let inits = function
+  | [] -> []
+  | xs -> [Node ("set " ^ String.concat " " (list var xs), [])]
+
 let block_type = function
-  | VarBlockType (SynVar x) -> [Node ("type " ^ nat32 x, [])]
-  | VarBlockType (SemVar _) -> assert false
-  | ValBlockType ts -> decls "result" (list_of_opt ts)
+  | VarBlockType (SynVar x, xs) -> Node ("type " ^ nat32 x, []) :: inits xs
+  | VarBlockType (SemVar _, _) -> assert false
+  | ValBlockType (ts, xs) -> decls "result" (list_of_opt ts) @ inits xs
 
 let rec instr e =
   let head, inner =
diff --git a/interpreter/text/lexer.mll b/interpreter/text/lexer.mll
index 4678dd37..864a1015 100644
--- a/interpreter/text/lexer.mll
+++ b/interpreter/text/lexer.mll
@@ -152,6 +152,7 @@ rule token = parse
       | "ref" -> REF
       | "null" -> NULL
       | "mut" -> MUT
+      | "set" -> SET
 
       | "nop" -> NOP
       | "unreachable" -> UNREACHABLE
diff --git a/interpreter/text/parser.mly b/interpreter/text/parser.mly
index c1feb01a..6aae073e 100644
--- a/interpreter/text/parser.mly
+++ b/interpreter/text/parser.mly
@@ -241,7 +241,7 @@ let inline_func_type_explicit (c : context) x ft at =
 %token NAT INT FLOAT STRING VAR
 %token NUM_TYPE VEC_TYPE VEC_SHAPE FUNCREF EXTERNREF REF EXTERN NULL MUT
 %token UNREACHABLE NOP DROP SELECT
-%token BLOCK END IF THEN ELSE LOOP LET
+%token BLOCK END IF THEN ELSE LOOP LET SET
 %token BR BR_IF BR_TABLE BR_ON_NULL BR_ON_NON_NULL
 %token CALL CALL_REF CALL_INDIRECT RETURN RETURN_CALL_REF FUNC_BIND
 %token LOCAL_GET LOCAL_SET LOCAL_TEE GLOBAL_GET GLOBAL_SET
@@ -631,31 +631,38 @@ block_instr :
 block :
   | type_use block_param_body
     { let at1 = ati 1 in
-      fun c -> let ft, es = $2 c in
+      fun c -> let ft, xs, es = $2 c in
       let x = inline_func_type_explicit c ($1 c type_) ft at1 in
-      VarBlockType (SynVar x.it), es }
+      VarBlockType (SynVar x.it, xs), es }
   | block_param_body  /* Sugar */
     { let at = at () in
-      fun c -> let ft, es = $1 c in
+      fun c -> let ft, xs, es = $1 c in
       let bt =
         match ft with
-        | FuncType ([], []) -> ValBlockType None
-        | FuncType ([], [t]) -> ValBlockType (Some t)
-        | ft ->  VarBlockType (SynVar (inline_func_type c ft at).it)
+        | FuncType ([], []) -> ValBlockType (None, xs)
+        | FuncType ([], [t]) -> ValBlockType (Some t, xs)
+        | ft ->  VarBlockType (SynVar (inline_func_type c ft at).it, xs)
       in bt, es }
 
 block_param_body :
   | block_result_body { $1 }
   | LPAR PARAM value_type_list RPAR block_param_body
-    { fun c -> let FuncType (ins, out), es = $5 c in
-      FuncType (snd $3 c @ ins, out), es }
+    { fun c -> let FuncType (ins, out), xs, es = $5 c in
+      FuncType (snd $3 c @ ins, out), xs, es }
 
 block_result_body :
-  | instr_list { fun c -> FuncType ([], []), $1 c }
+  | block_set_body
+    { fun c -> let xs, es = $1 c in
+      FuncType ([], []), xs, es }
   | LPAR RESULT value_type_list RPAR block_result_body
-    { fun c ->
-      let FuncType (ins, out), es = $5 c in
-      FuncType (ins, snd $3 c @ out), es }
+    { fun c -> let FuncType (ins, out), xs, es = $5 c in
+      FuncType (ins, snd $3 c @ out), xs, es }
+
+block_set_body :
+  | instr_list { fun c -> [], $1 c }
+  | LPAR SET var_list RPAR block_set_body
+    { fun c -> let xs, es = $5 c in
+      $3 c local @ xs, es }
 
 
 let_block :
@@ -663,15 +670,15 @@ let_block :
     { let at = at () in
       fun c c' -> let ft, ls, es = $2 c c' in
       let x = inline_func_type_explicit c ($1 c type_) ft at in
-      VarBlockType (SynVar x.it), ls, es }
+      VarBlockType (SynVar x.it, []), ls, es }
   | let_block_param_body  /* Sugar */
     { let at = at () in
       fun c c' -> let ft, ls, es = $1 c c' in
       let bt =
         match ft with
-        | FuncType ([], []) -> ValBlockType None
-        | FuncType ([], [t]) -> ValBlockType (Some t)
-        | ft ->  VarBlockType (SynVar (inline_func_type c ft at).it)
+        | FuncType ([], []) -> ValBlockType (None, [])
+        | FuncType ([], [t]) -> ValBlockType (Some t, [])
+        | ft ->  VarBlockType (SynVar (inline_func_type c ft at).it, [])
       in bt, ls, es }
 
 let_block_param_body :
@@ -772,32 +779,40 @@ call_expr_results :
 if_block :
   | type_use if_block_param_body
     { let at = at () in
-      fun c c' -> let ft, es = $2 c c' in
+      fun c c' -> let ft, xs, es = $2 c c' in
       let x = inline_func_type_explicit c ($1 c type_) ft at in
-      VarBlockType (SynVar x.it), es }
+      VarBlockType (SynVar x.it, xs), es }
   | if_block_param_body  /* Sugar */
     { let at = at () in
-      fun c c' -> let ft, es = $1 c c' in
+      fun c c' -> let ft, xs, es = $1 c c' in
       let bt =
         match ft with
-        | FuncType ([], []) -> ValBlockType None
-        | FuncType ([], [t]) -> ValBlockType (Some t)
-        | ft ->  VarBlockType (SynVar (inline_func_type c ft at).it)
+        | FuncType ([], []) -> ValBlockType (None, xs)
+        | FuncType ([], [t]) -> ValBlockType (Some t, xs)
+        | ft ->  VarBlockType (SynVar (inline_func_type c ft at).it, xs)
       in bt, es }
 
 if_block_param_body :
   | if_block_result_body { $1 }
   | LPAR PARAM value_type_list RPAR if_block_param_body
     { fun c c' ->
-      let FuncType (ins, out), es = $5 c c' in
-      FuncType (snd $3 c @ ins, out), es }
+      let FuncType (ins, out), xs, es = $5 c c' in
+      FuncType (snd $3 c @ ins, out), xs, es }
 
 if_block_result_body :
-  | if_ { fun c c' -> FuncType ([], []), $1 c c' }
+  | if_block_set_body
+    { fun c c' -> let xs, es = $1 c c' in
+      FuncType ([], []), xs, es }
   | LPAR RESULT value_type_list RPAR if_block_result_body
     { fun c c' ->
-      let FuncType (ins, out), es = $5 c c' in
-      FuncType (ins, snd $3 c @ out), es }
+      let FuncType (ins, out), xs, es = $5 c c' in
+      FuncType (ins, snd $3 c @ out), xs, es }
+
+if_block_set_body :
+  | if_ { fun c c' -> [], $1 c c' }
+  | LPAR SET var_list RPAR if_block_set_body
+    { fun c c' -> let xs, es = $5 c c' in
+      $3 c local @ xs, es }
 
 if_ :
   | expr if_
diff --git a/interpreter/util/lib.ml b/interpreter/util/lib.ml
index b0548100..2cd5b402 100644
--- a/interpreter/util/lib.ml
+++ b/interpreter/util/lib.ml
@@ -129,6 +129,10 @@ struct
   and make' n x xs =
     if n = 0l then xs else make' (Int32.sub n 1l) x (x::xs)
 
+  let rec table n f = table' n f []
+  and table' n f xs =
+    if n = 0l then xs else table' (Int32.sub n 1l) f (f (Int32.sub n 1l) :: xs)
+
   let rec length xs = length' xs 0l
   and length' xs n =
     match xs with
@@ -142,6 +146,12 @@ struct
     | n, _::xs' when n > 0l -> nth xs' (Int32.sub n 1l)
     | _ -> failwith "nth"
 
+  let rec replace xs n y =
+    match n, xs with
+    | 0l, _::xs' -> y::xs'
+    | n, x::xs' when n > 0l -> x :: replace xs' (Int32.sub n 1l) y
+    | _ -> failwith "replace"
+
   let rec take n xs =
     match n, xs with
     | 0l, _ -> []
diff --git a/interpreter/util/lib.mli b/interpreter/util/lib.mli
index 08978cb2..772332e2 100644
--- a/interpreter/util/lib.mli
+++ b/interpreter/util/lib.mli
@@ -33,8 +33,10 @@ end
 module List32 :
 sig
   val make : int32 -> 'a -> 'a list
+  val table : int32 -> (int32 -> 'a) -> 'a list
   val length : 'a list -> int32
   val nth : 'a list -> int32 -> 'a (* raises Failure *)
+  val replace : 'a list -> int32 -> 'a -> 'a list (* raises Failure *)
   val take : int32 -> 'a list -> 'a list (* raises Failure *)
   val drop : int32 -> 'a list -> 'a list (* raises Failure *)
   val mapi : (int32 -> 'a -> 'b) -> 'a list -> 'b list
diff --git a/interpreter/valid/match.ml b/interpreter/valid/match.ml
index 3b1dac44..35fb6f5e 100644
--- a/interpreter/valid/match.ml
+++ b/interpreter/valid/match.ml
@@ -53,12 +53,12 @@ and eq_value_type c a t1 t2 =
   | BotType, BotType -> true
   | _, _ -> false
 
-and eq_result_type c a ts1 ts2 =
+and eq_value_types c a ts1 ts2 =
   List.length ts1 = List.length ts2 &&
   List.for_all2 (eq_value_type c a) ts1 ts2
 
 and eq_func_type c a (FuncType (ts11, ts12)) (FuncType (ts21, ts22)) =
-  eq_result_type c a ts11 ts21 && eq_result_type c a ts12 ts22
+  eq_value_types c a ts11 ts21 && eq_value_types c a ts12 ts22
 
 and eq_def_type c a dt1 dt2 =
   match dt1, dt2 with
@@ -130,7 +130,7 @@ and match_value_type c a t1 t2 =
   | BotType, _ -> true
   | _, _ -> false
 
-and match_result_type c a ts1 ts2 =
+and match_value_types c a ts1 ts2 =
   List.length ts1 = List.length ts2 &&
   List.for_all2 (match_value_type c a) ts1 ts2
 
diff --git a/interpreter/valid/match.mli b/interpreter/valid/match.mli
index d258af5d..1e73519d 100644
--- a/interpreter/valid/match.mli
+++ b/interpreter/valid/match.mli
@@ -9,8 +9,7 @@ type assump = (var * var) list
 val eq_num_type : context -> assump -> num_type -> num_type -> bool
 val eq_ref_type : context -> assump -> ref_type -> ref_type -> bool
 val eq_value_type : context -> assump -> value_type -> value_type -> bool
-
-val eq_result_type : context -> assump -> result_type -> result_type -> bool
+val eq_value_types : context -> assump -> value_type list -> value_type list -> bool
 
 val eq_func_type : context -> assump -> func_type -> func_type -> bool
 val eq_table_type : context -> assump -> table_type -> table_type -> bool
@@ -27,8 +26,7 @@ val eq_def_type : context -> assump -> def_type -> def_type -> bool
 val match_num_type : context -> assump -> num_type -> num_type -> bool
 val match_ref_type : context -> assump -> ref_type -> ref_type -> bool
 val match_value_type : context -> assump -> value_type -> value_type -> bool
-
-val match_result_type : context -> assump -> result_type -> result_type -> bool
+val match_value_types : context -> assump -> value_type list -> value_type list -> bool
 
 val match_func_type : context -> assump -> func_type -> func_type -> bool
 val match_table_type : context -> assump -> table_type -> table_type -> bool
diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml
index 7bdad9c5..fffe8cc1 100644
--- a/interpreter/valid/valid.ml
+++ b/interpreter/valid/valid.ml
@@ -24,7 +24,7 @@ type context =
   globals : global_type list;
   elems : ref_type list;
   datas : unit list;
-  locals : value_type list;
+  locals : local_type list;
   results : value_type list;
   labels : result_type list;
   refs : Free.t;
@@ -51,6 +51,21 @@ let data (c : context) x = lookup "data segment" c.datas x
 let local (c : context) x = lookup "local" c.locals x
 let label (c : context) x = lookup "label" c.labels x
 
+let replace category list x y =
+  try Lib.List32.replace list x.it y with Failure _ ->
+    error x.at ("unknown " ^ category ^ " " ^ I32.to_string_u x.it)
+
+let all_locals (c : context) =
+  Lib.List32.table (Lib.List32.length c.locals) (fun x -> x @@ no_region)
+
+let init_local (c : context) x =
+  let LocalType (t, _) = local c x in
+  {c with locals = replace "local" c.locals x (LocalType (t, Initialized))}
+
+let init_locals (c : context) xs poly =
+  List.fold_left init_local c (if poly then all_locals c else xs)
+
+
 let func_type (c : context) x =
   match type_ c x with
   | FuncDefType ft -> ft
@@ -97,13 +112,13 @@ let check_value_type (c : context) (t : value_type) at =
   | RefType t' -> check_ref_type c t' at
   | BotType -> ()
 
-let check_result_type (c : context) (ts : result_type) at =
+let check_value_types (c : context) (ts : value_type list) at =
   List.iter (fun t -> check_value_type c t at) ts
 
 let check_func_type (c : context) (ft : func_type) at =
   let FuncType (ts1, ts2) = ft in
-  check_result_type c ts1 at;
-  check_result_type c ts2 at
+  check_value_types c ts1 at;
+  check_value_types c ts2 at
 
 let check_table_type (c : context) (tt : table_type) at =
   let TableType (lim, t) = tt in
@@ -139,19 +154,21 @@ let check_def_type (c : context) (dt : def_type) at =
 
 type ellipses = NoEllipses | Ellipses
 type infer_result_type = ellipses * value_type list
-type op_type = {ins : infer_result_type; outs : infer_result_type}
+type infer_func_type = {ins : infer_result_type; outs : infer_result_type}
+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 poly (ell, _) = (ell = Ellipses)
 
 let check_stack (c : context) ts1 ts2 at =
   require
     (List.length ts1 = List.length ts2 &&
       List.for_all2 (match_value_type c.types []) ts1 ts2) at
-    ("type mismatch: instruction requires " ^ string_of_result_type ts2 ^
-     " but stack has " ^ string_of_result_type ts1)
+    ("type mismatch: instruction requires " ^ string_of_value_types ts2 ^
+     " but stack has " ^ string_of_value_types ts1)
 
 let pop c (ell1, ts1) (ell2, ts2) at =
   let n1 = List.length ts1 in
@@ -279,8 +296,8 @@ let check_memop (c : context) (memop : ('t, 's) memop) ty_size get_sz at =
  *   e  : instr
  *   es : instr list
  *   v  : value
- *   t  : value_type var
- *   ts : result_type
+ *   t  : value_type
+ *   ts : value_type list
  *   x  : variable
  *
  * Note: To deal with the non-determinism in some of the declarative rules,
@@ -293,113 +310,139 @@ let check_memop (c : context) (memop : ('t, 's) memop) ty_size get_sz at =
  * declarative typing rules.
  *)
 
-let check_block_type (c : context) (bt : block_type) at : func_type =
-  match bt with
-  | ValBlockType None -> FuncType ([], [])
-  | ValBlockType (Some t) -> check_value_type c t at; FuncType ([], [t])
-  | VarBlockType (SynVar x) -> func_type c (x @@ at)
-  | VarBlockType (SemVar _) -> assert false
+let check_block_type (c : context) (bt : block_type) at : instr_type =
+  let ts1, ts2, xs =
+    match bt with
+    | ValBlockType (None, xs) -> [], [], xs
+    | ValBlockType (Some t, xs) -> check_value_type c t at; [], [t], xs
+    | VarBlockType (SynVar x, xs) ->
+      let FuncType (ts1, ts2) = func_type c (x @@ at) in ts1, ts2, xs
+    | VarBlockType (SemVar _, _) -> assert false
+  in
+  InstrType (ts1, ts2, List.map (fun x -> ignore (local c x); x) xs)
 
-let check_local (c : context) (defaults : bool) (t : local) =
+let check_local (c : context) (defaulted : bool) (t : local) : local_type =
   check_value_type c t.it t.at;
-  require (not defaults || defaultable_value_type t.it) t.at
-    "non-defaultable local type"
-
-let rec check_instr (c : context) (e : instr) (s : infer_result_type) : op_type =
+  let init =
+    if not defaulted || defaultable_value_type t.it
+    then Initialized else Uninitialized
+  in LocalType (t.it, init)
+
+and check_init (c : context) (xs : idx list) at =
+  List.iter (fun x ->
+    let LocalType (_, init) = local c x in
+    require (init = Initialized) at
+      ("uninitialized local " ^ I32.to_string_u x.it ^ " at branch or block end")
+  ) xs
+
+let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_instr_type =
   match e.it with
   | Unreachable ->
-    [] -->... []
+    [] -->... [], []
 
   | Nop ->
-    [] --> []
+    [] --> [], []
 
   | Drop ->
-    [peek 0 s] --> []
+    [peek 0 s] --> [], []
 
   | Select None ->
     let t = peek 1 s in
     require (is_num_type t || is_vec_type t) e.at
       ("type mismatch: instruction requires numeric or vector type" ^
        " but stack has " ^ string_of_value_type t);
-    [t; t; NumType I32Type] --> [t]
+    [t; t; NumType I32Type] --> [t], []
 
   | Select (Some ts) ->
     require (List.length ts = 1) e.at
       "invalid result arity other than 1 is not (yet) allowed";
-    check_result_type c ts e.at;
-    (ts @ ts @ [NumType I32Type]) --> ts
+    check_value_types c ts e.at;
+    (ts @ ts @ [NumType I32Type]) --> ts, []
 
   | Block (bt, es) ->
-    let FuncType (ts1, ts2) as ft = check_block_type c bt e.at in
-    check_block {c with labels = ts2 :: c.labels} es ft e.at;
-    ts1 --> ts2
+    let InstrType (ts1, ts2, xs) as it = check_block_type c bt e.at in
+    check_block {c with labels = ResultType (ts2, xs) :: c.labels} es it e.at;
+    ts1 --> ts2, xs
 
   | Loop (bt, es) ->
-    let FuncType (ts1, ts2) as ft = check_block_type c bt e.at in
-    check_block {c with labels = ts1 :: c.labels} es ft e.at;
-    ts1 --> ts2
+    let InstrType (ts1, ts2, xs) as it = check_block_type c bt e.at in
+    check_block {c with labels = ResultType (ts1, []) :: c.labels} es it e.at;
+    ts1 --> ts2, xs
 
   | If (bt, es1, es2) ->
-    let FuncType (ts1, ts2) as ft = check_block_type c bt e.at in
-    check_block {c with labels = ts2 :: c.labels} es1 ft e.at;
-    check_block {c with labels = ts2 :: c.labels} es2 ft e.at;
-    (ts1 @ [NumType I32Type]) --> ts2
+    let InstrType (ts1, ts2, xs) as it = check_block_type c bt e.at in
+    check_block {c with labels = ResultType (ts2, xs) :: c.labels} es1 it e.at;
+    check_block {c with labels = ResultType (ts2, xs) :: c.labels} es2 it e.at;
+    (ts1 @ [NumType I32Type]) --> ts2, xs
 
   | Let (bt, locals, es) ->
-    let FuncType (ts1, ts2) as ft = check_block_type c bt e.at in
-    List.iter (check_local c false) locals;
+    let InstrType (ts1, ts2, xs) as it = check_block_type c bt e.at in
+    let ts = List.map (check_local c false) locals in
     let c' =
       { c with
-        labels = ts2 :: c.labels;
-        locals = List.map Source.it locals @ c.locals;
+        labels = ResultType (ts2, xs) :: c.labels;
+        locals = ts @ c.locals;
       }
-    in check_block c' es ft e.at;
-    (ts1 @ List.map Source.it locals) --> ts2
+    in check_block c' es it e.at;
+    (ts1 @ List.map Source.it locals) --> ts2, xs
 
   | Br x ->
-    label c x -->... []
+    let ResultType (ts, xs) = label c x in
+    check_init c xs x.at;
+    ts -->... [], []
 
   | BrIf x ->
-    (label c x @ [NumType I32Type]) --> label c x
+    let ResultType (ts, xs) = label c x in
+    check_init c xs x.at;
+    (ts @ [NumType I32Type]) --> ts, []
 
   | BrTable (xs, x) ->
-    let n = List.length (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;
-    (ts @ [NumType I32Type]) -->... []
+    let ResultType (ts, ys) = label c x in
+    let n = List.length ts in
+    let ts' = Lib.List.table n (fun i -> peek (n - i) s) in
+    check_init c ys x.at;
+    check_stack c ts' ts x.at;
+    List.iter (fun x' ->
+      let ResultType (ts'', ys') = label c x' in
+      check_init c ys' x'.at;
+      check_stack c ts' ts'' x'.at
+    ) xs;
+    (ts' @ [NumType I32Type]) -->... [], []
 
   | BrOnNull x ->
+    let ResultType (ts, xs) = label c x in
     let (_, t) = peek_ref 0 s e.at in
-    (label c x @ [RefType (Nullable, t)]) -->
-      (label c x @ [RefType (NonNullable, t)])
+    check_init c xs x.at;
+    (ts @ [RefType (Nullable, t)]) --> (ts @ [RefType (NonNullable, t)]), []
 
   | BrOnNonNull x ->
+    let ResultType (ts, xs) = label c x in
     let (_, ht) as rt = peek_ref 0 s e.at in
     let t' = RefType (NonNullable, ht) in
-    require (label c x <> []) e.at
+    check_init c xs x.at;
+    require (ts <> []) e.at
       ("type mismatch: instruction requires type " ^ string_of_value_type t' ^
-       " but label has " ^ string_of_result_type (label c x));
-    let ts0, t = Lib.List.split_last (label c x) in
+       " but label has " ^ string_of_value_types ts);
+    let ts0, t = Lib.List.split_last ts in
     require (match_value_type c.types [] t' t) e.at
       ("type mismatch: instruction requires type " ^ string_of_value_type t' ^
-       " but label has " ^ string_of_result_type (label c x));
-    (ts0 @ [RefType rt]) --> ts0
+       " but label has " ^ string_of_value_types ts);
+    (ts0 @ [RefType rt]) --> ts0, []
 
   | Return ->
-    c.results -->... []
+    c.results -->... [], []
 
   | Call x ->
     let FuncType (ts1, ts2) = func c x in
-    ts1 --> ts2
+    ts1 --> ts2, []
 
   | CallRef ->
     (match peek_ref 0 s e.at with
     | (nul, DefHeapType (SynVar x)) ->
       let FuncType (ts1, ts2) = func_type c (x @@ e.at) in
-      (ts1 @ [RefType (nul, DefHeapType (SynVar x))]) --> ts2
+      (ts1 @ [RefType (nul, DefHeapType (SynVar x))]) --> ts2, []
     | (_, BotHeapType) as rt ->
-      [RefType rt] -->... []
+      [RefType rt] -->... [], []
     | rt ->
       error e.at
         ("type mismatch: instruction requires function reference type" ^
@@ -412,19 +455,19 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : op_type
     require (match_ref_type c.types [] t (Nullable, FuncHeapType)) x.at
       ("type mismatch: instruction requires table of function type" ^
        " but table has element type " ^ string_of_ref_type t);
-    (ts1 @ [NumType I32Type]) --> ts2
+    (ts1 @ [NumType I32Type]) --> ts2, []
 
   | ReturnCallRef ->
     (match peek_ref 0 s e.at with
     | (nul, DefHeapType (SynVar x)) ->
       let FuncType (ts1, ts2) = func_type c (x @@ e.at) in
-      require (match_result_type c.types [] ts2 c.results) e.at
+      require (match_value_types c.types [] ts2 c.results) e.at
         ("type mismatch: current function requires result type " ^
-         string_of_result_type c.results ^
-         " but callee returns " ^ string_of_result_type ts2);
-      (ts1 @ [RefType (nul, DefHeapType (SynVar x))]) -->... []
+         string_of_value_types c.results ^
+         " but callee returns " ^ string_of_value_types ts2);
+      (ts1 @ [RefType (nul, DefHeapType (SynVar x))]) -->... [], []
     | (_, BotHeapType) as rt ->
-      [RefType rt] -->... []
+      [RefType rt] -->... [], []
     | rt ->
       error e.at
         ("type mismatch: instruction requires function reference type" ^
@@ -442,9 +485,9 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : op_type
       require (match_func_type c.types [] (FuncType (ts12, ts2)) ft') e.at
         "type mismatch in function type";
       (ts11 @ [RefType (nul, DefHeapType (SynVar y))]) -->
-        [RefType (NonNullable, DefHeapType (SynVar x.it))]
+        [RefType (NonNullable, DefHeapType (SynVar x.it))], []
     | (_, BotHeapType) as rt ->
-      [RefType rt] -->.. [RefType (NonNullable, DefHeapType (SynVar x.it))]
+      [RefType rt] -->.. [RefType (NonNullable, DefHeapType (SynVar x.it))], []
     | rt ->
       error e.at
         ("type mismatch: instruction requires function reference type" ^
@@ -452,42 +495,46 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : op_type
     )
 
   | LocalGet x ->
-    [] --> [local c x]
+    let LocalType (t, init) = local c x in
+    require (init = Initialized) x.at "uninitialized local";
+    [] --> [t], []
 
   | LocalSet x ->
-    [local c x] --> []
+    let LocalType (t, _) = local c x in
+    [t] --> [], [x]
 
   | LocalTee x ->
-    [local c x] --> [local c x]
+    let LocalType (t, _) = local c x in
+    [t] --> [t], [x]
 
   | GlobalGet x ->
     let GlobalType (t, _mut) = global c x in
-    [] --> [t]
+    [] --> [t], []
 
   | GlobalSet x ->
     let GlobalType (t, mut) = global c x in
     require (mut = Mutable) x.at "global is immutable";
-    [t] --> []
+    [t] --> [], []
 
   | TableGet x ->
     let TableType (_lim, t) = table c x in
-    [NumType I32Type] --> [RefType t]
+    [NumType I32Type] --> [RefType t], []
 
   | TableSet x ->
     let TableType (_lim, t) = table c x in
-    [NumType I32Type; RefType t] --> []
+    [NumType I32Type; RefType t] --> [], []
 
   | TableSize x ->
     let _tt = table c x in
-    [] --> [NumType I32Type]
+    [] --> [NumType I32Type], []
 
   | TableGrow x ->
     let TableType (_lim, t) = table c x in
-    [RefType t; NumType I32Type] --> [NumType I32Type]
+    [RefType t; NumType I32Type] --> [NumType I32Type], []
 
   | TableFill x ->
     let TableType (_lim, t) = table c x in
-    [NumType I32Type; RefType t; NumType I32Type] --> []
+    [NumType I32Type; RefType t; NumType I32Type] --> [], []
 
   | TableCopy (x, y) ->
     let TableType (_lim1, t1) = table c x in
@@ -495,7 +542,7 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : op_type
     require (match_ref_type c.types [] t2 t1) x.at
       ("type mismatch: source element type " ^ string_of_ref_type t1 ^
        " does not match destination element type " ^ string_of_ref_type t2);
-    [NumType I32Type; NumType I32Type; NumType I32Type] --> []
+    [NumType I32Type; NumType I32Type; NumType I32Type] --> [], []
 
   | TableInit (x, y) ->
     let TableType (_lim1, t1) = table c x in
@@ -503,195 +550,196 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : op_type
     require (match_ref_type c.types [] t2 t1) x.at
       ("type mismatch: element segment's type " ^ string_of_ref_type t1 ^
        " does not match table's element type " ^ string_of_ref_type t2);
-    [NumType I32Type; NumType I32Type; NumType I32Type] --> []
+    [NumType I32Type; NumType I32Type; NumType I32Type] --> [], []
 
   | ElemDrop x ->
     ignore (elem c x);
-    [] --> []
+    [] --> [], []
 
   | Load memop ->
     check_memop c memop num_size (Lib.Option.map fst) e.at;
-    [NumType I32Type] --> [NumType memop.ty]
+    [NumType I32Type] --> [NumType memop.ty], []
 
   | Store memop ->
     check_memop c memop num_size (fun sz -> sz) e.at;
-    [NumType I32Type; NumType memop.ty] --> []
+    [NumType I32Type; NumType memop.ty] --> [], []
 
   | VecLoad memop ->
     check_memop c memop vec_size (Lib.Option.map fst) e.at;
-    [NumType I32Type] --> [VecType memop.ty]
+    [NumType I32Type] --> [VecType memop.ty], []
 
   | VecStore memop ->
     check_memop c memop vec_size (fun _ -> None) e.at;
-    [NumType I32Type; VecType memop.ty] --> []
+    [NumType I32Type; VecType memop.ty] --> [], []
 
   | VecLoadLane (memop, i) ->
     check_memop c memop vec_size (fun sz -> Some sz) e.at;
     require (i < vec_size memop.ty / packed_size memop.pack) e.at
       "invalid lane index";
-    [NumType I32Type; VecType memop.ty] -->  [VecType memop.ty]
+    [NumType I32Type; VecType memop.ty] -->  [VecType memop.ty], []
 
   | VecStoreLane (memop, i) ->
     check_memop c memop vec_size (fun sz -> Some sz) e.at;
     require (i < vec_size memop.ty / packed_size memop.pack) e.at
       "invalid lane index";
-    [NumType I32Type; VecType memop.ty] -->  []
+    [NumType I32Type; VecType memop.ty] -->  [], []
 
   | MemorySize ->
     let _mt = memory c (0l @@ e.at) in
-    [] --> [NumType I32Type]
+    [] --> [NumType I32Type], []
 
   | MemoryGrow ->
     let _mt = memory c (0l @@ e.at) in
-    [NumType I32Type] --> [NumType I32Type]
+    [NumType I32Type] --> [NumType I32Type], []
 
   | MemoryFill ->
     ignore (memory c (0l @@ e.at));
-    [NumType I32Type; NumType I32Type; NumType I32Type] --> []
+    [NumType I32Type; NumType I32Type; NumType I32Type] --> [], []
 
   | MemoryCopy ->
     ignore (memory c (0l @@ e.at));
-    [NumType I32Type; NumType I32Type; NumType I32Type] --> []
+    [NumType I32Type; NumType I32Type; NumType I32Type] --> [], []
 
   | MemoryInit x ->
     ignore (memory c (0l @@ e.at));
     ignore (data c x);
-    [NumType I32Type; NumType I32Type; NumType I32Type] --> []
+    [NumType I32Type; NumType I32Type; NumType I32Type] --> [], []
 
   | DataDrop x ->
     ignore (data c x);
-    [] --> []
+    [] --> [], []
 
   | RefNull t ->
     check_heap_type c t e.at;
-    [] --> [RefType (Nullable, t)]
+    [] --> [RefType (Nullable, t)], []
 
   | RefIsNull ->
     let (_, t) = peek_ref 0 s e.at in
-    [RefType (Nullable, t)] --> [NumType I32Type]
+    [RefType (Nullable, t)] --> [NumType I32Type], []
 
   | RefAsNonNull ->
     let (_, t) = peek_ref 0 s e.at in
-    [RefType (Nullable, t)] --> [RefType (NonNullable, t)]
+    [RefType (Nullable, t)] --> [RefType (NonNullable, t)], []
 
   | RefFunc x ->
     let ft = func c x in
     let y = Lib.Option.force (Lib.List32.index_of (FuncDefType ft) c.types) in
     refer_func c x;
-    [] --> [RefType (NonNullable, DefHeapType (SynVar y))]
+    [] --> [RefType (NonNullable, DefHeapType (SynVar y))], []
 
   | Const v ->
     let t = NumType (type_num v.it) in
-    [] --> [t]
+    [] --> [t], []
 
   | Test testop ->
     let t = NumType (type_num testop) in
-    [t] --> [NumType I32Type]
+    [t] --> [NumType I32Type], []
 
   | Compare relop ->
     let t = NumType (type_num relop) in
-    [t; t] --> [NumType I32Type]
+    [t; t] --> [NumType I32Type], []
 
   | Unary unop ->
     check_unop unop e.at;
     let t = NumType (type_num unop) in
-    [t] --> [t]
+    [t] --> [t], []
 
   | Binary binop ->
     let t = NumType (type_num binop) in
-    [t; t] --> [t]
+    [t; t] --> [t], []
 
   | Convert cvtop ->
     let t1, t2 = type_cvtop e.at cvtop in
-    [NumType t1] --> [NumType t2]
+    [NumType t1] --> [NumType t2], []
 
   | VecConst v ->
     let t = VecType (type_vec v.it) in
-    [] --> [t]
+    [] --> [t], []
 
   | VecTest testop ->
     let t = VecType (type_vec testop) in
-    [t] --> [NumType I32Type]
+    [t] --> [NumType I32Type], []
 
   | VecUnary unop ->
     let t = VecType (type_vec unop) in
-    [t] --> [t]
+    [t] --> [t], []
 
   | VecBinary binop ->
     check_vec_binop binop e.at;
     let t = VecType (type_vec binop) in
-    [t; t] --> [t]
+    [t; t] --> [t], []
 
   | VecCompare relop ->
     let t = VecType (type_vec relop) in
-    [t; t] --> [t]
+    [t; t] --> [t], []
 
   | VecConvert cvtop ->
     let t = VecType (type_vec cvtop) in
-    [t] --> [t]
+    [t] --> [t], []
 
   | VecShift shiftop ->
     let t = VecType (type_vec shiftop) in
-    [t; NumType I32Type] --> [VecType V128Type]
+    [t; NumType I32Type] --> [VecType V128Type], []
 
   | VecBitmask bitmaskop ->
     let t = VecType (type_vec bitmaskop) in
-    [t] --> [NumType I32Type]
+    [t] --> [NumType I32Type], []
 
   | VecTestBits vtestop ->
     let t = VecType (type_vec vtestop) in
-    [t] --> [NumType I32Type]
+    [t] --> [NumType I32Type], []
 
   | VecUnaryBits vunop ->
     let t = VecType (type_vec vunop) in
-    [t] --> [t]
+    [t] --> [t], []
 
   | VecBinaryBits vbinop ->
     let t = VecType (type_vec vbinop) in
-    [t; t] --> [t]
+    [t; t] --> [t], []
 
   | VecTernaryBits vternop ->
     let t = VecType (type_vec vternop) in
-    [t; t; t] --> [t]
+    [t; t; t] --> [t], []
 
   | VecSplat splatop ->
     let t1 = type_vec_lane splatop in
     let t2 = VecType (type_vec splatop) in
-    [NumType t1] --> [t2]
+    [NumType t1] --> [t2], []
 
   | VecExtract extractop ->
     let t = VecType (type_vec extractop) in
     let t2 = type_vec_lane extractop in
     require (lane_extractop extractop < num_lanes extractop) e.at
       "invalid lane index";
-    [t] --> [NumType t2]
+    [t] --> [NumType t2], []
 
   | VecReplace replaceop ->
     let t = VecType (type_vec replaceop) in
     let t2 = type_vec_lane replaceop in
     require (lane_replaceop replaceop < num_lanes replaceop) e.at
       "invalid lane index";
-    [t; NumType t2] --> [t]
+    [t; NumType t2] --> [t], []
 
 and check_seq (c : context) (s : infer_result_type) (es : instr list)
-  : infer_result_type =
+  : infer_result_type * idx list =
   match es with
   | [] ->
-    s
+    s, []
 
   | _ ->
     let es', e = Lib.List.split_last es in
-    let s' = check_seq c s es' in
-    let {ins; outs} = check_instr c e s' in
-    push c outs (pop c ins s' e.at)
+    let s', xs = check_seq c s es' in
+    let {ins; outs}, xs' = check_instr (init_locals c xs (poly s')) e s' in
+    push c outs (pop c ins s' e.at), xs @ xs'
 
-and check_block (c : context) (es : instr list) (ft : func_type) at =
-  let FuncType (ts1, ts2) = ft in
-  let s = check_seq c (stack ts1) es in
+and check_block (c : context) (es : instr list) (it : instr_type) at =
+  let InstrType (ts1, ts2, xs) = it in
+  let s, xs' = check_seq c (stack ts1) es in
   let s' = pop c (stack ts2) s at in
+  check_init (init_locals c xs' (poly s')) xs at;
   require (snd s' = []) at
-    ("type mismatch: block requires " ^ string_of_result_type ts2 ^
-     " but stack has " ^ string_of_result_type (snd s))
+    ("type mismatch: block requires " ^ string_of_value_types ts2 ^
+     " but stack has " ^ string_of_value_types (snd s))
 
 
 (* Functions & Constants *)
@@ -711,14 +759,14 @@ and check_block (c : context) (es : instr list) (ft : func_type) at =
 let check_func (c : context) (f : func) =
   let {ftype; locals; body} = f.it in
   let FuncType (ts1, ts2) = func_type c ftype in
-  List.iter (check_local c true) locals;
+  let ts = List.map (check_local c true) locals in
   let c' =
     { c with
-      locals = ts1 @ List.map Source.it locals;
+      locals = List.map (fun t -> LocalType (t, Initialized)) ts1 @ ts;
       results = ts2;
-      labels = [ts2]
+      labels = [ResultType (ts2, [])]
     }
-  in check_block c' body (FuncType ([], ts2)) f.at
+  in check_block c' body (InstrType ([], ts2, [])) f.at
 
 
 let is_const (c : context) (e : instr) =
@@ -733,7 +781,7 @@ let is_const (c : context) (e : instr) =
 let check_const (c : context) (const : const) (t : value_type) =
   require (List.for_all (is_const c) const.it) const.at
     "constant expression required";
-  check_block c const.it (FuncType ([], [t])) const.at
+  check_block c const.it (InstrType ([], [t], [])) const.at
 
 
 (* Tables, Memories, & Globals *)
diff --git a/proposals/function-references/Overview.md b/proposals/function-references/Overview.md
index da019d1f..b25e9e11 100644
--- a/proposals/function-references/Overview.md
+++ b/proposals/function-references/Overview.md
@@ -199,6 +199,50 @@ The following rules, now defined in terms of heap types, replace and extend the
 * TODO: Table definitions with a type that is not defaultable must have an initialiser value. (Imports are not affected.)
 
 
+#### Local Types
+
+* Locals are now recorded in the context with types of the following form:
+  - `localtype ::= set? <valtype>`
+  - the flag `set` records that the local has been initialized
+  - all locals with non-defaultable type start out unset
+
+
+#### Result Types
+
+* Result types are refined to the following form:
+  - `resulttype ::= [<valtype>*] <localidx>*`
+  - the local indices record which locals have been set as a side effect
+  - result types are assigned to labels and the result of instruction sequences
+
+* There is a natural notion of subtyping on result types:
+  - `[t1*] x1*  <:  [t2*] x2*`
+    - iff `(t1 <: t2)*`
+    - and `{x2*} subset {x1*}`
+
+
+#### Instruction Types
+
+* Instructions and instruction sequences are now typed with types of the following form:
+  - `instrtype ::= [<valtype>*] -> <resulttype>`
+  - the local indices record which locals have been set by the instructions
+  - most typing rules except those for locals and for instruction sequences remain unchanged, since the index list is empty
+
+* There is a natural notion of subtyping on instruction types:
+  - `[t1*] -> [t2*] x1*  <:  [t3*] -> [t4*] x2*`
+    - iff `t1* = t0* t1'*`
+    - and `t2* = t0* t2'*`
+    - and `(t3 <: t1')*`
+    - and `[t2'*] x1* <: [t4*] x2*`
+
+
+#### Block Types
+
+* Block types denote [instruction types](#instruction-types). For that purpose, they are likewise extended with a (possibly empty) sequence of local indices
+  - `blocktype ::= (<valtype> | <typeidx>) <localidx>*`
+    - `t x* : [] -> [t] x*` iff `t ok` and `(x ok)*`
+      - note: this rule does not enforce that the `x*` are all different
+    - `$t x* : [t1*] -> [t2*] x*` iff `$t = [t1*] -> [t2*]` and `(x ok)*`
+
 ### Instructions
 
 #### Functions
@@ -276,6 +320,104 @@ The rule also implies that let-bound locals are mutable.
 Like all other block instructions, `let` binds a label
 
 
+#### Locals
+
+Typing of local instructions is updated to account for the initialization status of locals.
+
+* `local.get $x`
+  - `local.get $x : [] -> [t]`
+    - iff `$x : set t`
+
+* `local.set $x`
+  - `local.set $x : [t] -> [] $x`
+    - iff `$x : set? t`
+
+* `local.tee $x`
+  - `local.tee $x : [t] -> [t] $x`
+    - iff `$x : set? t`
+
+Note: These typing rules do not try to exclude indices for locals that have already been set, but an implementation could.
+
+
+#### Instruction Sequences
+
+Typing of instruction sequences is updated to account for initialization of locals.
+
+* `instr*`
+  - `instr* instrN : [t1*] -> [t3*] x1* x2*`
+    - iff `instr* : [t1*] -> [t2*] x1*`
+    - and `instrN : [t2*] -> [t3*] x2*` under a context where `x1*` are changed to `set`
+  - `epsilon : [] -> [] x*`
+    - iff `(x : set t)*`
+
+Note: These typing rules do not try to eliminate duplicate indices, but an implementation could.
+
+A subsumption rule allows to go to a supertype for any instruction:
+
+* `instr`
+  - `instr : [t1*] -> [t2*] x*`
+    - iff `instr : [t1'*] -> [t2'*] x'*`
+    - and `[t1'*] -> [t2'*] x'*  <:  [t1*] -> [t2*] x*`
+
+
+#### Blocks
+
+The block types ascribed to blocks declare the instruction type of the respective body's instruction sequence.
+
+* `block bt <instr>* end`
+  - `block $l bt <instr>* end : it`
+    - iff `bt : it`
+    - and `<instr>* : it` assuming `$l : [t2*] x*`
+    - where `it = [t1*] -> [t2*] x*`
+
+* `loop bt <instr>* end`
+  - `loop $l bt <instr>* end : it`
+    - iff `bt : it`
+    - and `<instr>* : it` assuming `$l : [t1*]`
+    - where `it = [t1*] -> [t2*] x*`
+
+* `if bt <instr1>* else <instr2>* end`
+  - `if $l bt <instr1>* else <instr2>* end : it`
+    - iff `bt : it`
+    - and `<instr1>* : it` assuming `$l : [t2*] x*`
+    - and `<instr2>* : it` assuming `$l : [t2*] x*`
+    - where `it = [t1*] -> [t2*] x*`
+
+Note: For a future `try-catch`, the block type associated with `try` would likewise apply to all catch clauses – in order to avoid the need for exception and effect analysis, no assumption is being made about what parts of the `try` block have already been executed when entering a catch clause, and conservatively assumes none. Sketch (omitting `catch_all`):
+
+  - `try $l bt <instr0>* (catch $x <instr>*)* end`
+    - iff `bt : it`
+    - and `<instr0>* : it0` assuming `$l : [t2*] x*`
+    - and `(<instr>* : it)*` assuming `$l : [t2*] x*`
+    - and `($x : [tx*] -> [])*`
+    - where `it0 = [t1*] -> [t2*] x*`
+    - and `(it = [tx*] -> [t2*] x*)*`
+
+
+#### Branches
+
+Branches need to match the respective label type. Moreover, stack polymorphism now entails an arbitrary initialization set.
+
+* `br $l`
+  - `br $l : [t1* t*] -> [t2*] x2*`
+    - iff `$l : [t*] x*`
+    - and `(x : set tX)*`
+    - and `(x2 : set? tX2)*`
+
+* `br_if $l`
+  - `br_if $l : [t* i32] -> [t*]`
+    - iff `$l : [t*] x*`
+    - and `(x : set tX)*`
+
+* `br_table $l* $l'`
+  - `br_table $l* $l' : [t1* t'* i32] -> [t2* t'*] x2*`
+    - iff `$l' : [t'*] x'*`
+    - and `(x' : set tX')*`
+    - and `($l : [t*] x*)*`
+    - and `(x : set tX)*`
+    - and `(x2 : set? tX2)*`
+
+
 ### Tables
 
 * TODO: Table definitions have an initialiser value: `(table <tabletype> <constexpr>)`
@@ -306,6 +448,18 @@ The opcode for heap types is encoded as an `s33`.
 | -0x10  | `func`          |            |
 | -0x11  | `extern`        |            |
 
+#### Block Types
+
+The opcode for block types is encoded as an `s33`.
+
+| Opcode | Type            | Parameters | Note |
+| ------ | --------------- | ---------- | ---- |
+| -0x40  | `[] -> []`      |            |      |
+| -0x3f  | `<ft> <idx>*`   | `idx* : vec(u32)`, `ft : blocktype` | `ft` must not be `-0x3f` |
+| i < 0  | `valtype`       |            |      |
+| i >= 0 | `$t`            |            |      |
+
+
 ### Instructions
 
 | Opcode | Instruction              | Immediates |
diff --git a/test/core/func.wast b/test/core/func.wast
index 46a01383..b844d4a6 100644
--- a/test/core/func.wast
+++ b/test/core/func.wast
@@ -657,8 +657,11 @@
 )
 
 (assert_invalid
-  (module (type $t (func)) (func $type-local-no-default (local (ref $t))))
-  "non-defaultable local type"
+  (module
+    (type $t (func))
+    (func $type-local-uninitialized (local $x (ref $t)) (drop (local.get $x)))
+  )
+  "uninitialized local"
 )
 
 
@@ -956,24 +959,31 @@
   "unexpected token"
 )
 
+
 ;; Duplicate name errors
 
-(assert_malformed (module quote
-  "(func $foo)"
-  "(func $foo)")
-  "duplicate func")
-(assert_malformed (module quote
-  "(import \"\" \"\" (func $foo))"
-  "(func $foo)")
-  "duplicate func")
-(assert_malformed (module quote
-  "(import \"\" \"\" (func $foo))"
-  "(import \"\" \"\" (func $foo))")
-  "duplicate func")
-
-(assert_malformed (module quote "(func (param $foo i32) (param $foo i32))")
-  "duplicate local")
-(assert_malformed (module quote "(func (param $foo i32) (local $foo i32))")
-  "duplicate local")
-(assert_malformed (module quote "(func (local $foo i32) (local $foo i32))")
-  "duplicate local")
+(assert_malformed
+  (module quote "(func $foo)" "(func $foo)")
+  "duplicate func"
+)
+(assert_malformed
+  (module quote "(import \"\" \"\" (func $foo))" "(func $foo)")
+  "duplicate func"
+)
+(assert_malformed
+  (module quote "(import \"\" \"\" (func $foo))" "(import \"\" \"\" (func $foo))")
+  "duplicate func"
+)
+
+(assert_malformed
+  (module quote "(func (param $foo i32) (param $foo i32))")
+  "duplicate local"
+)
+(assert_malformed
+  (module quote "(func (param $foo i32) (local $foo i32))")
+  "duplicate local"
+)
+(assert_malformed
+  (module quote "(func (local $foo i32) (local $foo i32))")
+  "duplicate local"
+)
diff --git a/test/core/local-block-set.wast b/test/core/local-block-set.wast
new file mode 100644
index 00000000..52cb6c0a
--- /dev/null
+++ b/test/core/local-block-set.wast
@@ -0,0 +1,697 @@
+;; Syntax
+
+(module
+  (func (export "syntax")
+    (local $y1 i64)
+    (local $y2 i32)
+
+    (block (set))
+    (block $l (set))
+    (block (param) (set))
+    (block $l (param) (set))
+    (block (result) (set))
+    (block $l (result) (set))
+    (block (param) (result) (set))
+    (block $l (param) (result) (set))
+
+    (block $l (set $y1))
+    (block $l (set $y1 $y2))
+    (block $l (set $y1 $y1 0 1))
+    (block $l (set 0 $y1) (set $y1 $y2))
+
+    (i32.const 1)
+    (block $l (param i32) (result i64) (set $y1 $y2) (br $l (i64.const 3)))
+    (drop)
+
+    block (set) end
+    block $l (set) end
+    block (param) (set) end
+    block $l (param) (set) end
+    block (result) (set) end
+    block $l (result) (set) end
+    block (param) (result) (set) end
+    block $l (param) (result) (set) end
+
+    block $l (set $y1) end
+    block $l (set $y1 $y2) end
+    block $l (set $y1 $y1 0 1) end
+    block $l (set 0 $y1) (set $y1 $y2) end
+
+    (i32.const 1)
+    block $l (param i32) (result i64) (set $y1 $y2) (br $l (i64.const 3)) end
+    (drop)
+
+    (loop (set))
+    (loop $l (set))
+    (loop (param) (set))
+    (loop $l (param) (set))
+    (loop (result) (set))
+    (loop $l (result) (set))
+    (loop (param) (result) (set))
+    (loop $l (param) (result) (set))
+
+    (loop $l (set $y1))
+    (loop $l (set $y1 $y2))
+    (loop $l (set $y1 $y1 0 1))
+    (loop $l (set 0 $y1) (set $y1 $y2))
+
+    (i32.const 1)
+    (loop $l (param i32) (result i64) (set $y1 $y2) (i64.extend_i32_u))
+    (drop)
+
+    loop (set) end
+    loop $l (set) end
+    loop (param) (set) end
+    loop $l (param) (set) end
+    loop (result) (set) end
+    loop $l (result) (set) end
+    loop (param) (result) (set) end
+    loop $l (param) (result) (set) end
+
+    loop $l (set $y1) end
+    loop $l (set $y1 $y2) end
+    loop $l (set $y1 $y1 0 1) end
+    loop $l (set 0 $y1) (set $y1 $y2) end
+
+    (i32.const 1)
+    loop $l (param i32) (result i64) (set $y1 $y2) (i64.extend_i32_u) end
+    (drop)
+
+    (i32.const 1)
+    (if (set) (then))
+    (i32.const 1)
+    (if $l (set) (then))
+    (i32.const 1)
+    (if (param) (set) (then))
+    (i32.const 1)
+    (if $l (param) (set) (then))
+    (i32.const 1)
+    (if (result) (set) (then))
+    (i32.const 1)
+    (if $l (result) (set) (then))
+    (i32.const 1)
+    (if (param) (result) (set) (then))
+    (i32.const 1)
+    (if $l (param) (result) (set) (then))
+
+    (i32.const 1)
+    (if $l (set $y1) (then))
+    (i32.const 1)
+    (if $l (set $y1 $y2) (then))
+    (i32.const 1)
+    (if $l (set $y1 $y1 0 1) (then))
+    (i32.const 1)
+    (if $l (set 0 $y1) (set $y1 $y2) (then))
+
+    (i32.const 1)
+    (i32.const 1)
+    (if $l (param i32) (result i64) (set $y1 $y2)
+      (then (i64.extend_i32_s))
+      (else (br $l (i64.const 4)))
+    )
+    (drop)
+
+    (i32.const 1)
+    if (set) else end
+    (i32.const 1)
+    if $l (set) end
+    (i32.const 1)
+    if (param) (set) else end
+    (i32.const 1)
+    if $l (param) (set) end
+    (i32.const 1)
+    if (result) (set) else end
+    (i32.const 1)
+    if $l (result) (set) end
+    (i32.const 1)
+    if (param) (result) (set) else end
+    (i32.const 1)
+    if $l (param) (result) (set) end
+
+    (i32.const 1)
+    if $l (set $y1) else end
+    (i32.const 1)
+    if $l (set $y1 $y2) end
+    (i32.const 1)
+    if $l (set $y1 $y1 0 1) else end
+    (i32.const 1)
+    if $l (set 0 $y1) (set $y1 $y2) else end
+
+    (i32.const 1)
+    (i32.const 1)
+    if $l (param i32) (result i64) (set $y1 $y2)
+      (br $l (i64.const 3))
+    else
+      (i64.extend_i32_u)
+    end
+    (drop)
+  )
+)
+
+(assert_return (invoke "syntax"))
+
+
+(assert_malformed
+  (module quote "(func (block (set) (param)))")
+  "unexpected token"
+)
+(assert_malformed
+  (module quote
+    "(func"
+    "  (local i32)"
+    "  (i32.const 0) (i32.const 0)"
+    "  (block (set 0) (param i32) (drop))"
+    ")"
+  )
+  "unexpected token"
+)
+
+(assert_malformed
+  (module quote "(func (block (set) (result)))")
+  "unexpected token"
+)
+(assert_malformed
+  (module quote
+    "(func (result i32)"
+    "  (local i32)"
+    "  (i32.const 0)"
+    "  (block (set 0) (result i32) (local.get 0))"
+    ")"
+  )
+  "unexpected token"
+)
+(assert_malformed
+  (module quote
+    "(func (result i32)"
+    "  (local $x i32)"
+    "  (block (set $x) (result i32) (local.get 0))"
+    ")"
+  )
+  "unexpected token"
+)
+
+(assert_malformed
+  (module quote "(func (block (set) $l))")
+  "unexpected token"
+)
+
+
+;; Typing
+
+(module
+  (type $t (func))
+  (func $f)
+  (elem declare func $f)
+
+  (func
+    (local $x i32)
+    (drop (local.get $x))
+    (block (set $x))
+    (drop (local.get $x))
+  )
+  (func (param $x i32)
+    (drop (local.get $x))
+    (block (set $x))
+    (drop (local.get $x))
+  )
+
+  (func (param $x (ref $t))
+    (drop (local.get $x))
+    (block (set $x))
+    (drop (local.get $x))
+  )
+
+  (func
+    (local $x (ref $t))
+    (local.set $x (ref.func $f))
+    (drop (local.get $x))
+    (block (set $x))
+    (drop (local.get $x))
+  )
+  (func
+    (local $x (ref $t))
+    (block (set $x)
+      (local.set $x (ref.func $f))
+      (drop (local.get $x))
+    )
+    (drop (local.get $x))
+  )
+  (func
+    (local $x (ref $t))
+    (block (set $x)
+      (block (set $x)
+        (local.set $x (ref.func $f))
+      )
+      (drop (local.get $x))
+    )
+    (drop (local.get $x))
+  )
+  (func
+    (local $x (ref $t))
+    (block (set $x)
+      (local.set $x (ref.func $f))
+    )
+    (drop (local.get $x))
+    (block (set $x)
+      (drop (local.get $x))
+    )
+  )
+
+  (func
+    (local $x (ref $t))
+    (block $l
+      (block (set $x)
+        (br $l)
+        (drop (local.get $x))
+      )
+      (drop (local.get $x))
+    )
+  )
+  (func
+    (local $x (ref $t))
+    (block $l
+      (block (set $x)
+        (i32.const 0)
+        (br_table $l $l)
+        (drop (local.get $x))
+      )
+      (drop (local.get $x))
+    )
+  )
+  (func
+    (local $x (ref $t))
+    (block $l
+      (block (set $x)
+        (unreachable)
+        (drop (local.get $x))
+      )
+      (drop (local.get $x))
+    )
+  )
+
+  (func
+    (local $x i32)
+    (drop (local.get $x))
+    (loop (set $x))
+    (drop (local.get $x))
+  )
+  (func (param $x i32)
+    (drop (local.get $x))
+    (loop (set $x))
+    (drop (local.get $x))
+  )
+
+  (func (param $x (ref $t))
+    (drop (local.get $x))
+    (loop (set $x))
+    (drop (local.get $x))
+  )
+
+  (func
+    (local $x (ref $t))
+    (local.set $x (ref.func $f))
+    (drop (local.get $x))
+    (loop (set $x))
+    (drop (local.get $x))
+  )
+  (func
+    (local $x (ref $t))
+    (loop (set $x)
+      (local.set $x (ref.func $f))
+      (drop (local.get $x))
+    )
+    (drop (local.get $x))
+  )
+  (func
+    (local $x (ref $t))
+    (loop (set $x)
+      (loop (set $x)
+        (local.set $x (ref.func $f))
+      )
+      (drop (local.get $x))
+    )
+    (drop (local.get $x))
+  )
+  (func
+    (local $x (ref $t))
+    (loop (set $x)
+      (local.set $x (ref.func $f))
+    )
+    (drop (local.get $x))
+    (loop (set $x)
+      (drop (local.get $x))
+    )
+  )
+
+  (func
+    (local $x (ref $t))
+    (loop $l (set $x)
+      (br $l)
+      (drop (local.get $x))
+    )
+  )
+  (func
+    (local $x (ref $t))
+    (loop $l (set $x)
+      (i32.const 0)
+      (br_table $l $l)
+      (drop (local.get $x))
+    )
+  )
+  (func
+    (local $x (ref $t))
+    (loop $l (set $x)
+      (unreachable)
+      (drop (local.get $x))
+    )
+  )
+
+  (func
+    (local $x i32)
+    (drop (local.get $x))
+    (i32.const 1)
+    (if (set $x) (then))
+    (drop (local.get $x))
+  )
+  (func (param $x i32)
+    (drop (local.get $x))
+    (i32.const 1)
+    (if (set $x) (then))
+    (drop (local.get $x))
+  )
+
+  (func (param $x (ref $t))
+    (drop (local.get $x))
+    (i32.const 1)
+    (if (set $x) (then))
+    (drop (local.get $x))
+  )
+
+  (func
+    (local $x (ref $t))
+    (local.set $x (ref.func $f))
+    (drop (local.get $x))
+    (i32.const 1)
+    (if (set $x) (then))
+    (drop (local.get $x))
+  )
+  (func
+    (local $x (ref $t))
+    (i32.const 1)
+    (if (set $x)
+      (then
+        (local.set $x (ref.func $f))
+        (drop (local.get $x))
+      )
+      (else
+        (local.set $x (ref.func $f))
+        (drop (local.get $x))
+      )
+    )
+    (drop (local.get $x))
+  )
+  (func
+    (local $x (ref $t))
+    (i32.const 1)
+    (if (set $x)
+      (then
+        (block (set $x)
+          (local.set $x (ref.func $f))
+        )
+        (drop (local.get $x))
+      )
+      (else
+        (block (set $x)
+          (local.set $x (ref.func $f))
+        )
+        (drop (local.get $x))
+      )
+    )
+    (drop (local.get $x))
+  )
+  (func
+    (local $x (ref $t))
+    (block (set $x)
+      (local.set $x (ref.func $f))
+    )
+    (drop (local.get $x))
+    (i32.const 1)
+    (if (set $x)
+      (then (drop (local.get $x)))
+    )
+  )
+
+  (func
+    (local $x (ref $t))
+    (block $l
+      (i32.const 1)
+      (if (set $x)
+        (then
+          (br $l)
+          (drop (local.get $x))
+        )
+        (else
+          (br $l)
+          (drop (local.get $x))
+        )
+      )
+      (drop (local.get $x))
+    )
+  )
+  (func
+    (local $x (ref $t))
+    (block $l
+      (i32.const 1)
+      (if (set $x)
+        (then
+          (i32.const 0)
+          (br_table $l $l)
+          (drop (local.get $x))
+        )
+        (else
+          (i32.const 0)
+          (br_table $l $l)
+          (drop (local.get $x))
+        )
+      )
+      (drop (local.get $x))
+    )
+  )
+  (func
+    (local $x (ref $t))
+    (block $l
+      (i32.const 1)
+      (if (set $x)
+        (then
+          (unreachable)
+          (drop (local.get $x))
+        )
+        (else
+          (unreachable)
+          (drop (local.get $x))
+        )
+      )
+      (drop (local.get $x))
+    )
+  )
+
+  (elem declare func $pow)
+  (type $pow (func (param $x i64) (param $n i32) (result i64)))
+  (func $pow (export "pow") (param $x i64) (param $n i32) (result i64)
+    (local $y i64)
+    (local $recurse (ref $pow))
+    (local.set $y
+      (if (result i64) (i32.and (local.get $n) (i32.const 1))
+        (then (local.get $x)) (else (i64.const 1))
+      )
+    )
+    (i64.mul
+      (block (result i64) (set $recurse)
+        (local.set $recurse (ref.func $pow))
+        (local.get $y)
+      )
+      (if (result i64) (i32.le_u (local.get $n) (i32.const 1))
+        (then (i64.const 1))
+        (else
+          (call_ref
+            (i64.mul (local.get $x) (local.get $x))
+            (i32.shr_u (local.get $n) (i32.const 1))
+            (local.get $recurse)
+          )
+        )
+      )
+    )
+  )
+)
+
+(assert_return (invoke "pow" (i64.const 17) (i32.const 0)) (i64.const 1))
+(assert_return (invoke "pow" (i64.const 19) (i32.const 1)) (i64.const 19))
+(assert_return (invoke "pow" (i64.const 11) (i32.const 2)) (i64.const 121))
+(assert_return (invoke "pow" (i64.const 13) (i32.const 3)) (i64.const 2197))
+(assert_return (invoke "pow" (i64.const 2) (i32.const 4)) (i64.const 16))
+(assert_return (invoke "pow" (i64.const 3) (i32.const 5)) (i64.const 243))
+(assert_return (invoke "pow" (i64.const 5) (i32.const 6)) (i64.const 15625))
+(assert_return (invoke "pow" (i64.const 7) (i32.const 7)) (i64.const 823543))
+
+(assert_invalid
+  (module
+    (type $t (func))
+    (func
+      (local $x (ref $t))
+      (local.get $x)
+      (drop)
+    )
+  )
+  "uninitialized local"
+)
+
+(assert_invalid
+  (module
+    (type $t (func))
+    (func
+      (local $x (ref $t))
+      (block
+        (local.get $x)
+        (drop)
+      )
+    )
+  )
+  "uninitialized local"
+)
+
+(assert_invalid
+  (module
+    (type $t (func))
+    (elem declare func $f)
+    (func $f
+      (local $x (ref $t))
+      (block (local.set $x (ref.func $f)))
+      (local.get $x)
+      (drop)
+    )
+  )
+  "uninitialized local"
+)
+
+(assert_invalid
+  (module
+    (type $t (func))
+    (elem declare func $f)
+    (func $f
+      (local $x (ref $t))
+      (block (set $x)
+        (block (local.set $x (ref.func $f)))
+      )
+    )
+  )
+  "uninitialized local"
+)
+
+(assert_invalid
+  (module
+    (type $t (func))
+    (elem declare func $f)
+    (func $f
+      (local $x (ref $t))
+      (block (set $x))
+      (local.get $x)
+      (drop)
+    )
+  )
+  "uninitialized local"
+)
+
+(assert_invalid
+  (module
+    (type $t (func))
+    (elem declare func $f)
+    (func $f
+      (local $x (ref $t))
+      (loop (set $x))
+      (local.get $x)
+      (drop)
+    )
+  )
+  "uninitialized local"
+)
+
+(assert_invalid
+  (module
+    (type $t (func))
+    (elem declare func $f)
+    (func $f
+      (local $x (ref $t))
+      (if (set $x) (then (local.set $x (ref.func $f))))
+      (local.get $x)
+      (drop)
+    )
+  )
+  "uninitialized local"
+)
+(assert_invalid
+  (module
+    (type $t (func))
+    (elem declare func $f)
+    (func $f
+      (local $x (ref $t))
+      (if (set $x) (then) (else (local.set $x (ref.func $f))))
+      (local.get $x)
+      (drop)
+    )
+  )
+  "uninitialized local"
+)
+
+(assert_invalid
+  (module
+    (type $t (func))
+    (elem declare func $f)
+    (func $f
+      (local $x (ref $t))
+      (block $l (set $x)
+        (i32.const 0)
+        (br_if $l)
+        (local.set $x (ref.func $f))
+      )
+      (local.get $x)
+      (drop)
+    )
+  )
+  "uninitialized local"
+)
+
+(assert_invalid
+  (module
+    (type $t (func))
+    (elem declare func $f)
+    (func $f
+      (local $x (ref $t))
+      (block $l (set $x)
+        (i32.const 0)
+        (br_table 1 1 $l 1)
+        (local.set $x (ref.func $f))
+      )
+      (local.get $x)
+      (drop)
+    )
+  )
+  "uninitialized local"
+)
+
+(assert_invalid
+  (module
+    (type $t (func))
+    (elem declare func $f)
+    (func $f
+      (local $x (ref $t))
+      (block $l (set $x)
+        (i32.const 0)
+        (br_table 1 1 $l)
+        (local.set $x (ref.func $f))
+      )
+      (local.get $x)
+      (drop)
+    )
+  )
+  "uninitialized local"
+)
diff --git a/test/core/local_get.wast b/test/core/local_get.wast
index 6acab398..b56aeec3 100644
--- a/test/core/local_get.wast
+++ b/test/core/local_get.wast
@@ -175,7 +175,7 @@
 )
 
 
-;; local.set should have retval
+;; Invalid result type
 
 (assert_invalid
   (module (func $type-empty-vs-i32 (local i32) (local.get 0)))
@@ -224,3 +224,42 @@
   "unknown local"
 )
 
+
+;; Uninitialized undefaulted locals
+
+(module
+  (func (export "get-after-set") (param $p (ref extern)) (result (ref extern))
+    (local $x (ref extern))
+    (local.set $x (local.get $p))
+    (local.get $x)
+  )
+  (func (export "get-after-tee") (param $p (ref extern)) (result (ref extern))
+    (local $x (ref extern))
+    (drop (local.tee $x (local.get $p)))
+    (local.get $x)
+  )
+  (func (export "get-in-block-after-set") (param $p (ref extern)) (result (ref extern))
+    (local $x (ref extern))
+    (local.set $x (local.get $p))
+    (block (result (ref extern)) (local.get $x))
+  )
+)
+
+(assert_return (invoke "get-after-set" (ref.extern 1)) (ref.extern 1))
+(assert_return (invoke "get-after-tee" (ref.extern 2)) (ref.extern 2))
+(assert_return (invoke "get-in-block-after-set" (ref.extern 3)) (ref.extern 3))
+
+(assert_invalid
+  (module (func $uninit (local $x (ref extern)) (drop (local.get $x))))
+  "uninitialized local"
+)
+(assert_invalid
+  (module
+    (func $uninit-after-end (param $p (ref extern))
+      (local $x (ref extern))
+      (block (local.set $x (local.get $p)) (drop (local.tee $x (local.get $p))))
+      (drop (local.get $x))
+    )
+  )
+  "uninitialized local"
+)