diff --git a/document/core/appendix/algorithm.rst b/document/core/appendix/algorithm.rst
index 259b0107..f13ddc3e 100644
--- a/document/core/appendix/algorithm.rst
+++ b/document/core/appendix/algorithm.rst
@@ -22,48 +22,29 @@ Data Structures
 ~~~~~~~~~~~~~~~
 
 Types are representable as an enumeration.
-In addition to the plain types from the WebAssembly validation semantics, an extended notion of operand type includes a bottom type `Unknown` that is used as the type of :ref:`polymorphic <polymorphism>` operands.
-
 A simple subtyping check can be defined on these types.
-In addition, corresponding functions computing the join (least upper bound) and meet (greatest lower bound) of two types are used.
-Because there is no top type, a join does not exist in all cases.
-Similarly, a meet must always be defined on known value types that exclude the auxiliary bottom type `Unknown`,
-hence a meet does not exist in all cases either.
-A type error is encountered if a join or meet is required when it does not exist.
 
 .. code-block:: pseudo
 
-   type val_type = I32 | I64 | F32 | F64 | Anyref | Funcref | Nullref
-   type opd_type = val_type | Unknown
+   type val_type = I32 | I64 | F32 | F64 | Anyref | Funcref | Nullref | Bot
+
+   func is_num(t : val_type) : bool =
+     return t = I32 || t = I64 || t = F32 || t = F64 || t = Bot
 
-   func is_ref(t : opd_type) : bool =
-     return t = Anyref || t = Funcref || t = Nullref
+   func is_ref(t : val_type) : bool =
+     return t = Anyref || t = Funcref || t = Nullref || t = Bot
 
-   func matches(t1 : opd_type, t2 : opd_type) : bool =
-     return t1 = t2 || t1 = Unknown ||
+   func matches(t1 : val_type, t2 : val_type) : bool =
+     return t1 = t2 || t1 = Bot ||
        (t1 = Nullref && is_ref(t2)) || (is_ref(t1) && t2 = Anyref)
 
-   func join(t1 : opd_type, t2 : opd_type) : opd_type =
-     if (t1 = t2) return t1
-     if (matches(t1, t2)) return t2
-     if (matches(t2, t1)) return t1
-     error_if(not (is_ref(t1) && is_ref(t2)))
-     return Anyref
-
-   func meet(t1 : val_type, t2 : val_type) : val_type =
-     if (t1 = t2) return t1
-     if (matches(t1, t2)) return t1
-     if (matches(t2, t1)) return t2
-     error_if(not (is_ref(t1) && is_ref(t2)))
-     return Nullref
-
-The algorithm uses two separate stacks: the *operand stack* and the *control stack*.
+The algorithm uses two separate stacks: the *value stack* and the *control stack*.
 The former tracks the :ref:`types <syntax-valtype>` of operand values on the :ref:`stack <stack>`,
 the latter surrounding :ref:`structured control instructions <syntax-instr-control>` and their associated :ref:`blocks <syntax-instr-control>`.
 
 .. code-block:: pseudo
 
