diff --git a/document/core/appendix/index-instructions.py b/document/core/appendix/index-instructions.py
index 0c0ea6f0..c2d4fd13 100755
--- a/document/core/appendix/index-instructions.py
+++ b/document/core/appendix/index-instructions.py
@@ -279,7 +279,7 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat
     Instruction(None, r'\hex{CF}'),
     Instruction(r'\REFNULL~\X{ht}', r'\hex{D0}', r'[] \to [(\REF~\NULL~\X{ht})]', r'valid-ref.null', r'exec-ref.null'),
     Instruction(r'\REFISNULL', r'\hex{D1}', r'[(\REF~\NULL~\X{ht})] \to [\I32]', r'valid-ref.is_null', r'exec-ref.is_null'),
-    Instruction(r'\REFFUNC~x', r'\hex{D2}', r'[] \to [\FUNCREF]', r'valid-ref.func', r'exec-ref.func'),
+    Instruction(r'\REFFUNC~x', r'\hex{D2}', r'[] \to [\REF~\X{ht}]', r'valid-ref.func', r'exec-ref.func'),
     Instruction(None, r'\hex{D3}'),
     Instruction(r'\REFASNONNULL', r'\hex{D4}', r'[(\REF~\NULL~\X{ht})] \to [(\REF~\X{ht})]', r'valid-ref.as_non_null', r'exec-ref.as_non_null'),
     Instruction(r'\BRONNULL~l', r'\hex{D5}', r'[t^\ast~(\REF~\NULL~\X{ht})] \to [t^\ast~(\REF~\X{ht})]', r'valid-br_on_null', r'exec-br_on_null'),
diff --git a/document/core/binary/instructions.rst b/document/core/binary/instructions.rst
index 80ac806c..9693fc13 100644
--- a/document/core/binary/instructions.rst
+++ b/document/core/binary/instructions.rst
@@ -41,6 +41,7 @@ Control Instructions
 .. _binary-call_ref:
 .. _binary-call_indirect:
 .. _binary-return_call:
+.. _binary-return_call_ref:
 .. _binary-return_call_indirect:
 
 .. math::
diff --git a/document/core/binary/modules.rst b/document/core/binary/modules.rst
index 902f424a..9449f6f7 100644
--- a/document/core/binary/modules.rst
+++ b/document/core/binary/modules.rst
@@ -338,7 +338,7 @@ It decodes into a vector of :ref:`element segments <syntax-elem>` that represent
    \production{element segment} & \Belem &::=&
      0{:}\Bu32~~e{:}\Bexpr~~y^\ast{:}\Bvec(\Bfuncidx)
        &\Rightarrow& \\&&&\quad
-       \{ \ETYPE~\FUNCREF, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EACTIVE~\{ \ETABLE~0, \EOFFSET~e \} \} \\ &&|&
+       \{ \ETYPE~(\REF~\NULL~\FUNC), \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EACTIVE~\{ \ETABLE~0, \EOFFSET~e \} \} \\ &&|&
      1{:}\Bu32~~\X{et}:\Belemkind~~y^\ast{:}\Bvec(\Bfuncidx)
        &\Rightarrow& \\&&&\quad
        \{ \ETYPE~\X{et}, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EPASSIVE \} \\ &&|&
@@ -350,7 +350,7 @@ It decodes into a vector of :ref:`element segments <syntax-elem>` that represent
        \{ \ETYPE~\X{et}, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EDECLARATIVE \} \\ &&|&
      4{:}\Bu32~~e{:}\Bexpr~~\X{el}^\ast{:}\Bvec(\Bexpr)
        &\Rightarrow& \\&&&\quad
-       \{ \ETYPE~\FUNCREF, \EINIT~\X{el}^\ast, \EMODE~\EACTIVE~\{ \ETABLE~0, \EOFFSET~e \} \} \\ &&|&
+       \{ \ETYPE~(\REF~\NULL~\FUNC), \EINIT~\X{el}^\ast, \EMODE~\EACTIVE~\{ \ETABLE~0, \EOFFSET~e \} \} \\ &&|&
      5{:}\Bu32~~\X{et}:\Breftype~~\X{el}^\ast{:}\Bvec(\Bexpr)
        &\Rightarrow& \\&&&\quad
        \{ \ETYPE~et, \EINIT~\X{el}^\ast, \EMODE~\EPASSIVE \} \\ &&|&
