diff --git a/interpreter/binary/decode.ml b/interpreter/binary/decode.ml
index 85ad9687..4af12320 100644
--- a/interpreter/binary/decode.ml
+++ b/interpreter/binary/decode.ml
@@ -323,14 +323,7 @@ let rec instr s =
 
   | 0x16 as b -> illegal s pos b
 
-  | 0x17 ->
-    let bt = block_type s in
-    let locs = locals s in
-    let es = instr_block s in
-    end_ s;
-    let_ bt locs es
-
-  | 0x18 | 0x19 as b -> illegal s pos b
+  | 0x17 | 0x18 | 0x19 as b -> illegal s pos b
 
   | 0x1a -> drop
   | 0x1b -> select None
diff --git a/interpreter/binary/encode.ml b/interpreter/binary/encode.ml
index 4bfb59fb..5cab624d 100644
--- a/interpreter/binary/encode.ml
+++ b/interpreter/binary/encode.ml
@@ -189,8 +189,6 @@ struct
       op 0x04; block_type bt; list instr es1;
       if es2 <> [] then op 0x05;
       list instr es2; end_ ()
-    | Let (bt, locs, es) ->
-      op 0x17; block_type bt; locals locs; list instr es; end_ ()
 
     | Br x -> op 0x0c; var x
     | BrIf x -> op 0x0d; var x
diff --git a/interpreter/exec/eval.ml b/interpreter/exec/eval.ml
index d92b25dd..19074de0 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
@@ -64,7 +64,6 @@ and admin_instr' =
   | ReturningInvoke of value stack * func_inst
   | Breaking of int32 * value stack
   | Label of int * instr list * code
-  | Local of int * value list * code
   | Frame of int * frame * code
 
 type config =
@@ -74,8 +73,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
 
@@ -184,16 +183,6 @@ let rec step (c : config) : config =
         else
           vs', [Plain (Block (bt, es1)) @@ e.at]
 