-   type opd_stack = stack(opd_type)
+   type val_stack = stack(val_type)
 
    type ctrl_stack = stack(ctrl_frame)
    type ctrl_frame = {
@@ -73,7 +54,7 @@ the latter surrounding :ref:`structured control instructions <syntax-instr-contr
      unreachable : bool
    }
 
-For each value, the operand stack records its :ref:`value type <syntax-valtype>`, or :code:`Unknown` when the type is not known.
+For each value, the value stack records its :ref:`value type <syntax-valtype>`.
 
 For each entered block, the control stack records a *control frame* with the type of the associated :ref:`label <syntax-label>` (used to type-check branches), the result type of the block (used to check its result), the height of the operand stack at the start of the block (used to check that operands do not underflow the current block), and a flag recording whether the remainder of the block is unreachable (used to handle :ref:`stack-polymorphic <polymorphism>` typing after branches).
 
@@ -85,43 +66,48 @@ For the purpose of presenting the algorithm, the operand and control stacks are
 
 .. code-block:: pseudo
 
-   var opds : opd_stack
+   var vals : val_stack
    var ctrls : ctrl_stack
 
 However, these variables are not manipulated directly by the main checking function, but through a set of auxiliary functions:
 
 .. code-block:: pseudo
 
-   func push_opd(type : opd_type) =
-     opds.push(type)
+   func push_val(type : val_type) =
+     vals.push(type)
 
-   func pop_opd() : opd_type =
-     if (opds.size() = ctrls[0].height && ctrls[0].unreachable) return Unknown
-     error_if(opds.size() = ctrls[0].height)
-     return opds.pop()
+   func pop_val() : val_type =
+     if (vals.size() = ctrls[0].height && ctrls[0].unreachable) return Bot
+     error_if(vals.size() = ctrls[0].height)
+     return vals.pop()
 
-   func pop_opd(expect : val_type) =
-     let actual = pop_opd()
+   func pop_val(expect : val_type) : val_type =
+     let actual = pop_val()
      error_if(not matches(actual, expect))
+     return actual
 
-   func push_opds(types : list(val_type)) = foreach (t in types) push_opd(t)
-   func pop_opds(types : list(val_type)) = foreach (t in reverse(types)) pop_opd(t)
+   func push_vals(types : list(val_type)) = foreach (t in types) push_val(t)
+   func pop_vals(types : list(val_type)) : list(val_type) =
+     var popped := []
+     foreach (t in reverse(types)) popped.append(pop_val(t))
+     return popped
 
-Pushing an operand simply pushes the respective type to the operand stack.
+Pushing an operand value simply pushes the respective type to the value stack.
 
-Popping an operand checks that the operand stack does not underflow the current block and then removes one type.
-But first, a special case is handled where the block contains no known operands, but has been marked as unreachable.
+Popping an operand value checks that the value stack does not underflow the current block and then removes one type.
+But first, a special case is handled where the block contains no known values, but has been marked as unreachable.
 That can occur after an unconditional branch, when the stack is typed :ref:`polymorphically <polymorphism>`.
-In that case, an unknown type is returned.
+In that case, the :code:`Bot` type is returned, because that is a *principal* choice trivially satisfying all use constraints.
 
-A second function for popping an operand takes an expected (known) type, which the actual operand type is checked against.
-The types may differ by subtyping, inlcuding the case where the actual type is unknown.
+A second function for popping an operand value takes an expected type, which the actual operand type is checked against.
+The types may differ by subtyping, including the case where the actual type is :code:`Bot`, and thereby matches unconditionally.
+The function returns the actual type popped from the stack.
 
 Finally, there are accumulative functions for pushing or popping multiple operand types.
 
 .. note::
    The notation :code:`stack[i]` is meant to index the stack from the top,
-   so that :code:`ctrls[0]` accesses the element pushed last.
+   so that, e.g., :code:`ctrls[0]` accesses the element pushed last.
 
 
 The control stack is likewise manipulated through auxiliary functions:
@@ -129,19 +115,19 @@ The control stack is likewise manipulated through auxiliary functions:
 .. code-block:: pseudo
 
    func push_ctrl(label : list(val_type), out : list(val_type)) =
-     let frame = ctrl_frame(label, out, opds.size(), false)
+     let frame = ctrl_frame(label, out, vals.size(), false)
      ctrls.push(frame)
 
    func pop_ctrl() : list(val_type) =
      error_if(ctrls.is_empty())
      let frame = ctrls[0]
-     pop_opds(frame.end_types)
-     error_if(opds.size() =/= frame.height)
+     pop_vals(frame.end_types)
+     error_if(vals.size() =/= frame.height)
      ctrls.pop()
      return frame.end_types
 
    func unreachable() =
-     opds.resize(ctrls[0].height)
+     vals.resize(ctrls[0].height)
      ctrls[0].unreachable := true
 
 Pushing a control frame takes the types of the label and result values.
@@ -152,18 +138,18 @@ It then verifies that the operand stack contains the right types of values expec
 Afterwards, it checks that the stack has shrunk back to its initial height.
 
 Finally, the current frame can be marked as unreachable.
-In that case, all existing operand types are purged from the operand stack, in order to allow for the :ref:`stack-polymorphism <polymorphism>` logic in :code:`pop_opd` to take effect.
+In that case, all existing operand types are purged from the value stack, in order to allow for the :ref:`stack-polymorphism <polymorphism>` logic in :code:`pop_val` to take effect.
 
 .. note::
    Even with the unreachable flag set, consecutive operands are still pushed to and popped from the operand stack.
    That is necessary to detect invalid :ref:`examples <polymorphism>` like :math:`(\UNREACHABLE~(\I32.\CONST)~\I64.\ADD)`.
-   However, a polymorphic stack cannot underflow, but instead generates :code:`Unknown` types as needed.
+   However, a polymorphic stack cannot underflow, but instead generates :code:`Bot` types as needed.
 
 
 .. index:: opcode
 
-Validation of Opcode Sequences
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Validation of Instruction Sequences
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 The following function shows the validation of a number of representative instructions that manipulate the stack.
 Other instructions are checked in a similar manner.
@@ -177,18 +163,26 @@ Other instructions are checked in a similar manner.
    func validate(opcode) =
      switch (opcode)
        case (i32.add)
-         pop_opd(I32)
-         pop_opd(I32)
-         push_opd(I32)
+         pop_val(I32)
+         pop_val(I32)
+         push_val(I32)
 
        case (drop)
-         pop_opd()
+         pop_val()
 
        case (select)
-         pop_opd(I32)
-         let t1 = pop_opd()
-         let t2 = pop_opd()
-         push_opd(join(t1, t2))
+         pop_val(I32)
+         let t1 = pop_val()
+         let t2 = pop_val()
+         error_if(not (is_num(t1) && is_num(t2)))
+         error_if(t1 =/= t2 && t1 =/= Bot && t2 =/= Bot)
+         push_val(if (t1 = Bot) t2 else t1)
+
+       case (select t)
+         pop_val(I32)
+         pop_val(t)
+         pop_val(t)
+         push_val(t)
 
        case (unreachable)
          unreachable()
@@ -200,12 +194,12 @@ Other instructions are checked in a similar manner.
          push_ctrl([], [t*])
 
        case (if t*)
-         pop_opd(I32)
+         pop_val(I32)
          push_ctrl([t*], [t*])
 
        case (end)
          let results = pop_ctrl()
-         push_opds(results)
+         push_vals(results)
 
        case (else)
          let results = pop_ctrl()
@@ -213,26 +207,22 @@ Other instructions are checked in a similar manner.
 
        case (br n)
          error_if(ctrls.size() < n)
-         pop_opds(ctrls[n].label_types)
+         pop_vals(ctrls[n].label_types)
          unreachable()
 
        case (br_if n)
          error_if(ctrls.size() < n)
-         pop_opd(I32)
-         pop_opds(ctrls[n].label_types)
-         push_opds(ctrls[n].label_types)
+         pop_val(I32)
+         pop_vals(ctrls[n].label_types)
+         push_vals(ctrls[n].label_types)
 
        case (br_table n* m)
+         pop_val(I32)
          error_if(ctrls.size() < m)
-         var ts = ctrls[m].label_types
+         let arity = ctrls[m].label_types.size()
          foreach (n in n*)
            error_if(ctrls.size() < n)
-           ts := meet(ts, ctrls[n].label_types)
-         pop_opd(I32)
-         pop_opds(ts)
+           error_if(ctrls[n].label_types.size() =/= arity)
+           push_vals(pop_vals(ctrls[n].label_types))
+         pop_vals(ctrls[m].label_types)
          unreachable()
-
-.. note::
-   It is an invariant under the current WebAssembly instruction set that an operand of :code:`Unknown` type is never duplicated on the stack.
-   This would change if the language were extended with stack operators like :code:`dup`.
-   Under such an extension, the above algorithm would need to be refined by replacing the :code:`Unknown` type with proper *type variables* to ensure that all uses are consistent.
diff --git a/document/core/appendix/index-instructions.rst b/document/core/appendix/index-instructions.rst
index 29ee73d6..394a98e5 100644
--- a/document/core/appendix/index-instructions.rst
+++ b/document/core/appendix/index-instructions.rst
@@ -35,7 +35,7 @@ Instruction                             Binary Opcode     Type
 (reserved)                              :math:`\hex{19}`                                                  
 :math:`\DROP`                           :math:`\hex{1A}`  :math:`[t] \to []`                          :ref:`validation <valid-drop>`            :ref:`execution <exec-drop>`
 :math:`\SELECT`                         :math:`\hex{1B}`  :math:`[t~t~\I32] \to [t]`                  :ref:`validation <valid-select>`          :ref:`execution <exec-select>`
-(reserved)                              :math:`\hex{1C}`                                                  
+:math:`\SELECT~t`                       :math:`\hex{1C}`  :math:`[t~t~\I32] \to [t]`                  :ref:`validation <valid-select>`          :ref:`execution <exec-select>`
 (reserved)                              :math:`\hex{1D}`                                                  
 (reserved)                              :math:`\hex{1E}`                                                  
 (reserved)                              :math:`\hex{1F}`                                                  
diff --git a/document/core/binary/instructions.rst b/document/core/binary/instructions.rst
index e1ad15ce..27deed05 100644
--- a/document/core/binary/instructions.rst
+++ b/document/core/binary/instructions.rst
@@ -92,7 +92,7 @@ Reference Instructions
 Parametric Instructions
 ~~~~~~~~~~~~~~~~~~~~~~~
 
-:ref:`Parametric instructions <syntax-instr-parametric>` are represented by single byte codes.
+:ref:`Parametric instructions <syntax-instr-parametric>` are represented by single byte codes, possibly followed by a type annotation.
 
 .. _binary-drop:
 .. _binary-select:
@@ -101,7 +101,8 @@ Parametric Instructions
    \begin{array}{llclll}
    \production{instruction} & \Binstr &::=& \dots \\ &&|&
      \hex{1A} &\Rightarrow& \DROP \\ &&|&
-     \hex{1B} &\Rightarrow& \SELECT \\
+     \hex{1B} &\Rightarrow& \SELECT \\ &&|&
+     \hex{1C}~~t^\ast{:}\Bvec(\Bvaltype) &\Rightarrow& \SELECT~t^\ast \\
    \end{array}
 
 
diff --git a/document/core/binary/types.rst b/document/core/binary/types.rst
index 8e99de82..541f45db 100644
--- a/document/core/binary/types.rst
+++ b/document/core/binary/types.rst
@@ -45,6 +45,9 @@ Reference Types
      \hex{6F} &\Rightarrow& \ANYREF \\
    \end{array}
 
+.. note::
+   The type :math:`\NULLREF` cannot occur in a module.
+
 
 .. index:: value type, number type, reference type
    pair: binary format; value type
@@ -62,6 +65,9 @@ Value Types
      t{:}\Breftype &\Rightarrow& t \\
    \end{array}
 
+.. note::
+   The type :math:`\BOT` cannot occur in a module.
+
 
 .. index:: result type, value type
    pair: binary format; result type
diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst
index 91452e8c..b1e9c1d0 100644
--- a/document/core/exec/instructions.rst
+++ b/document/core/exec/instructions.rst
@@ -264,8 +264,8 @@ Parametric Instructions
 
 .. _exec-select:
 
-:math:`\SELECT`
-...............
+:math:`\SELECT~(t^\ast)^?`
+..........................
 
 1. Assert: due to :ref:`validation <valid-select>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.
 
@@ -287,12 +287,15 @@ Parametric Instructions
 
 .. math::
    \begin{array}{lcl@{\qquad}l}
-   \val_1~\val_2~(\I32\K{.}\CONST~c)~\SELECT &\stepto& \val_1
+   \val_1~\val_2~(\I32\K{.}\CONST~c)~\SELECT~t^? &\stepto& \val_1
      & (\iff c \neq 0) \\
-   \val_1~\val_2~(\I32\K{.}\CONST~c)~\SELECT &\stepto& \val_2
+   \val_1~\val_2~(\I32\K{.}\CONST~c)~\SELECT~t^? &\stepto& \val_2
      & (\iff c = 0) \\
    \end{array}
 
+.. note::
+   In future versions of WebAssembly, |SELECT| may allow more than one value per choice.
+
 
 .. index:: variable instructions, local index, global index, address, global address, global instance, store, frame, value
    pair: execution; instruction
diff --git a/document/core/syntax/instructions.rst b/document/core/syntax/instructions.rst
index c4806d5c..7fe2a3af 100644
--- a/document/core/syntax/instructions.rst
+++ b/document/core/syntax/instructions.rst
@@ -205,12 +205,16 @@ Instructions in this group can operate on operands of any :ref:`value type <synt
    \production{instruction} & \instr &::=&
      \dots \\&&|&
      \DROP \\&&|&
-     \SELECT
+     \SELECT~(\valtype^\ast)^? \\
    \end{array}
 
 The |DROP| operator simply throws away a single operand.
 
 The |SELECT| operator selects one of its first two operands based on whether its third operand is zero or not.
+It may include a :ref:`value type <syntax-valtype>` determining the type of these operands. If missing, the operands must be of :ref:`numeric type <syntax-numtype>`.
+
+.. note::
+   In future versions of WebAssembly, the type annotation on |SELECT| may allow for more than a single value being selected at the same time.
 
 
 .. index:: ! variable instruction, local, global, local index, global index
diff --git a/document/core/syntax/types.rst b/document/core/syntax/types.rst
index ee722c6e..522e4795 100644
--- a/document/core/syntax/types.rst
+++ b/document/core/syntax/types.rst
@@ -63,7 +63,7 @@ The type |FUNCREF| denotes the infinite union of all references to :ref:`functio
 
 The type |NULLREF| only contains a single value: the :ref:`null <syntax-ref.null>` reference.
 It is a :ref:`subtype <match-reftype>` of all other reference types.
-By virtue of not being representable in either the :ref:`binary format <binary-reftype>` nor the :ref:`text format <text-reftype>`, the |NULLREF| type cannot be used in a program;
+By virtue of being representable in neither the :ref:`binary format <binary-reftype>` nor the :ref:`text format <text-reftype>`, the |NULLREF| type cannot be used in a program;
 it only occurs during :ref:`validation <valid>`.
 
 .. note::
@@ -73,7 +73,7 @@ Reference types are *opaque*, meaning that neither their size nor their bit patt
 Values of reference type can be stored in :ref:`tables <syntax-table>`.
 
 
-.. index:: ! value type, number type, reference type
+.. index:: ! value type, number type, reference type, ! bottom type
    pair: abstract syntax; value type
    pair: value; type
 .. _syntax-valtype:
@@ -82,11 +82,16 @@ Value Types
 ~~~~~~~~~~~
 
 *Value types* classify the individual values that WebAssembly code can compute with and the values that a variable accepts.
+They are either :ref:`number types <syntax-numtype>`, :ref:`reference type <syntax-reftype>`, or the unique *bottom type*, written :math:`\BOT`.
+
+The type :math:`\BOT` is a :ref:`subtype <match-valtype>` of all other types.
+By virtue of being representable in neither the :ref:`binary format <binary-valtype>` nor the :ref:`text format <text-valtype>`, it cannot be used in a program;
+it only occurs during :ref:`validation <valid>`.
 
 .. math::
    \begin{array}{llll}
    \production{value type} & \valtype &::=&
-     \numtype ~|~ \reftype \\
+     \numtype ~|~ \reftype ~|~ \BOT \\
    \end{array}
 
 Conventions
diff --git a/document/core/text/instructions.rst b/document/core/text/instructions.rst
index e51fa805..d5901a87 100644
--- a/document/core/text/instructions.rst
+++ b/document/core/text/instructions.rst
@@ -163,7 +163,7 @@ Parametric Instructions
    \begin{array}{llclll}
    \production{instruction} & \Tplaininstr_I &::=& \dots \\ &&|&
      \text{drop} &\Rightarrow& \DROP \\ &&|&
-     \text{select} &\Rightarrow& \SELECT \\
+     \text{select}~((t{:}\Tresult)^\ast)^? &\Rightarrow& \SELECT~(t^\ast)^? \\
    \end{array}
 
 
diff --git a/document/core/util/macros.def b/document/core/util/macros.def
index d66f9a52..85cbef86 100644
--- a/document/core/util/macros.def
+++ b/document/core/util/macros.def
@@ -164,6 +164,8 @@
 
 .. |to| mathdef:: \xref{syntax/types}{syntax-functype}{\rightarrow}
 
+.. |BOT| mathdef:: \xref{syntax/types}{syntax-valtype}{\K{bot}}
+
 .. |I8| mathdef:: \xref{exec/runtime}{syntax-storagetype}{\K{i8}}
 .. |I16| mathdef:: \xref{exec/runtime}{syntax-storagetype}{\K{i16}}
 .. |I32| mathdef:: \xref{syntax/types}{syntax-valtype}{\K{i32}}
diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst
index 16a432c1..cf38da6a 100644
--- a/document/core/valid/instructions.rst
+++ b/document/core/valid/instructions.rst
@@ -35,7 +35,7 @@ Two degrees of polymorphism can be distinguished:
 In both cases, the unconstrained types or type sequences can be chosen arbitrarily, as long as they meet the constraints imposed for the surrounding parts of the program.
 
 .. note::
-   For example, the |SELECT| instruction is valid with type :math:`[t~t~\I32] \to [t]`, for any possible :ref:`value type <syntax-valtype>` :math:`t`.   Consequently, both instruction sequences
+   For example, the |SELECT| instruction is valid with type :math:`[t~t~\I32] \to [t]`, for any possible :ref:`number type <syntax-numtype>` :math:`t`.   Consequently, both instruction sequences
 
    .. math::
       (\I32.\CONST~1)~~(\I32.\CONST~2)~~(\I32.\CONST~3)~~\SELECT{}
@@ -61,6 +61,8 @@ In both cases, the unconstrained types or type sequences can be chosen arbitrari
 
    is invalid, because there is no possible type to pick for the |UNREACHABLE| instruction that would make the sequence well-typed.
 
+The :ref:`Appendix <algo-valid>` describes a type checking :ref:`algorithm <algo-valid>` that efficiently implements validation of instruction sequences as prescribed by the rules given here.
+
 
 .. index:: numeric instruction
    pair: validation; instruction
@@ -227,22 +229,40 @@ Parametric Instructions
      C \vdashinstr \DROP : [t] \to []
    }
 