diff --git a/document/core/syntax/types.rst b/document/core/syntax/types.rst
index 5d1b355c..1eb7b836 100644
--- a/document/core/syntax/types.rst
+++ b/document/core/syntax/types.rst
@@ -142,6 +142,13 @@ Other references are *non-null*.
 Reference types are *opaque*, meaning that neither their size nor their bit pattern can be observed.
 Values of reference type can be stored in :ref:`tables <syntax-table>`.
 
+Conventions
+...........
+
+* The reference type |FUNCREF| is an abbreviation for :math:`\REF~\NULL~\FUNC`.
+
+* The reference type |EXTERNREF| is an abbreviation for :math:`\REF~\NULL~\EXTERN`.
+
 
 .. index:: ! value type, number type, vector type, reference type, ! bottom type
    pair: abstract syntax; value type
diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst
index 05581d4e..e2825422 100644
--- a/document/core/valid/instructions.rst
+++ b/document/core/valid/instructions.rst
@@ -1649,9 +1649,9 @@ Control Instructions
 
 * The table :math:`C.\CTABLES[x]` must be defined in the context.
 
-* Let :math:`\limits~\reftype` be the :ref:`table type <syntax-tabletype>` :math:`C.\CTABLES[x]`.
+* Let :math:`\limits~t` be the :ref:`table type <syntax-tabletype>` :math:`C.\CTABLES[x]`.
 
-* The :ref:`reference type <syntax-reftype>` :math:`\reftype` must be |FUNCREF|.
+* The :ref:`reference type <syntax-reftype>` :math:`t` must :ref:`match <match-reftype>` type :math:`\REF~\NULL~\FUNC`.
 
 * The type :math:`C.\CTYPES[y]` must be defined in the context.
 
@@ -1663,7 +1663,9 @@ Control Instructions
 
 .. math::
    \frac{
-     C.\CTABLES[x] = \limits~\FUNCREF
+     C.\CTABLES[x] = \limits~t
+     \qquad
+     C \vdashvaltypematch t \matchesreftype \REF~\NULL~\FUNC
      \qquad
      C.\CTYPES[y] = [t_1^\ast] \toF C.\CRETURN
    }{
diff --git a/interpreter/README.md b/interpreter/README.md
index 6195e977..cd208195 100644
--- a/interpreter/README.md
+++ b/interpreter/README.md
@@ -221,7 +221,6 @@ expr:
   ( loop <name>? <block_type> <instr>* )
   ( if <name>? <block_type> ( then <instr>* ) ( else <instr>* )? )
   ( if <name>? <block_type> <expr>+ ( then <instr>* ) ( else <instr>* )? ) ;; = <expr>+ (if <name>? <block_type> (then <instr>*) (else <instr>*)?)
-  ( let <name>? <block_type> <local>* <instr>* )
 
 instr:
   <expr>
@@ -230,7 +229,6 @@ instr:
   loop <name>? <block_type> <instr>* end <name>?                     ;; = (loop <name>? <block_type> <instr>*)
   if <name>? <block_type> <instr>* end <name>?                       ;; = (if <name>? <block_type> (then <instr>*))
   if <name>? <block_type> <instr>* else <name>? <instr>* end <name>? ;; = (if <name>? <block_type> (then <instr>*) (else <instr>*))
-  let <name>? <block_type> <local>* <instr>* end <name>?             ;; = (let <name>? <block_type> <local>* <instr>*)
 
 op:
   unreachable
diff --git a/test/core/binary.wast b/test/core/binary.wast
index 65407391..1661a1c6 100644
--- a/test/core/binary.wast
+++ b/test/core/binary.wast
@@ -1132,4 +1132,3 @@
   )
   "unexpected content after last section"
 )
-