-      | Let (bt, locals, es'), vs ->
-        let vs0, vs' = split (List.length locals) vs e.at in
-        let FuncType (ts1, ts2) = block_type c.frame.inst bt e.at in
-        let vs1, vs2 = split (List.length ts1) vs' e.at in
-        vs2, [
-          Local (List.length ts2, List.rev vs0,
-            (vs1, [Plain (Block (bt, es')) @@ e.at])
-          ) @@ e.at
-        ]
-
       | Br x, vs ->
         [], [Breaking (x.it, vs) @@ e.at]
 
@@ -266,14 +255,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 ->
@@ -676,18 +670,6 @@ let rec step (c : config) : config =
       let c' = step {c with code = code'} in
       vs, [Label (n, es0, c'.code) @@ e.at]
 
-    | Local (n, vs0, (vs', [])), vs ->
-      vs' @ vs, []
-
-    | Local (n, vs0, (vs', e' :: es')), vs when is_jumping e' ->
-      vs' @ vs, [e']
-
-    | Local (n, vs0, code'), vs ->
-      let frame' = {c.frame with locals = List.map ref vs0 @ 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
-      vs, [Local (n, vs0', c'.code) @@ e.at]
-
     | Frame (n, frame', (vs', [])), vs ->
       vs' @ vs, []
 
@@ -710,17 +692,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 (map Option.some args) @ 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/syntax/ast.ml b/interpreter/syntax/ast.ml
index 9552897d..9503b010 100644
--- a/interpreter/syntax/ast.ml
+++ b/interpreter/syntax/ast.ml
@@ -148,7 +148,6 @@ and instr' =
   | Block of block_type * instr list  (* execute in sequence *)
   | Loop of block_type * instr list   (* loop header *)
   | If of block_type * instr list * instr list   (* conditional *)
-  | Let of block_type * local list * instr list  (* local bindings *)
   | Br of idx                         (* break to n-th surrounding label *)
   | BrIf of idx                       (* conditional break *)
   | BrTable of idx list * idx         (* indexed break *)
diff --git a/interpreter/syntax/free.ml b/interpreter/syntax/free.ml
index cb8f2f65..66b8b789 100644
--- a/interpreter/syntax/free.ml
+++ b/interpreter/syntax/free.ml
@@ -108,9 +108,6 @@ let rec instr (e : instr) =
   | Const _ | Test _ | Compare _ | Unary _ | Binary _ | Convert _ -> empty
   | Block (bt, es) | Loop (bt, es) -> block_type bt ++ block es
   | If (bt, es1, es2) -> block_type bt ++ block es1 ++ block es2
-  | Let (bt, ts, es) ->
-    let free = block_type bt ++ block es in
-    {free with locals = Lib.Fun.repeat (List.length ts) shift free.locals}
   | Br x | BrIf x | BrOnNull x | BrOnNonNull x -> labels (idx x)
   | BrTable (xs, x) -> list (fun x -> labels (idx x)) (x::xs)
   | Return | CallRef | ReturnCallRef -> empty
diff --git a/interpreter/syntax/operators.ml b/interpreter/syntax/operators.ml
index de58f2ee..04464e5b 100644
--- a/interpreter/syntax/operators.ml
+++ b/interpreter/syntax/operators.ml
@@ -21,7 +21,6 @@ let select t = Select t
 let block bt es = Block (bt, es)
 let loop bt es = Loop (bt, es)
 let if_ bt es1 es2 = If (bt, es1, es2)
-let let_ bt ts es = Let (bt, ts, es)
 
 let br x = Br x
 let br_if x = BrIf x
diff --git a/interpreter/syntax/types.ml b/interpreter/syntax/types.ml
index 3e6c93b4..b9766b98 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
@@ -16,6 +19,7 @@ and value_type =
   NumType of num_type | VecType of vec_type | RefType of ref_type | BotType
 
 and result_type = value_type list
+and instr_type = result_type * result_type * local_idx list
 and func_type = FuncType of result_type * result_type
 and def_type = FuncDefType of func_type
 
@@ -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,12 @@ let string_of_name n =
   List.iter escape n;
   Buffer.contents b
 
+let string_of_idx x = I32.to_string_u x
+
 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;
diff --git a/interpreter/text/arrange.ml b/interpreter/text/arrange.ml
index 2b02848e..e1a40e43 100644
--- a/interpreter/text/arrange.ml
+++ b/interpreter/text/arrange.ml
@@ -448,9 +448,6 @@ let rec instr e =
     | If (bt, es1, es2) ->
       "if", block_type bt @
         [Node ("then", list instr es1); Node ("else", list instr es2)]
-    | Let (bt, locals, es) ->
-      "let", block_type bt @ decls "local" (List.map Source.it locals) @
-        list instr es
     | Br x -> "br " ^ var x, []
     | BrIf x -> "br_if " ^ var x, []
     | BrTable (xs, x) ->
diff --git a/interpreter/text/parser.mly b/interpreter/text/parser.mly
index a0ef1210..2aeb0ac1 100644
--- a/interpreter/text/parser.mly
+++ b/interpreter/text/parser.mly
@@ -142,19 +142,6 @@ let force_locals (c : context) =
   List.fold_right Stdlib.(@@) !(c.deferred_locals) ();
   c.deferred_locals := []
 
-let merge_locals (c : context) (c' : context) at =
-  force_locals c';  (* check that there aren't too many locals locally *)
-  if VarMap.is_empty c'.locals.map then
-    defer_locals c (fun () -> bind "local" c.locals c'.locals.count at)
-  else
-  (
-    force_locals c;
-    let n = c.locals.count in
-    ignore (bind "local" c.locals c'.locals.count at);
-    c.locals.map <- VarMap.union (fun x i1 i2 -> Some i1)
-      c.locals.map (scoped "local" n c'.locals at).map
-  )
-
 
 let lookup category space x =
   try VarMap.find x.it space.map
@@ -241,7 +228,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
 %token BR BR_IF BR_TABLE BR_ON_NULL BR_ON_NON_NULL
 %token CALL CALL_REF CALL_INDIRECT RETURN RETURN_CALL_REF
 %token LOCAL_GET LOCAL_SET LOCAL_TEE GLOBAL_GET GLOBAL_SET
@@ -618,10 +605,6 @@ block_instr :
   | IF labeling_opt block ELSE labeling_end_opt instr_list END labeling_end_opt
     { fun c -> let c' = $2 c ($5 @ $8) in
       let ts, es1 = $3 c' in if_ ts es1 ($6 c') }
-  | LET labeling_opt let_block END labeling_end_opt
-    { let at = at () in
-      fun c -> let c' = enter_let ($2 c $5) at in
-      let ts, ls, es = $3 c c' in let_ ts ls es }
 
 block :
   | type_use block_param_body
@@ -653,59 +636,6 @@ block_result_body :
       FuncType (ins, snd $3 c @ out), es }
 
 
-let_block :
-  | type_use let_block_param_body
-    { 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 }
-  | 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)
-      in bt, ls, es }
-
-let_block_param_body :
-  | let_block_result_body { $1 }
-  | LPAR PARAM value_type_list RPAR let_block_param_body
-    { fun c c' ->
-      let FuncType (ins, out), ls, es = $5 c c' in
-      FuncType (snd $3 c @ ins, out), ls, es }
-
-let_block_result_body :
-  | let_block_local_body
-    { let at = at () in
-      fun c c' -> let ls, es = $1 c c' at in FuncType ([], []), ls, es }
-  | LPAR RESULT value_type_list RPAR let_block_result_body
-    { fun c c' ->
-      let FuncType (ins, out), ls, es = $5 c c' in
-      FuncType (ins, snd $3 c @ out), ls, es }
-
-let_block_local_body :
-  | instr_list
-    { fun c c' at -> merge_locals c' c at; [], $1 c' }
-  | LPAR LOCAL local_type_list RPAR let_block_local_body
-    { let at3 = ati 3 in let at4 = ati 4 in
-      fun c c' at -> ignore (anon_locals c' (fst $3) at3);
-      let at' = {left = at.left; right = at4.right} in
-      let ls, es = $5 c c' at' in snd $3 c @ ls, es }
-  | LPAR LOCAL bind_var local_type RPAR let_block_local_body  /* Sugar */
-    { let at5 = ati 5 in
-      fun c c' at -> ignore (bind_local c' $3);
-      let at' = {left = at.left; right = at5.right} in
-      let ls, es = $6 c c' at' in $4 c :: ls, es }
-
-local_type :
-  | value_type { let at = at () in fun c -> $1 c @@ at }
-
-local_type_list :
-  | /* empty */ { 0l, fun c -> [] }
-  | local_type local_type_list { I32.add (fst $2) 1l, fun c -> $1 c :: snd $2 c }
-
 expr :  /* Sugar */
   | LPAR expr1 RPAR
     { let at = at () in fun c -> let es, e' = $2 c in es @ [e' @@ at] }
@@ -726,10 +656,6 @@ expr1 :  /* Sugar */
   | IF labeling_opt if_block
     { fun c -> let c' = $2 c [] in
       let bt, (es, es1, es2) = $3 c c' in es, if_ bt es1 es2 }
-  | LET labeling_opt let_block
-    { let at = at () in
-      fun c -> let c' = enter_let ($2 c []) at in
-      let bt, ls, es = $3 c c' in [], let_ bt ls es }
 
 select_expr_results :
   | LPAR RESULT value_type_list RPAR select_expr_results
@@ -893,6 +819,13 @@ func_body :
     { fun c -> ignore (bind_local c $3); let f = $6 c in
       {f with locals = $4 c :: f.locals} }
 
+local_type :
+  | value_type { let at = at () in fun c -> $1 c @@ at }
+
+local_type_list :
+  | /* empty */ { 0l, fun c -> [] }
+  | local_type local_type_list { I32.add (fst $2) 1l, fun c -> $1 c :: snd $2 c }
+
 
 /* Tables, Memories & Globals */
 
diff --git a/interpreter/util/lib.ml b/interpreter/util/lib.ml
index b0548100..1a4ce425 100644
--- a/interpreter/util/lib.ml
+++ b/interpreter/util/lib.ml
@@ -142,6 +142,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..164d4d9a 100644
--- a/interpreter/util/lib.mli
+++ b/interpreter/util/lib.mli
@@ -35,6 +35,7 @@ sig
   val make : 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/valid.ml b/interpreter/valid/valid.ml
index 3f8fa53d..2c4a0219 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,17 @@ 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 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 =
+  List.fold_left init_local c xs
+
 let func_type (c : context) x =
   match type_ c x with
   | FuncDefType ft -> ft
@@ -139,7 +150,8 @@ 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}
@@ -278,7 +290,7 @@ 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
+ *   t  : value_type
  *   ts : result_type
  *   x  : variable
  *
@@ -299,79 +311,70 @@ let check_block_type (c : context) (bt : block_type) at : func_type =
   | VarBlockType (SynVar x) -> func_type c (x @@ at)
   | VarBlockType (SemVar _) -> assert false
 
-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 init =
+    if not defaulted || defaultable_value_type t.it
+    then Initialized else Uninitialized
+  in LocalType (t.it, init)
 
-let rec check_instr (c : context) (e : instr) (s : infer_result_type) : op_type =
+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
+    (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
+    ts1 --> ts2, []
 
   | 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
+    ts1 --> ts2, []
 
   | 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 (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 c' =
-      { c with
-        labels = ts2 :: c.labels;
-        locals = List.map Source.it locals @ c.locals;
-      }
-    in check_block c' es ft e.at;
-    (ts1 @ List.map Source.it locals) --> ts2
+    (ts1 @ [NumType I32Type]) --> ts2, []
 
   | Br x ->
-    label c x -->... []
+    label c x -->... [], []
 
   | BrIf x ->
-    (label c x @ [NumType I32Type]) --> label c x
+    (label c x @ [NumType I32Type]) --> label c x, []
 
   | 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]) -->... []
+    (ts @ [NumType I32Type]) -->... [], []
 
   | BrOnNull x ->
     let (_, t) = peek_ref 0 s e.at in
     (label c x @ [RefType (Nullable, t)]) -->
-      (label c x @ [RefType (NonNullable, t)])
+      (label c x @ [RefType (NonNullable, t)]), []
 
   | BrOnNonNull x ->
     let (_, ht) as rt = peek_ref 0 s e.at in
@@ -383,22 +386,22 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : op_type
     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
+    (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" ^
@@ -411,7 +414,7 @@ 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
@@ -421,9 +424,9 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : op_type
         ("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))]) -->... []
+      (ts1 @ [RefType (nul, DefHeapType (SynVar x))]) -->... [], []
     | (_, BotHeapType) as rt ->
-      [RefType rt] -->... []
+      [RefType rt] -->... [], []
     | rt ->
       error e.at
         ("type mismatch: instruction requires function reference type" ^
@@ -431,42 +434,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
@@ -474,7 +481,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
@@ -482,191 +489,191 @@ 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) 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
+  let s, xs = check_seq c (stack ts1) es in
   let s' = pop c (stack ts2) s at in
   require (snd s' = []) at
     ("type mismatch: block requires " ^ string_of_result_type ts2 ^
@@ -690,10 +697,10 @@ 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]
     }
diff --git a/proposals/function-references/Overview.md b/proposals/function-references/Overview.md
index 5331d714..4a5fcafb 100644
--- a/proposals/function-references/Overview.md
+++ b/proposals/function-references/Overview.md
@@ -8,7 +8,7 @@ The proposal distinguished regular and nullable function reference. The former c
 
 The proposal has instructions for producing and consuming (calling) function references. It also includes instruction for testing and converting between regular and nullable references.
 
-Typed references have no canonical default value, because they cannot be null. To enable storing them in locals, which so far depend on default values for initialisation, the proposal also introduces a new instruction `let` for block-scoped locals whose initialisation values are taken from the operand stack.
+Typed references have no canonical default value, because they cannot be null. To enable storing them in locals, which so far depend on default values for initialisation, the proposal also tracks the initialisation status of locals during validation.
 
 
 ### Motivation
@@ -36,7 +36,7 @@ Typed references have no canonical default value, because they cannot be null. T
 
 * Refine the instruction `ref.func $f` to return a typed function reference
 
-* Add a block instruction `let (local t*) ... end` for introducing locals with block scope, in order to handle reference types without default initialisation values
+* Track initialisation status of locals during validation and only allow `local.get` after a `local.set/tee` in the same or a surrounding block.
 
 * Add an optional initialiser expression to table definitions, for element types that do not have an implicit default value.
 
@@ -168,6 +168,33 @@ 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
+
+
+#### Instruction Types
+
+* Instructions and instruction sequences are now typed with types of the following form:
+  - `instrtype ::= <functype> <localidx>*`
+  - 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 `[t1'*] -> [t2'*] <: [t3*] -> [t4*]*`
+    - and `{x2*} subset {x1*}`
+
+* Block types are instruction types with empty index set.
+
+Note: Extending block types with index sets to allow initialization status to last beyond a block's end is a possible extension.
+
+
 ### Instructions
 
 #### Functions
@@ -215,26 +242,43 @@ The following rules, now defined in terms of heap types, replace and extend the
 * Note: `ref.is_null` already exists via the [reference types proposal](https://github.com/WebAssembly/reference-types)
 
 
-#### Local Bindings
+#### Locals
 
-* `let <blocktype> (local <valtype>)* <instr>* end` locally binds operands to variables
-  - `let bt (local t)* instr* end : [t1* t*] -> [t2*]`
-    - iff `bt = [t1*] -> [t2*]`
-    - and `instr* : bt` under a context with `locals` extended with `t*` and `labels` extended with `[t2*]`
+Typing of local instructions is updated to account for the initialization status of locals.
 
-Note: The latter condition implies that inside the body of the `let`, its locals are prepended to the list of locals. Nesting multiple `let` blocks hence addresses them relatively, similar to labels. Function-level local declarations can be viewed as syntactic sugar for a bunch of zero constant instructions and a `let` wrapping the function body. That is,
-```
-(func ... (local t)* ...)
-```
-is equivalent to
-```
-(func ... (t.default)* (let (local t)* ...))
-```
-where `(t.default)` is `(t.const 0)` for numeric types `t`, and `(ref.null)` for reference types.
+* `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*`
+  - `instr1 instr* : [t1*] -> [t3*] x1* x2*`
+    - iff `instr1 : [t1*] -> [t2*] x1*`
+    - and `instr* : [t2*] -> [t3*] x2*` under a context where `x1*` are changed to `set`
+  - `epsilon : [] -> [] epsilon`
 
-The rule also implies that let-bound locals are mutable.
+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:
 
-Like all other block instructions, `let` binds a label
+* `instr`
+  - `instr : [t1*] -> [t2*] x*`
+    - iff `instr : [t1'*] -> [t2'*] x'*`
+    - and `[t1'*] -> [t2'*] x'*  <:  [t1*] -> [t2*] x*`
 
 
 ### Tables
@@ -273,7 +317,6 @@ The opcode for heap types is encoded as an `s33`.
 | ------ | ------------------------ | ---------- |
 | 0x14   | `call_ref`               |            |
 | 0x15   | `return_call_ref`        |            |
-| 0x17   | `let <bt> <locals>`      | `bt : blocktype, locals : (as in functions)` |
 | 0xd3   | `ref.as_non_null`        |            |
 | 0xd4   | `br_on_null $l`          | `$l : u32` |
 | 0xd6   | `br_on_non_null $l`      | `$l : u32` |
diff --git a/test/core/func.wast b/test/core/func.wast
index 46a01383..f2d18cc9 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"
 )
 
 
@@ -958,22 +961,28 @@
 
 ;; 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_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"
+)