+.. note::
+   Both |DROP| and |SELECT| without annotation are :ref:`value-polymorphic <polymorphism>` instructions.
+
+
 
 .. _valid-select:
 
-:math:`\SELECT`
-...............
+:math:`\SELECT~(t^\ast)^?`
+..........................
+
+* If :math:`t^\ast` is present, then:
+
+  * The length of :math:`t^\ast` must be :math:`1`.
 
-* The instruction is valid with type :math:`[t~t~\I32] \to [t]`, for any :ref:`value type <syntax-valtype>` :math:`t`.
+  * Then the instruction is valid with type :math:`[t^\ast~t^\ast~\I32] \to [t^\ast]`.
+
+* Else:
+
+  * The instruction is valid with type :math:`[t~t~\I32] \to [t]`, for any :ref:`value type <syntax-valtype>` :math:`t` that :ref:`matches <match-valtype>` some :ref:`number type <syntax-numtype>`.
 
 .. math::
    \frac{
+   }{
+     C \vdashinstr \SELECT~t : [t~t~\I32] \to [t]
+   }
+   \qquad
+   \frac{
+     \vdashvaltypematch t \matchesvaltype \numtype
    }{
      C \vdashinstr \SELECT : [t~t~\I32] \to [t]
    }
 
 .. note::
-   Both |DROP| and |SELECT| are :ref:`value-polymorphic <polymorphism>` instructions.
+   In future versions of WebAssembly, |SELECT| may allow more than one value per choice.
 
 
 .. index:: variable instructions, local index, global index, context
diff --git a/document/core/valid/types.rst b/document/core/valid/types.rst
index 44536f22..37aa01ee 100644
--- a/document/core/valid/types.rst
+++ b/document/core/valid/types.rst
@@ -270,6 +270,15 @@ A :ref:`value type <syntax-valtype>` :math:`\valtype_1` matches a :ref:`value ty
 
 * Or both :math:`\valtype_1` and :math:`\valtype_2` are :ref:`reference types <syntax-reftype>` and :math:`\valtype_1` :ref:`matches <match-reftype>` :math:`\valtype_2`.
 
+* Or :math:`\valtype_1` is :math:`\BOT`.
+
+.. math::
+   ~\\[-1ex]
+   \frac{
+   }{
+     \vdashvaltypematch \BOT \matchesvaltype \valtype
+   }
+
 
 .. _match-resulttype:
 
diff --git a/interpreter/binary/decode.ml b/interpreter/binary/decode.ml
index 08e41d36..691778de 100644
--- a/interpreter/binary/decode.ml
+++ b/interpreter/binary/decode.ml
@@ -258,9 +258,10 @@ let rec instr s =
   | 0x12 | 0x13 | 0x14 | 0x15 | 0x16 | 0x17 | 0x18 | 0x19 as b -> illegal s pos b
 
   | 0x1a -> drop
-  | 0x1b -> select
+  | 0x1b -> select None
+  | 0x1c -> select (Some (vec value_type s))
 
-  | 0x1c | 0x1d | 0x1e | 0x1f as b -> illegal s pos b
+  | 0x1d | 0x1e | 0x1f as b -> illegal s pos b
 
   | 0x20 -> local_get (at var s)
   | 0x21 -> local_set (at var s)
diff --git a/interpreter/binary/encode.ml b/interpreter/binary/encode.ml
index 7519bc2e..3d7d13a5 100644
--- a/interpreter/binary/encode.ml
+++ b/interpreter/binary/encode.ml
@@ -104,6 +104,7 @@ let encode m =
     let value_type = function
       | NumType t -> num_type t
       | RefType t -> ref_type t
+      | BotType -> assert false
 
     let stack_type = function
       | [] -> vs7 (-0x40)
@@ -166,7 +167,8 @@ let encode m =
       | CallIndirect (x, y) -> op 0x11; var y; var x
 
       | Drop -> op 0x1a
-      | Select -> op 0x1b
+      | Select None -> op 0x1b
+      | Select (Some ts) -> op 0x1c; vec value_type ts
 
       | LocalGet x -> op 0x20; var x
       | LocalSet x -> op 0x21; var x
diff --git a/interpreter/exec/eval.ml b/interpreter/exec/eval.ml
index 84eb2f4e..03a4ff30 100644
--- a/interpreter/exec/eval.ml
+++ b/interpreter/exec/eval.ml
@@ -172,10 +172,10 @@ let rec step (c : config) : config =
       | Drop, v :: vs' ->
         vs', []
 
-      | Select, Num (I32 0l) :: v2 :: v1 :: vs' ->
+      | Select _, Num (I32 0l) :: v2 :: v1 :: vs' ->
         v2 :: vs', []
 
-      | Select, Num (I32 i) :: v2 :: v1 :: vs' ->
+      | Select _, Num (I32 i) :: v2 :: v1 :: vs' ->
         v1 :: vs', []
 
       | LocalGet x, vs ->
diff --git a/interpreter/host/spectest.ml b/interpreter/host/spectest.ml
index c343e1bb..a8d32aa5 100644
--- a/interpreter/host/spectest.ml
+++ b/interpreter/host/spectest.ml
@@ -15,6 +15,7 @@ let global (GlobalType (t, _) as gt) =
     | NumType F32Type -> Num (F32 (F32.of_float 666.6))
     | NumType F64Type -> Num (F64 (F64.of_float 666.6))
     | RefType _ -> Ref NullRef
+    | BotType -> assert false
   in Global.alloc gt v
 
 let table =
diff --git a/interpreter/script/js.ml b/interpreter/script/js.ml
index fe89d768..6f5c3e6c 100644
--- a/interpreter/script/js.ml
+++ b/interpreter/script/js.ml
@@ -306,6 +306,7 @@ let assert_return_nan_bitpattern nan_bitmask_of ts at =
         Test (Values.I32 I32Op.Eqz) @@ at;
         BrIf (0l @@ at) @@ at ]
     | RefType _ -> [Br (0l @@ at) @@ at]
+    | BotType -> assert false
   in [], List.flatten (List.rev_map test ts)
 
 let assert_return_canonical_nan = assert_return_nan_bitpattern abs_mask_of
@@ -317,6 +318,7 @@ let assert_return_ref ts at =
     | RefType _ ->
       [ RefIsNull @@ at;
         BrIf (0l @@ at) @@ at ]
+    | BotType -> assert false
   in [], List.flatten (List.rev_map test ts)
 
 let assert_return_func ts at =
@@ -326,6 +328,7 @@ let assert_return_func ts at =
       [ Call (is_funcref_idx @@ at) @@ at;
         Test (Values.I32 I32Op.Eqz) @@ at;
         BrIf (0l @@ at) @@ at ]
+    | BotType -> assert false
   in [], List.flatten (List.rev_map test ts)
 
 let wrap item_name wrap_action wrap_assertion at =
@@ -374,6 +377,7 @@ let is_js_num_type = function
 let is_js_value_type = function
   | NumType t -> is_js_num_type t
   | RefType t -> true
+  | BotType -> assert false
 
 let is_js_global_type = function
   | GlobalType (t, mut) -> is_js_value_type t && mut = Immutable
diff --git a/interpreter/syntax/ast.ml b/interpreter/syntax/ast.ml
index 93fed9ea..06e75c39 100644
--- a/interpreter/syntax/ast.ml
+++ b/interpreter/syntax/ast.ml
@@ -71,7 +71,7 @@ and instr' =
   | Unreachable                       (* trap unconditionally *)
   | Nop                               (* do nothing *)
   | Drop                              (* forget a value *)
-  | Select                            (* branchless conditional *)
+  | Select of value_type list option  (* branchless conditional *)
   | Block of stack_type * instr list  (* execute in sequence *)
   | Loop of stack_type * instr list   (* loop header *)
   | If of stack_type * instr list * instr list  (* conditional *)
diff --git a/interpreter/syntax/operators.ml b/interpreter/syntax/operators.ml
index 3fb6a4b4..2ff649b6 100644
--- a/interpreter/syntax/operators.ml
+++ b/interpreter/syntax/operators.ml
@@ -16,7 +16,7 @@ let ref_is_null = RefIsNull
 let unreachable = Unreachable
 let nop = Nop
 let drop = Drop
-let select = Select
+let select t = Select t
 let block ts es = Block (ts, es)
 let loop ts es = Loop (ts, es)
 let br x = Br x
diff --git a/interpreter/syntax/types.ml b/interpreter/syntax/types.ml
index 3e429db6..fb3f13b1 100644
--- a/interpreter/syntax/types.ml
+++ b/interpreter/syntax/types.ml
@@ -2,7 +2,7 @@
 
 type num_type = I32Type | I64Type | F32Type | F64Type
 type ref_type = NullRefType | AnyRefType | FuncRefType
-type value_type = NumType of num_type | RefType of ref_type
+type value_type = NumType of num_type | RefType of ref_type | BotType
 type stack_type = value_type list
 type func_type = FuncType of stack_type * stack_type
 
@@ -40,6 +40,7 @@ let match_value_type t1 t2 =
   match t1, t2 with
   | NumType t1', NumType t2' -> match_num_type t1' t2'
   | RefType t1', RefType t2' -> match_ref_type t1' t2'
+  | BotType, _ -> true
   | _, _ -> false
 
 let match_limits lim1 lim2 =
@@ -70,49 +71,13 @@ let match_extern_type et1 et2 =
   | ExternGlobalType gt1, ExternGlobalType gt2 -> match_global_type gt1 gt2
   | _, _ -> false
 
+let is_num_type = function
+  | NumType _ | BotType -> true
+  | RefType _ -> false
 
-(* Meet and join *)
-
-let join_num_type t1 t2 =
-  if t1 = t2 then Some t1 else None
-
-let join_ref_type t1 t2 =
-  match t1, t2 with
-  | AnyRefType, _ | _, NullRefType -> Some t1
-  | _, AnyRefType | NullRefType, _ -> Some t2
-  | _, _ when t1 = t2 -> Some t1
-  | _, _ -> Some AnyRefType
-
-let join_value_type t1 t2 =
-  match t1, t2 with
-  | NumType t1', NumType t2' ->
-    Lib.Option.map (fun t' -> NumType t') (join_num_type t1' t2')
-  | RefType t1', RefType t2' ->
-    Lib.Option.map (fun t' -> RefType t') (join_ref_type t1' t2')
-  | _, _ -> None
-
-
-let meet_num_type t1 t2 =
-  if t1 = t2 then Some t1 else None
-
-let meet_ref_type t1 t2 =
-  match t1, t2 with
-  | _, AnyRefType | NullRefType, _ -> Some t1
-  | AnyRefType, _ | _, NullRefType -> Some t2
-  | _, _ when t1 = t2 -> Some t1
-  | _, _ -> Some NullRefType
-
-let meet_value_type t1 t2 =
-  match t1, t2 with
-  | NumType t1', NumType t2' ->
-    Lib.Option.map (fun t' -> NumType t') (meet_num_type t1' t2')
-  | RefType t1', RefType t2' ->
-    Lib.Option.map (fun t' -> RefType t') (meet_ref_type t1' t2')
-  | _, _ -> None
-
-let meet_stack_type ts1 ts2 =
-  try Some (List.map Lib.Option.force (List.map2 meet_value_type ts1 ts2))
-  with Invalid_argument _ -> None
+let is_ref_type = function
+  | NumType _ -> false
+  | RefType _ | BotType -> true
 
 
 (* Filters *)
@@ -143,6 +108,7 @@ let string_of_ref_type = function
 let string_of_value_type = function
   | NumType t -> string_of_num_type t
   | RefType t -> string_of_ref_type t
+  | BotType -> "impossible"
 
 let string_of_value_types = function
   | [t] -> string_of_value_type t
diff --git a/interpreter/syntax/values.ml b/interpreter/syntax/values.ml
index de22eb36..cf5c6cb8 100644
--- a/interpreter/syntax/values.ml
+++ b/interpreter/syntax/values.ml
@@ -44,6 +44,7 @@ let default_ref = function
 let default_value = function
   | NumType t' -> Num (default_num t')
   | RefType t' -> Ref (default_ref t')
+  | BotType -> assert false
 
 
 (* Conversion *)
diff --git a/interpreter/text/arrange.ml b/interpreter/text/arrange.ml
index e2b7adae..c4bb3645 100644
--- a/interpreter/text/arrange.ml
+++ b/interpreter/text/arrange.ml
@@ -224,7 +224,9 @@ let rec instr e =
     | Unreachable -> "unreachable", []
     | Nop -> "nop", []
     | Drop -> "drop", []
-    | Select -> "select", []
+    | Select None -> "select", []
+    | Select (Some []) -> "select", [Node ("result", [])]
+    | Select (Some ts) -> "select", decls "result" ts
     | Block (ts, es) -> "block", stack_type ts @ list instr es
     | Loop (ts, es) -> "loop", stack_type ts @ list instr es
     | If (ts, es1, es2) ->
diff --git a/interpreter/text/parser.mly b/interpreter/text/parser.mly
index 576e0dd1..6bad0891 100644
--- a/interpreter/text/parser.mly
+++ b/interpreter/text/parser.mly
@@ -305,6 +305,7 @@ align_opt :
 
 instr :
   | plain_instr { let at = at () in fun c -> [$1 c @@ at] }
+  | select_instr_instr { fun c -> let e, es = $1 c in e :: es }
   | call_instr_instr { fun c -> let e, es = $1 c in e :: es }
   | block_instr { let at = at () in fun c -> [$1 c @@ at] }
   | expr { $1 } /* Sugar */
@@ -313,7 +314,6 @@ plain_instr :
   | UNREACHABLE { fun c -> unreachable }
   | NOP { fun c -> nop }
   | DROP { fun c -> drop }
-  | SELECT { fun c -> select }
   | BR var { fun c -> br ($2 c label) }
   | BR_IF var { fun c -> br_if ($2 c label) }
   | BR_TABLE var var_list
@@ -346,12 +346,35 @@ plain_instr :
   | CONVERT { fun c -> $1 }
 
 
+select_instr :
+  | SELECT select_instr_results
+    { let at = at () in fun c -> let b, ts = $2 in
+      select (if b then (Some ts) else None) @@ at }
+
+select_instr_results :
+  | LPAR RESULT value_type_list RPAR select_instr_results
+    { let _, ts = $5 in true, $3 @ ts }
+  | /* empty */
+    { false, [] }
+
+select_instr_instr :
+  | SELECT select_instr_results_instr
+    { let at1 = ati 1 in
+      fun c -> let b, ts, es = $2 c in
+      select (if b then (Some ts) else None) @@ at1, es }
+
+select_instr_results_instr :
+  | LPAR RESULT value_type_list RPAR select_instr_results_instr
+    { fun c -> let _, ts, es = $5 c in true, $3 @ ts, es }
+  | instr
+    { fun c -> false, [], $1 c }
+
+
 call_instr :
   | CALL_INDIRECT var call_instr_type
-    { let at1 = ati 1 in fun c -> call_indirect ($2 c table) ($3 c) @@ at1 }
+    { let at = at () in fun c -> call_indirect ($2 c table) ($3 c) @@ at }
   | CALL_INDIRECT call_instr_type  /* Sugar */
-    { let at1 = ati 1 in
-      fun c -> call_indirect (0l @@ at1) ($2 c) @@ at1 }
+    { let at = at () in fun c -> call_indirect (0l @@ at) ($2 c) @@ at }
 
 call_instr_type :
   | type_use call_instr_params
@@ -434,6 +457,8 @@ expr :  /* Sugar */
 
 expr1 :  /* Sugar */
   | plain_instr expr_list { fun c -> $2 c, $1 c }
+  | SELECT select_expr_results
+    { fun c -> let b, ts, es = $2 c in es, select (if b then (Some ts) else None) }
   | CALL_INDIRECT var call_expr_type
     { fun c -> let x, es = $3 c in es, call_indirect ($2 c table) x }
   | CALL_INDIRECT call_expr_type  /* Sugar */
@@ -447,6 +472,12 @@ expr1 :  /* Sugar */
     { fun c -> let c' = $2 c [] in
       let ts, (es, es1, es2) = $3 c c' in es, if_ ts es1 es2 }
 
+select_expr_results :
+  | LPAR RESULT value_type_list RPAR select_expr_results
+    { fun c -> let _, ts, es = $5 c in true, $3 @ ts, es }
+  | expr_list
+    { fun c -> false, [], $1 c }
+
 call_expr_type :
   | type_use call_expr_params
     { let at1 = ati 1 in
@@ -487,6 +518,7 @@ if_ :
 
 instr_list :
   | /* empty */ { fun c -> [] }
+  | select_instr { fun c -> [$1 c] }
   | call_instr { fun c -> [$1 c] }
   | instr instr_list { fun c -> $1 c @ $2 c }
 
diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml
index 5946f689..bb8f7bea 100644
--- a/interpreter/valid/valid.ml
+++ b/interpreter/valid/valid.ml
@@ -55,49 +55,25 @@ let label (c : context) x = lookup "label" c.labels x
  *)
 
 type ellipses = NoEllipses | Ellipses
-type infer_stack_type = ellipses * value_type option list
+type infer_stack_type = ellipses * value_type list
 type op_type = {ins : infer_stack_type; outs : infer_stack_type}
 
-let known = List.map (fun t -> Some t)
-let stack ts = (NoEllipses, known ts)
-let (-~>) ts1 ts2 = {ins = NoEllipses, ts1; outs = NoEllipses, ts2}
-let (-->) ts1 ts2 = {ins = NoEllipses, known ts1; outs = NoEllipses, known ts2}
-let (-->...) ts1 ts2 = {ins = Ellipses, known ts1; outs = Ellipses, known ts2}
-
-let string_of_infer_type t =
-  Lib.Option.get (Lib.Option.map string_of_value_type t) "_"
-let string_of_infer_types ts =
-  "[" ^ String.concat " " (List.map string_of_infer_type ts) ^ "]"
-
-let match_type t1 t2 =
-  match t1, t2 with
-  | Some t1, Some t2 -> match_value_type t1 t2
-  | _, _ -> true
-
-let join_type t1 t2 at =
-  match t1, t2 with
-  | _, None -> t1
-  | None, _ -> t2
-  | Some t1', Some t2' ->
-    let t = join_value_type t1' t2' in
-    require (t <> None) at
-      ("type mismatch: operator requires common supertype for " ^
-       string_of_infer_type t1 ^ " and " ^ string_of_infer_type t2 ^
-       " but none exists");
-    t
+let stack ts = (NoEllipses, ts)
+let (-->) ts1 ts2 = {ins = NoEllipses, ts1; outs = NoEllipses, ts2}
+let (-->...) ts1 ts2 = {ins = Ellipses, ts1; outs = Ellipses, ts2}
 
 let check_stack ts1 ts2 at =
   require
-    (List.length ts1 = List.length ts2 && List.for_all2 match_type ts1 ts2) at
-    ("type mismatch: operator requires " ^ string_of_infer_types ts2 ^
-     " but stack has " ^ string_of_infer_types ts1)
+    (List.length ts1 = List.length ts2 && List.for_all2 match_value_type ts1 ts2) at
+    ("type mismatch: operator requires " ^ string_of_stack_type ts2 ^
+     " but stack has " ^ string_of_stack_type ts1)
 
 let pop (ell1, ts1) (ell2, ts2) at =
   let n1 = List.length ts1 in
   let n2 = List.length ts2 in
   let n = min n1 n2 in
   let n3 = if ell2 = Ellipses then (n1 - n) else 0 in
-  check_stack (Lib.List.make n3 None @ Lib.List.drop (n2 - n) ts2) ts1 at;
+  check_stack (Lib.List.make n3 BotType @ Lib.List.drop (n2 - n) ts2) ts1 at;
   (ell2, if ell1 = Ellipses then [] else Lib.List.take (n2 - n) ts2)
 
 let push (ell1, ts1) (ell2, ts2) =
@@ -106,7 +82,7 @@ let push (ell1, ts1) (ell2, ts2) =
   ts2 @ ts1
 
 let peek i (ell, ts) =
-  try List.nth (List.rev ts) i with Failure _ -> None
+  try List.nth (List.rev ts) i with Failure _ -> BotType
 
 
 (* Type Synthesis *)
@@ -200,13 +176,19 @@ let rec check_instr (c : context) (e : instr) (s : infer_stack_type) : op_type =
     [] --> []
 
   | Drop ->
-    [peek 0 s] -~> []
+    [peek 0 s] --> []
 
-  | Select ->
-    let t1 = peek 2 s in
-    let t2 = peek 1 s in
-    let t = join_type t1 t2 e.at in
-    [t; t; Some (NumType I32Type)] -~> [t]
+  | Select None ->
+    let t = peek 1 s in
+    require (is_num_type t) e.at
+      ("type mismatch: instruction requires numeric type" ^
+       " but stack has " ^ string_of_value_type t);
+    [t; t; NumType I32Type] --> [t]
+
+  | Select (Some ts) ->
+    check_arity (List.length ts) e.at;
+    require (List.length ts <> 0) e.at "invalid result arity, 0 is not (yet) allowed";
+    (ts @ ts @ [NumType I32Type]) --> ts
 
   | Block (ts, es) ->
     check_arity (List.length ts) e.at;
@@ -231,18 +213,10 @@ let rec check_instr (c : context) (e : instr) (s : infer_stack_type) : op_type =
     (label c x @ [NumType I32Type]) --> label c x
 
   | BrTable (xs, x) ->
-    let ts =
-      List.fold_left (fun t1 t2 ->
-          let t = meet_stack_type t1 t2 in
-          require (t <> None) e.at
-            ("type mismatch: operator requires common subtype for " ^
-             string_of_stack_type t1 ^ " and " ^ string_of_stack_type t2 ^
-             " but none exists");
-          Lib.Option.force t)
-        (label c x) (List.map (label c) xs)
-    in
-    check_stack (known ts) (known (label c x)) x.at;
-    List.iter (fun x' -> check_stack (known ts) (known (label c x')) x'.at) xs;
+    let n = List.length (label c x) in
+    let ts = Lib.List.table n (fun i -> peek (i + 1) s) in
+    check_stack ts (label c x) x.at;
+    List.iter (fun x' -> check_stack ts (label c x') x'.at) xs;
     (ts @ [NumType I32Type]) -->... []
 
   | Return ->
@@ -256,8 +230,8 @@ let rec check_instr (c : context) (e : instr) (s : infer_stack_type) : op_type =
     let TableType (lim, t) = table c x in
     let FuncType (ins, out) = type_ c y in
     require (match_ref_type t FuncRefType) x.at
-      ("type mismatch: operator requires table of functions, " ^ 
-       "but table has " ^ string_of_ref_type t);
+      ("type mismatch: instruction requires table of functions" ^
+       " but table has " ^ string_of_ref_type t);
     (ins @ [NumType I32Type]) --> out
 
   | LocalGet x ->
@@ -364,7 +338,7 @@ and check_block (c : context) (es : instr list) (ts : stack_type) at =
   let s' = pop (stack ts) s at in
   require (snd s' = []) at
     ("type mismatch: operator requires " ^ string_of_stack_type ts ^
-     " but stack has " ^ string_of_infer_types (snd s))
+     " but stack has " ^ string_of_stack_type (snd s))
 
 
 (* Types *)
@@ -388,6 +362,7 @@ let check_value_type (t : value_type) at =
   match t with
   | NumType t' -> check_num_type t' at
   | RefType t' -> check_ref_type t' at
+  | BotType -> ()
 
 let check_func_type (ft : func_type) at =
   let FuncType (ins, out) = ft in
diff --git a/test/core/br_table.wast b/test/core/br_table.wast
index f5a15344..11b51a71 100644
--- a/test/core/br_table.wast
+++ b/test/core/br_table.wast
@@ -1251,13 +1251,49 @@
     )
   )
 
-  (func (export "meet-funcref") (param i32) (result anyref)
+  (func (export "meet-funcref-1") (param i32) (result anyref)
+    (block $l1 (result anyref)
+      (block $l2 (result funcref)
+        (br_table $l1 $l1 $l2 (table.get 0 (i32.const 0)) (local.get 0))
+      )
+    )
+  )
+
+  (func (export "meet-funcref-2") (param i32) (result anyref)
+    (block $l1 (result anyref)
+      (block $l2 (result funcref)
+        (br_table $l2 $l2 $l1 (table.get 0 (i32.const 0)) (local.get 0))
+      )
+    )
+  )
+
+  (func (export "meet-funcref-3") (param i32) (result anyref)
     (block $l1 (result anyref)
       (block $l2 (result funcref)
         (br_table $l2 $l1 $l2 (table.get 0 (i32.const 0)) (local.get 0))
       )
     )
   )
+
+  (func (export "meet-funcref-4") (param i32) (result anyref)
+    (block $l1 (result anyref)
+      (block $l2 (result funcref)
+        (br_table $l1 $l2 $l1 (table.get 0 (i32.const 0)) (local.get 0))
+      )
+    )
+  )
+
+  (func (export "meet-bottom")
+    (block (result f64)
+      (block (result f32)
+        (unreachable)
+        (br_table 0 1 1 (i32.const 1))
+      )
+      (drop)
+      (f64.const 0)
+    )
+    (drop)
+  )
 )
 
 (assert_return (invoke "type-i32"))
@@ -1445,9 +1481,18 @@
 (assert_return (invoke "meet-anyref" (i32.const 1) (ref.host 1)) (ref.host 1))
 (assert_return (invoke "meet-anyref" (i32.const 2) (ref.host 1)) (ref.host 1))
 
-(assert_return_func (invoke "meet-funcref" (i32.const 0)))
-(assert_return_func (invoke "meet-funcref" (i32.const 1)))
-(assert_return_func (invoke "meet-funcref" (i32.const 2)))
+(assert_return_func (invoke "meet-funcref-1" (i32.const 0)))
+(assert_return_func (invoke "meet-funcref-1" (i32.const 1)))
+(assert_return_func (invoke "meet-funcref-1" (i32.const 2)))
+(assert_return_func (invoke "meet-funcref-2" (i32.const 0)))
+(assert_return_func (invoke "meet-funcref-2" (i32.const 1)))
+(assert_return_func (invoke "meet-funcref-2" (i32.const 2)))
+(assert_return_func (invoke "meet-funcref-3" (i32.const 0)))
+(assert_return_func (invoke "meet-funcref-3" (i32.const 1)))
+(assert_return_func (invoke "meet-funcref-3" (i32.const 2)))
+(assert_return_func (invoke "meet-funcref-4" (i32.const 0)))
+(assert_return_func (invoke "meet-funcref-4" (i32.const 1)))
+(assert_return_func (invoke "meet-funcref-4" (i32.const 2)))
 
 (assert_invalid
   (module (func $type-arg-void-vs-num (result i32)
diff --git a/test/core/select.wast b/test/core/select.wast
index 7be0b923..33b7f624 100644
--- a/test/core/select.wast
+++ b/test/core/select.wast
@@ -4,27 +4,62 @@
   (table $tab funcref (elem $dummy))
   (memory 1)
 
-  (func (export "select_i32") (param $lhs i32) (param $rhs i32) (param $cond i32) (result i32)
-   (select (local.get $lhs) (local.get $rhs) (local.get $cond)))
-
-  (func (export "select_i64") (param $lhs i64) (param $rhs i64) (param $cond i32) (result i64)
-   (select (local.get $lhs) (local.get $rhs) (local.get $cond)))
+  (func (export "select-i32") (param i32 i32 i32) (result i32)
+    (select (local.get 0) (local.get 1) (local.get 2))
+  )
+  (func (export "select-i64") (param i64 i64 i32) (result i64)
+    (select (local.get 0) (local.get 1) (local.get 2))
+  )
+  (func (export "select-f32") (param f32 f32 i32) (result f32)
+    (select (local.get 0) (local.get 1) (local.get 2))
+  )
+  (func (export "select-f64") (param f64 f64 i32) (result f64)
+    (select (local.get 0) (local.get 1) (local.get 2))
+  )
 
-  (func (export "select_f32") (param $lhs f32) (param $rhs f32) (param $cond i32) (result f32)
-   (select (local.get $lhs) (local.get $rhs) (local.get $cond)))
+  (func (export "select-i32-t") (param i32 i32 i32) (result i32)
+    (select (result i32) (local.get 0) (local.get 1) (local.get 2))
+  )
+  (func (export "select-i64-t") (param i64 i64 i32) (result i64)
+    (select (result i64) (local.get 0) (local.get 1) (local.get 2))
+  )
+  (func (export "select-f32-t") (param f32 f32 i32) (result f32)
+    (select (result f32) (local.get 0) (local.get 1) (local.get 2))
+  )
+  (func (export "select-f64-t") (param f64 f64 i32) (result f64)
+    (select (result f64) (local.get 0) (local.get 1) (local.get 2))
+  )
+  (func (export "select-anyref") (param anyref anyref i32) (result anyref)
+    (select (result anyref) (local.get 0) (local.get 1) (local.get 2))
+  )
 
-  (func (export "select_f64") (param $lhs f64) (param $rhs f64) (param $cond i32) (result f64)
-   (select (local.get $lhs) (local.get $rhs) (local.get $cond)))
+  (func (export "join-nullref") (param i32) (result anyref)
+    (select (result anyref) (ref.null) (ref.null) (local.get 0))
+  )
+  (func (export "join-funcref") (param i32) (result anyref)
+    (select (result anyref)
+      (table.get $tab (i32.const 0))
+      (ref.null)
+      (local.get 0)
+    )
+  )
+  (func (export "join-anyref") (param i32) (param anyref) (result anyref)
+    (select (result anyref)
+      (table.get $tab (i32.const 0))
+      (local.get 1)
+      (local.get 0)
+    )
+  )
 
   ;; Check that both sides of the select are evaluated
-  (func (export "select_trap_l") (param $cond i32) (result i32)
+  (func (export "select-trap-left") (param $cond i32) (result i32)
     (select (unreachable) (i32.const 0) (local.get $cond))
   )
-  (func (export "select_trap_r") (param $cond i32) (result i32)
+  (func (export "select-trap-right") (param $cond i32) (result i32)
     (select (i32.const 0) (unreachable) (local.get $cond))
   )
 
-  (func (export "select_unreached")
+  (func (export "select-unreached")
     (unreachable) (select)
     (unreachable) (i32.const 0) (select)
     (unreachable) (i32.const 0) (i32.const 0) (select)
@@ -33,19 +68,6 @@
   )
 
 
-  (func (export "join-nullref") (param i32) (result anyref)
-    (select (ref.null) (ref.null) (local.get 0))
-  )
-
-  (func (export "join-funcref") (param i32) (result anyref)
-    (select (table.get $tab (i32.const 0)) (ref.null) (local.get 0))
-  )
-
-  (func (export "join-anyref") (param i32) (param anyref) (result anyref)
-    (select (table.get $tab (i32.const 0)) (local.get 1) (local.get 0))
-  )
-
-
   ;; As the argument of control constructs and instructions
 
   (func (export "as-select-first") (param i32) (result i32)
@@ -190,33 +212,64 @@
   )
 )
 
-(assert_return (invoke "select_i32" (i32.const 1) (i32.const 2) (i32.const 1)) (i32.const 1))
-(assert_return (invoke "select_i64" (i64.const 2) (i64.const 1) (i32.const 1)) (i64.const 2))
-(assert_return (invoke "select_f32" (f32.const 1) (f32.const 2) (i32.const 1)) (f32.const 1))
-(assert_return (invoke "select_f64" (f64.const 1) (f64.const 2) (i32.const 1)) (f64.const 1))
-
-(assert_return (invoke "select_i32" (i32.const 1) (i32.const 2) (i32.const 0)) (i32.const 2))
-(assert_return (invoke "select_i32" (i32.const 2) (i32.const 1) (i32.const 0)) (i32.const 1))
-(assert_return (invoke "select_i64" (i64.const 2) (i64.const 1) (i32.const -1)) (i64.const 2))
-(assert_return (invoke "select_i64" (i64.const 2) (i64.const 1) (i32.const 0xf0f0f0f0)) (i64.const 2))
-
-(assert_return (invoke "select_f32" (f32.const nan) (f32.const 1) (i32.const 1)) (f32.const nan))
-(assert_return (invoke "select_f32" (f32.const nan:0x20304) (f32.const 1) (i32.const 1)) (f32.const nan:0x20304))
-(assert_return (invoke "select_f32" (f32.const nan) (f32.const 1) (i32.const 0)) (f32.const 1))
-(assert_return (invoke "select_f32" (f32.const nan:0x20304) (f32.const 1) (i32.const 0)) (f32.const 1))
-(assert_return (invoke "select_f32" (f32.const 2) (f32.const nan) (i32.const 1)) (f32.const 2))
-(assert_return (invoke "select_f32" (f32.const 2) (f32.const nan:0x20304) (i32.const 1)) (f32.const 2))
-(assert_return (invoke "select_f32" (f32.const 2) (f32.const nan) (i32.const 0)) (f32.const nan))
-(assert_return (invoke "select_f32" (f32.const 2) (f32.const nan:0x20304) (i32.const 0)) (f32.const nan:0x20304))
-
-(assert_return (invoke "select_f64" (f64.const nan) (f64.const 1) (i32.const 1)) (f64.const nan))
-(assert_return (invoke "select_f64" (f64.const nan:0x20304) (f64.const 1) (i32.const 1)) (f64.const nan:0x20304))
-(assert_return (invoke "select_f64" (f64.const nan) (f64.const 1) (i32.const 0)) (f64.const 1))
-(assert_return (invoke "select_f64" (f64.const nan:0x20304) (f64.const 1) (i32.const 0)) (f64.const 1))
-(assert_return (invoke "select_f64" (f64.const 2) (f64.const nan) (i32.const 1)) (f64.const 2))
-(assert_return (invoke "select_f64" (f64.const 2) (f64.const nan:0x20304) (i32.const 1)) (f64.const 2))
-(assert_return (invoke "select_f64" (f64.const 2) (f64.const nan) (i32.const 0)) (f64.const nan))
-(assert_return (invoke "select_f64" (f64.const 2) (f64.const nan:0x20304) (i32.const 0)) (f64.const nan:0x20304))
+(assert_return (invoke "select-i32" (i32.const 1) (i32.const 2) (i32.const 1)) (i32.const 1))
+(assert_return (invoke "select-i64" (i64.const 2) (i64.const 1) (i32.const 1)) (i64.const 2))
+(assert_return (invoke "select-f32" (f32.const 1) (f32.const 2) (i32.const 1)) (f32.const 1))
+(assert_return (invoke "select-f64" (f64.const 1) (f64.const 2) (i32.const 1)) (f64.const 1))
+
+(assert_return (invoke "select-i32" (i32.const 1) (i32.const 2) (i32.const 0)) (i32.const 2))
+(assert_return (invoke "select-i32" (i32.const 2) (i32.const 1) (i32.const 0)) (i32.const 1))
+(assert_return (invoke "select-i64" (i64.const 2) (i64.const 1) (i32.const -1)) (i64.const 2))
+(assert_return (invoke "select-i64" (i64.const 2) (i64.const 1) (i32.const 0xf0f0f0f0)) (i64.const 2))
+
+(assert_return (invoke "select-f32" (f32.const nan) (f32.const 1) (i32.const 1)) (f32.const nan))
+(assert_return (invoke "select-f32" (f32.const nan:0x20304) (f32.const 1) (i32.const 1)) (f32.const nan:0x20304))
+(assert_return (invoke "select-f32" (f32.const nan) (f32.const 1) (i32.const 0)) (f32.const 1))
+(assert_return (invoke "select-f32" (f32.const nan:0x20304) (f32.const 1) (i32.const 0)) (f32.const 1))
+(assert_return (invoke "select-f32" (f32.const 2) (f32.const nan) (i32.const 1)) (f32.const 2))
+(assert_return (invoke "select-f32" (f32.const 2) (f32.const nan:0x20304) (i32.const 1)) (f32.const 2))
+(assert_return (invoke "select-f32" (f32.const 2) (f32.const nan) (i32.const 0)) (f32.const nan))
+(assert_return (invoke "select-f32" (f32.const 2) (f32.const nan:0x20304) (i32.const 0)) (f32.const nan:0x20304))
+
+(assert_return (invoke "select-f64" (f64.const nan) (f64.const 1) (i32.const 1)) (f64.const nan))
+(assert_return (invoke "select-f64" (f64.const nan:0x20304) (f64.const 1) (i32.const 1)) (f64.const nan:0x20304))
+(assert_return (invoke "select-f64" (f64.const nan) (f64.const 1) (i32.const 0)) (f64.const 1))
+(assert_return (invoke "select-f64" (f64.const nan:0x20304) (f64.const 1) (i32.const 0)) (f64.const 1))
+(assert_return (invoke "select-f64" (f64.const 2) (f64.const nan) (i32.const 1)) (f64.const 2))
+(assert_return (invoke "select-f64" (f64.const 2) (f64.const nan:0x20304) (i32.const 1)) (f64.const 2))
+(assert_return (invoke "select-f64" (f64.const 2) (f64.const nan) (i32.const 0)) (f64.const nan))
+(assert_return (invoke "select-f64" (f64.const 2) (f64.const nan:0x20304) (i32.const 0)) (f64.const nan:0x20304))
+
+(assert_return (invoke "select-i32-t" (i32.const 1) (i32.const 2) (i32.const 1)) (i32.const 1))
+(assert_return (invoke "select-i64-t" (i64.const 2) (i64.const 1) (i32.const 1)) (i64.const 2))
+(assert_return (invoke "select-f32-t" (f32.const 1) (f32.const 2) (i32.const 1)) (f32.const 1))
+(assert_return (invoke "select-f64-t" (f64.const 1) (f64.const 2) (i32.const 1)) (f64.const 1))
+(assert_return (invoke "select-anyref" (ref.host 1) (ref.host 2) (i32.const 1)) (ref.host 1))
+
+(assert_return (invoke "select-i32-t" (i32.const 1) (i32.const 2) (i32.const 0)) (i32.const 2))
+(assert_return (invoke "select-i32-t" (i32.const 2) (i32.const 1) (i32.const 0)) (i32.const 1))
+(assert_return (invoke "select-i64-t" (i64.const 2) (i64.const 1) (i32.const -1)) (i64.const 2))
+(assert_return (invoke "select-i64-t" (i64.const 2) (i64.const 1) (i32.const 0xf0f0f0f0)) (i64.const 2))
+(assert_return (invoke "select-anyref" (ref.host 1) (ref.host 2) (i32.const 0)) (ref.host 2))
+(assert_return (invoke "select-anyref" (ref.host 2) (ref.host 1) (i32.const 0)) (ref.host 1))
+
+(assert_return (invoke "select-f32-t" (f32.const nan) (f32.const 1) (i32.const 1)) (f32.const nan))
+(assert_return (invoke "select-f32-t" (f32.const nan:0x20304) (f32.const 1) (i32.const 1)) (f32.const nan:0x20304))
+(assert_return (invoke "select-f32-t" (f32.const nan) (f32.const 1) (i32.const 0)) (f32.const 1))
+(assert_return (invoke "select-f32-t" (f32.const nan:0x20304) (f32.const 1) (i32.const 0)) (f32.const 1))
+(assert_return (invoke "select-f32-t" (f32.const 2) (f32.const nan) (i32.const 1)) (f32.const 2))
+(assert_return (invoke "select-f32-t" (f32.const 2) (f32.const nan:0x20304) (i32.const 1)) (f32.const 2))
+(assert_return (invoke "select-f32-t" (f32.const 2) (f32.const nan) (i32.const 0)) (f32.const nan))
+(assert_return (invoke "select-f32-t" (f32.const 2) (f32.const nan:0x20304) (i32.const 0)) (f32.const nan:0x20304))
+
+(assert_return (invoke "select-f64-t" (f64.const nan) (f64.const 1) (i32.const 1)) (f64.const nan))
+(assert_return (invoke "select-f64-t" (f64.const nan:0x20304) (f64.const 1) (i32.const 1)) (f64.const nan:0x20304))
+(assert_return (invoke "select-f64-t" (f64.const nan) (f64.const 1) (i32.const 0)) (f64.const 1))
+(assert_return (invoke "select-f64-t" (f64.const nan:0x20304) (f64.const 1) (i32.const 0)) (f64.const 1))
+(assert_return (invoke "select-f64-t" (f64.const 2) (f64.const nan) (i32.const 1)) (f64.const 2))
+(assert_return (invoke "select-f64-t" (f64.const 2) (f64.const nan:0x20304) (i32.const 1)) (f64.const 2))
+(assert_return (invoke "select-f64-t" (f64.const 2) (f64.const nan) (i32.const 0)) (f64.const nan))
+(assert_return (invoke "select-f64-t" (f64.const 2) (f64.const nan:0x20304) (i32.const 0)) (f64.const nan:0x20304))
 
 (assert_return (invoke "join-nullref" (i32.const 1)) (ref.null))
 (assert_return (invoke "join-nullref" (i32.const 0)) (ref.null))
@@ -227,10 +280,10 @@
 (assert_return_func (invoke "join-anyref" (i32.const 1) (ref.host 1)))
 (assert_return (invoke "join-anyref" (i32.const 0) (ref.host 1)) (ref.host 1))
 
-(assert_trap (invoke "select_trap_l" (i32.const 1)) "unreachable")
-(assert_trap (invoke "select_trap_l" (i32.const 0)) "unreachable")
-(assert_trap (invoke "select_trap_r" (i32.const 1)) "unreachable")
-(assert_trap (invoke "select_trap_r" (i32.const 0)) "unreachable")
+(assert_trap (invoke "select-trap-left" (i32.const 1)) "unreachable")
+(assert_trap (invoke "select-trap-left" (i32.const 0)) "unreachable")
+(assert_trap (invoke "select-trap-right" (i32.const 1)) "unreachable")
+(assert_trap (invoke "select-trap-right" (i32.const 0)) "unreachable")
 
 (assert_return (invoke "as-select-first" (i32.const 0)) (i32.const 1))
 (assert_return (invoke "as-select-first" (i32.const 1)) (i32.const 0))
@@ -309,22 +362,54 @@
 (assert_return (invoke "as-convert-operand" (i32.const 1)) (i32.const 1))
 
 (assert_invalid
-  (module (func $arity-0 (select (nop) (nop) (i32.const 1))))
+  (module (func $arity-0-implicit (select (nop) (nop) (i32.const 1))))
   "type mismatch"
 )
+(assert_invalid
+  (module (func $arity-0 (select (result) (nop) (nop) (i32.const 1))))
+  "invalid result arity"
+)
+(assert_invalid
+  (module (func $arity-2 (result i32 i32)
+    (select (result i32 i32)
+      (i32.const 0) (i32.const 0)
+      (i32.const 0) (i32.const 0)
+      (i32.const 1)
+    )
+  ))
+  "invalid result arity"
+)
 
-;; The first two operands should have the same type as each other
 
 (assert_invalid
-  (module (func $type-num-vs-num (select (i32.const 1) (i64.const 1) (i32.const 1))))
+  (module (func $type-nullref-implicit
+    (drop (select (ref.null) (ref.null) (i32.const 1)))
+  ))
+  "type mismatch"
+)
+(assert_invalid
+  (module (func $type-anyref-implicit (param $r anyref)
+    (drop (select (local.get $r) (local.get $r) (i32.const 1)))
+  ))
+  "type mismatch"
+)
+
+(assert_invalid
+  (module (func $type-num-vs-num
+    (drop (select (i32.const 1) (i64.const 1) (i32.const 1)))
+  ))
   "type mismatch"
 )
 (assert_invalid
-  (module (func $type-num-vs-num (select (i32.const 1) (f32.const 1.0) (i32.const 1))))
+  (module (func $type-num-vs-num
+    (drop (select (i32.const 1) (f32.const 1.0) (i32.const 1)))
+  ))
   "type mismatch"
 )
 (assert_invalid
-  (module (func $type-num-vs-num (select (i32.const 1) (f64.const 1.0) (i32.const 1))))
+  (module (func $type-num-vs-num
+    (drop (select (i32.const 1) (f64.const 1.0) (i32.const 1)))
+  ))
   "type mismatch"
 )
 
diff --git a/test/core/unreached-invalid.wast b/test/core/unreached-invalid.wast
index 6ef4ac55..3ddd7738 100644
--- a/test/core/unreached-invalid.wast
+++ b/test/core/unreached-invalid.wast
@@ -535,20 +535,6 @@
   ))
   "type mismatch"
 )
-(assert_invalid
-  (module (func $type-br_table-label-num-vs-label-num-after-unreachable
-    (block (result f64)
-      (block (result f32)
-        (unreachable)
-        (br_table 0 1 1 (i32.const 1))
-      )
-      (drop)
-      (f64.const 0)
-    )
-    (drop)
-  ))
-  "type mismatch"
-)
 
 (assert_invalid
   (module (func $type-block-value-nested-unreachable-num-vs-void