diff --git a/interpreter/binary/decode.ml b/interpreter/binary/decode.ml
index 61e94212cf..a1aca2ba8a 100644
--- a/interpreter/binary/decode.ml
+++ b/interpreter/binary/decode.ml
@@ -58,6 +58,12 @@ let at f s =
 
 
 
+(* FIXME add support for abstract types *)
+let fixme_w vt = Types.RawValueType vt
+let fixme_wl = List.map fixme_w
+
+
+
 (* Generic values *)
 
 let u8 s =
@@ -163,7 +169,7 @@ let func_type s =
   | -0x20 ->
     let ins = vec value_type s in
     let out = vec value_type s in
-    FuncType (ins, out)
+    FuncType (fixme_wl ins, fixme_wl out)
   | _ -> error s (pos s - 1) "invalid function type"
 
 let limits vu s =
diff --git a/interpreter/binary/encode.ml b/interpreter/binary/encode.ml
index 6910cf4256..4c85577881 100644
--- a/interpreter/binary/encode.ml
+++ b/interpreter/binary/encode.ml
@@ -9,6 +9,20 @@ module Code = Error.Make ()
 exception Code = Code.Error
 
 
+(* Abstract Types *)
+let raise_no_abstypes () = 
+  Code.error Source.no_region
+    "encoding abstract types is not supported (yet)"
+
+let fixme_uw wty =
+  let open Types in
+  match wty with
+  | RawValueType vt -> vt
+  | NewAbsType _ -> raise_no_abstypes ()
+
+let fixme_uwl = List.map fixme_uw
+
+
 (* Encoding stream *)
 
 type stream =
@@ -104,6 +118,8 @@ let encode m =
     let value_type = function
       | NumType t -> num_type t
       | RefType t -> ref_type t
+      (* FIXME add abstract type support *)
+      | SealedAbsType i -> raise_no_abstypes ()
       | BotType -> assert false
 
     let stack_type = function
@@ -115,7 +131,8 @@ let encode m =
 
     let func_type = function
       | FuncType (ins, out) ->
-        vs7 (-0x20); vec value_type ins; vec value_type out
+        (* FIXME add abstract type support *)
+        vs7 (-0x20); vec value_type (fixme_uwl ins); vec value_type (fixme_uwl out)
 
     let limits vu {min; max} =
       bool (max <> None); vu min; opt vu max
@@ -412,6 +429,7 @@ let encode m =
     (* Import section *)
     let import_desc d =
       match d.it with
+      | AbsTypeImport _ -> raise_no_abstypes ()
       | FuncImport x -> u8 0x00; var x
       | TableImport t -> u8 0x01; table_type t
       | MemoryImport t -> u8 0x02; memory_type t
@@ -457,6 +475,7 @@ let encode m =
     (* Export section *)
     let export_desc d =
       match d.it with
+      | AbsTypeExport _ -> raise_no_abstypes ()
       | FuncExport x -> u8 0; var x
       | TableExport x -> u8 1; var x
       | MemoryExport x -> u8 2; var x
diff --git a/interpreter/exec/eval.ml b/interpreter/exec/eval.ml
index 5880285015..3f5fef5781 100644
--- a/interpreter/exec/eval.ml
+++ b/interpreter/exec/eval.ml
@@ -1,6 +1,7 @@
 open Values
 open Types
 open Instance
+open Extern_types
 open Ast
 open Source
 
@@ -182,7 +183,9 @@ let rec step (c : config) : config =
 
       | CallIndirect (x, y), Num (I32 i) :: vs ->
         let func = func_ref frame.inst x i e.at in
-        if type_ frame.inst y <> Func.type_of func then
+        let func_ety = extern_type_of_func func in
+        let expected_ety = resolve_extern_func_type (ModuleInst frame.inst) (type_ frame.inst y) in
+        if not (match_resolved_func_type func_ety expected_ety) then
           vs, [Trapping "indirect call type mismatch" @@ e.at]
         else
           vs, [Invoke func @@ e.at]
@@ -504,7 +507,7 @@ let rec step (c : config) : config =
       (match func with
       | Func.AstFunc (t, inst', f) ->
         let locals' = List.rev args @ List.map default_value f.it.locals in
-        let code' = [], [Plain (Block (out, f.it.body)) @@ f.at] in
+        let code' = [], [Plain (Block (unwrap_stack out, f.it.body)) @@ f.at] in
         let frame' = {inst = !inst'; locals = List.map ref locals'} in
         vs', [Frame (List.length out, frame', code') @@ e.at]
 
@@ -534,7 +537,7 @@ let invoke (func : func_inst) (vs : value list) : value list =
   let FuncType (ins, out) = Func.type_of func in
   if List.length vs <> List.length ins then
     Crash.error at "wrong number of arguments";
-  if not (List.for_all2 (fun v -> match_value_type (type_of_value v)) vs ins) then
+  if not (List.for_all2 (fun v i -> match_value_type (type_of_value v) (unwrap i)) vs ins) then
     Crash.error at "wrong types of arguments";
   let c = config empty_module_inst (List.rev vs) [Invoke func @@ at] in
   try List.rev (eval c) with Stack_overflow ->
@@ -569,6 +572,7 @@ let create_export (inst : module_inst) (ex : export) : export_inst =
   let {name; edesc} = ex.it in
   let ext =
     match edesc.it with
+    | AbsTypeExport x -> ExternAbsTypeInst (inst.uid, x.it)
     | FuncExport x -> ExternFunc (func inst x)
     | TableExport x -> ExternTable (table inst x)
     | MemoryExport x -> ExternMemory (memory inst x)
@@ -583,12 +587,23 @@ let create_data (inst : module_inst) (seg : data_segment) : data_inst =
   let {dinit; _} = seg.it in
   ref dinit
 
-
-let add_import (m : module_) (ext : extern) (im : import) (inst : module_inst)
-  : module_inst =
-  if not (match_extern_type (extern_type_of ext) (import_type m im)) then
+let add_import (ext : extern) (im : import) (inst : module_inst) : module_inst =
+  let types_match =
+    match (extern_type_of ext), im.it.idesc.it with
+    | ExternAbsType ate, AbsTypeImport x -> true (* abstype matches are based purely on reference *)
+    | ExternFuncType rfte, FuncImport x ->
+      let fti = func_type_inst inst x in
+      let rfti = resolve_extern_func_type (ModuleInst inst) fti in
+      match_resolved_func_type rfte rfti
+    | ExternTableType tte, TableImport tti -> match_table_type tte tti
+    | ExternMemoryType mte, MemoryImport mti -> match_memory_type mte mti
+    | ExternGlobalType gte, GlobalImport gti -> match_global_type gte gti
+    | _, _ -> false
+  in
+  if not types_match then
     Link.error im.at "incompatible import type";
   match ext with
+  | ExternAbsTypeInst aty -> {inst with sealed_abstypes = aty :: inst.sealed_abstypes}
   | ExternFunc func -> {inst with funcs = func :: inst.funcs}
   | ExternTable tab -> {inst with tables = tab :: inst.tables}
   | ExternMemory mem -> {inst with memories = mem :: inst.memories}
@@ -638,26 +653,38 @@ let init (m : module_) (exts : extern list) : module_inst =
       exports; elems; datas; start
     } = m.it
   in
-  if List.length exts <> List.length imports then
-    Link.error m.at "wrong number of imports provided for initialisation";
   let inst0 =
-    { (List.fold_right2 (add_import m) exts imports empty_module_inst) with
+    { empty_module_inst with
       types = List.map (fun type_ -> type_.it) types }
   in
-  let fs = List.map (create_func inst0) funcs in
-  let inst1 = {inst0 with funcs = inst0.funcs @ fs} in
-  let inst2 =
-    { inst1 with
-      tables = inst1.tables @ List.map (create_table inst1) tables;
-      memories = inst1.memories @ List.map (create_memory inst1) memories;
-      globals = inst1.globals @ List.map (create_global inst1) globals;
+  if List.length exts <> List.length imports then
+    Link.error m.at "wrong number of imports provided for initialisation";
+  (* abstype imports must be resolved first *)
+  let imports, exts =
+    let abstypes_first = fun (im1, _) -> fun (im2, _) ->
+      match im1.it.idesc.it, im2.it.idesc.it with
+      | AbsTypeImport _, AbsTypeImport _ -> 0
+      | AbsTypeImport _, _ -> 1
+      | _ , AbsTypeImport _ -> -1
+      | _ -> 0
+    in
+    List.split (List.stable_sort abstypes_first (List.combine imports exts))
+  in
+  let inst1 = (List.fold_right2 add_import exts imports inst0) in
+  let fs = List.map (create_func inst1) funcs in
+  let inst2 = {inst1 with funcs = inst1.funcs @ fs} in
+  let inst3 =
+    { inst2 with
+      tables = inst2.tables @ List.map (create_table inst2) tables;
+      memories = inst2.memories @ List.map (create_memory inst2) memories;
+      globals = inst2.globals @ List.map (create_global inst2) globals;
     }
   in
   let inst =
-    { inst2 with
-      exports = List.map (create_export inst2) exports;
-      elems = List.map (create_elem inst2) elems;
-      datas = List.map (create_data inst2) datas;
+    { inst3 with
+      exports = List.map (create_export inst3) exports;
+      elems = List.map (create_elem inst3) elems;
+      datas = List.map (create_data inst3) datas;
     }
   in
   List.iter (init_func inst) fs;
diff --git a/interpreter/host/env.ml b/interpreter/host/env.ml
index 58239d10bc..5e925fd0eb 100644
--- a/interpreter/host/env.ml
+++ b/interpreter/host/env.ml
@@ -7,6 +7,7 @@
 open Values
 open Types
 open Instance
+open Extern_types
 
 
 let error msg = raise (Eval.Crash (Source.no_region, msg))
@@ -41,6 +42,8 @@ let exit vs =
 
 let lookup name t =
   match Utf8.encode name, t with
-  | "abort", ExternFuncType t -> ExternFunc (Func.alloc_host t abort)
-  | "exit", ExternFuncType t -> ExternFunc (Func.alloc_host t exit)
+  | "abort", ExternFuncType et ->
+    ExternFunc (Func.alloc_host (func_type_from_extern et) abort)
+  | "exit", ExternFuncType et ->
+    ExternFunc (Func.alloc_host (func_type_from_extern et) exit)
   | _ -> raise Not_found
diff --git a/interpreter/host/spectest.ml b/interpreter/host/spectest.ml
index a8d32aa55e..3925780337 100644
--- a/interpreter/host/spectest.ml
+++ b/interpreter/host/spectest.ml
@@ -15,6 +15,9 @@ 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
+    (* Start: Abstract Types *)
+    | SealedAbsType _ -> assert false
+    (* Start: Abstract Types *)
     | BotType -> assert false
   in Global.alloc gt v
 
@@ -31,19 +34,19 @@ let print_value v =
 let print (FuncType (_, out)) vs =
   List.iter print_value vs;
   flush_all ();
-  List.map default_value out
-
+  List.map (fun v -> default_value (unwrap v)) out
 
 let lookup name t =
+  let open Types_shorthand in
   match Utf8.encode name, t with
   | "print", _ -> ExternFunc (func print (FuncType ([], [])))
-  | "print_i32", _ -> ExternFunc (func print (FuncType ([NumType I32Type], [])))
+  | "print_i32", _ -> ExternFunc (func print (FuncType ([r (NumType I32Type)], [])))
   | "print_i32_f32", _ ->
-    ExternFunc (func print (FuncType ([NumType I32Type; NumType F32Type], [])))
+    ExternFunc (func print (FuncType ([r (NumType I32Type); r (NumType F32Type)], [])))
   | "print_f64_f64", _ ->
-    ExternFunc (func print (FuncType ([NumType F64Type; NumType F64Type], [])))
-  | "print_f32", _ -> ExternFunc (func print (FuncType ([NumType F32Type], [])))
-  | "print_f64", _ -> ExternFunc (func print (FuncType ([NumType F64Type], [])))
+    ExternFunc (func print (FuncType ([r (NumType F64Type); r (NumType F64Type)], [])))
+  | "print_f32", _ -> ExternFunc (func print (FuncType ([r (NumType F32Type)], [])))
+  | "print_f64", _ -> ExternFunc (func print (FuncType ([r (NumType F64Type)], [])))
   | "global_i32", _ -> ExternGlobal (global (GlobalType (NumType I32Type, Immutable)))
   | "global_f32", _ -> ExternGlobal (global (GlobalType (NumType F32Type, Immutable)))
   | "global_f64", _ -> ExternGlobal (global (GlobalType (NumType F64Type, Immutable)))
diff --git a/interpreter/main/main.ml b/interpreter/main/main.ml
index d7f2b44f37..91da56b07b 100644
--- a/interpreter/main/main.ml
+++ b/interpreter/main/main.ml
@@ -6,7 +6,7 @@ let configure () =
   Import.register (Utf8.decode "env") Env.lookup
 
 let banner () =
-  print_endline (name ^ " " ^ version ^ " reference interpreter")
+  print_endline (name ^ " " ^ version ^ " reference interpreter + abstract types")
 
 let usage = "Usage: " ^ name ^ " [option] [file ...]"
 
diff --git a/interpreter/runtime/extern_types.ml b/interpreter/runtime/extern_types.ml
new file mode 100644
index 0000000000..54d1072990
--- /dev/null
+++ b/interpreter/runtime/extern_types.ml
@@ -0,0 +1,250 @@
+open Types
+open Instance
+
+(* Fundamentally, abstract types are based on Module (or Host) instances,
+   not module definitions. The additional constructors (NameModuleRef, 
+   LocalModuleRef) exist to assist with representing abstract types
+   in contexts were modules haven't been instantiated yet, but these
+   representations of abstract types have to be resolved before they
+   can be properly compared. *)
+type unresolved_abstype_ref =
+  | NamedModuleAbsRef of Ast.name * Ast.name
+  | LocalModuleAbsRef of int32
+
+type resolved_abstype_ref =
+  | InstModuleAbsRef of sealed_abstype_inst
+(* FIXME host abstract types are not currently supported *)
+(* | HostModuleAbsRef *)
+
+type 'absref extern_value_type =
+  | ExternNumType of num_type
+  | ExternRefType of ref_type
+  | ExternSealedAbsType of 'absref
+  | ExternBotType
+
+type 'absref extern_stack_type = 'absref extern_value_type list
+
+type 'absref extern_func_type =
+  | ExternFuncSigType of
+      'absref extern_stack_type * 'absref extern_stack_type * func_type
+
+type resolved_extern_func_type = resolved_abstype_ref extern_func_type
+
+type 'absref extern_type =
+  | ExternAbsType of 'absref
+  | ExternFuncType of 'absref extern_func_type
+  | ExternTableType of table_type
+  | ExternMemoryType of memory_type
+  | ExternGlobalType of global_type
+
+type unresolved_extern_type = unresolved_abstype_ref extern_type
+type resolved_extern_type = resolved_abstype_ref extern_type
+
+
+(* Comparisons *)
+
+let match_resolved_value_type vt1 vt2 =
+  match vt1, vt2 with
+  | ExternNumType vt1', ExternNumType vt2' -> match_num_type vt1' vt2'
+  | ExternRefType vt1', ExternRefType vt2' -> match_ref_type vt1' vt2'
+  | ExternSealedAbsType vt1', ExternSealedAbsType vt2' ->
+    (match vt1', vt2' with
+    | InstModuleAbsRef (r1, i1), InstModuleAbsRef (r2, i2) -> r1 == r2 && i1 = i2
+    )
+  | ExternBotType, _ -> true
+  | _, _ -> false
+
+let match_resolved_stack_types st1 st2 =
+  List.length st1 = List.length st2 &&
+  List.for_all2 match_resolved_value_type st1 st2
+
+let match_resolved_func_type
+    (ft1 : resolved_extern_func_type)
+    (ft2 : resolved_extern_func_type) =
+  let ExternFuncSigType (ins1, out1, _) = ft1 in
+  let ExternFuncSigType (ins2, out2, _) = ft2 in
+  match_resolved_stack_types ins1 ins2 && match_resolved_stack_types out1 out2
+
+
+(* Type Conversions *)
+
+let func_type_from_extern = function ExternFuncSigType (_, _, ft) -> ft
+
+let extern_from_value_type handle_sealed_abstype vt =
+  match vt with
+  | NumType n -> ExternNumType n
+  | RefType r -> ExternRefType r
+  | SealedAbsType i -> ExternSealedAbsType (handle_sealed_abstype i)
+  | BotType -> ExternBotType
+
+let extern_from_wrapped_value_type handle_new_abstype handle_sealed_abstype vt =
+  match vt with
+  | RawValueType vt -> extern_from_value_type handle_sealed_abstype vt
+  | NewAbsType (vt, i) -> handle_new_abstype i
+
+let extern_from_func_type
+    (handle_new_abstype : int32 -> 'absref extern_value_type)
+    (handle_sealed_abstype : int32 -> 'absref)
+    (ft : func_type) =
+  let (FuncType (ins, outs)) = ft in
+  let externalize_vt =
+    extern_from_wrapped_value_type handle_new_abstype handle_sealed_abstype
+  in
+  let externalize l = List.map externalize_vt l in
+  ExternFuncSigType (externalize ins, externalize outs, ft)
+
+
+(* Type Conversions: Unresolved *)
+
+open Ast
+open Source
+
+let local_seal_new_abstype i = ExternSealedAbsType (LocalModuleAbsRef i)
+
+let imported_sealed_abstype (m : module_) i =
+  let sealed_abstypes =
+    Lib.List.map_filter
+      (fun im ->
+        match im.it.idesc.it with AbsTypeImport x -> Some im.it | _ -> None)
+      m.it.imports
+  in
+  let im = Lib.List32.nth sealed_abstypes i in
+  NamedModuleAbsRef (im.module_name, im.item_name)
+
+let local_extern_func_type (m : module_) =
+  extern_from_func_type local_seal_new_abstype (imported_sealed_abstype m)
+
+
+(* Type Conversions: Resolved *)
+
+let inst_seal_new_abstype hinst i =
+  match hinst with
+  | ModuleInst inst -> ExternSealedAbsType (InstModuleAbsRef (inst.uid, i))
+  | HostInst -> assert false
+
+let inst_resolve_sealed_abstype hinst i =
+  match hinst with
+  | ModuleInst inst -> InstModuleAbsRef (Lib.List32.nth inst.sealed_abstypes i)
+  | HostInst -> assert false
+
+let resolve_extern_func_type (hinst : host_module_inst) =
+  extern_from_func_type
+    (inst_seal_new_abstype hinst)
+    (inst_resolve_sealed_abstype hinst)
+
+open Func
+
+let extern_type_of_func = function
+  | AstFunc (ft, inst, _) -> resolve_extern_func_type (ModuleInst !inst) ft
+  | HostFunc (ft, _) -> resolve_extern_func_type HostInst ft
+
+let extern_type_of = function
+  | ExternAbsTypeInst sealed -> ExternAbsType (InstModuleAbsRef sealed)
+  | ExternFunc func -> ExternFuncType (extern_type_of_func func)
+  | ExternTable tab -> ExternTableType (Table.type_of tab)
+  | ExternMemory mem -> ExternMemoryType (Memory.type_of mem)
+  | ExternGlobal glob -> ExternGlobalType (Global.type_of glob)
+
+
+(* Filters *)
+
+let funcs =
+  Lib.List.map_filter (function ExternFuncType t -> Some t | _ -> None)
+let tables =
+  Lib.List.map_filter (function ExternTableType t -> Some t | _ -> None)
+let memories =
+  Lib.List.map_filter (function ExternMemoryType t -> Some t | _ -> None)
+let globals =
+  Lib.List.map_filter (function ExternGlobalType t -> Some t | _ -> None)
+
+
+(* Import/Export Conversions *)
+
+let func_type_module (m : module_) (x : var) : func_type =
+  (Lib.List32.nth m.it.types x.it).it
+
+let func_type_inst (m : module_inst) (x : var) : func_type =
+  Lib.List32.nth m.types x.it
+
+let sealed_abstype_for (inst : module_inst) (x : var) : sealed_abstype_inst =
+  Lib.List32.nth inst.sealed_abstypes x.it
+
+let unresolved_import_type (m : module_) (im : import) : unresolved_extern_type =
+  let {module_name; item_name; idesc; _} = im.it in
+  match idesc.it with
+  | AbsTypeImport x ->
+    ExternAbsType (NamedModuleAbsRef (module_name, item_name))
+  | FuncImport x -> ExternFuncType (local_extern_func_type m (func_type_module m x))
+  | TableImport t -> ExternTableType t
+  | MemoryImport t -> ExternMemoryType t
+  | GlobalImport t -> ExternGlobalType t
+
+let unresolved_export_type (m : module_) (ex : export) : unresolved_extern_type =
+  let {edesc; _} = ex.it in
+  let its = List.map (unresolved_import_type m) m.it.imports in
+  let open Lib.List32 in
+  match edesc.it with
+  | AbsTypeExport x -> ExternAbsType (LocalModuleAbsRef x.it)
+  | FuncExport x ->
+    let fts =
+      funcs its
+      @ List.map
+          (fun f -> local_extern_func_type m (func_type_module m f.it.ftype))
+          m.it.funcs
+    in
+    ExternFuncType (nth fts x.it)
+  | TableExport x ->
+    let tts = tables its @ List.map (fun t -> t.it.ttype) m.it.tables in
+    ExternTableType (nth tts x.it)
+  | MemoryExport x ->
+    let mts = memories its @ List.map (fun m -> m.it.mtype) m.it.memories in
+    ExternMemoryType (nth mts x.it)
+  | GlobalExport x ->
+    let gts = globals its @ List.map (fun g -> g.it.gtype) m.it.globals in
+    ExternGlobalType (nth gts x.it)
+
+
+(* Debugging *)
+
+let string_of_unresolved_abstype = function
+  | NamedModuleAbsRef (mname, iname) ->
+    "abs{'" ^ Ast.string_of_name iname ^ "','" ^ Ast.string_of_name mname ^ "'}"
+  | LocalModuleAbsRef i -> "abs{" ^ Int32.to_string i ^ "}"
+
+let string_of_resolved_abstype = function
+  | InstModuleAbsRef (ModuleInstUID uid, i) ->
+    "abs{" ^ Int32.to_string uid ^ "," ^ Int32.to_string i ^ "}"
+
+(* NOTE: these should behave similarly to string funcs in Types *)
+
+let string_of_extern_value_type strabs = function
+  | ExternNumType n -> string_of_num_type n
+  | ExternRefType r -> string_of_ref_type r
+  | ExternSealedAbsType a -> strabs a
+  | ExternBotType -> "impossible"
+
+let string_of_extern_stack_type strabs ts =
+  "[" ^ String.concat " " (List.map (string_of_extern_value_type strabs) ts) ^ "]"
+
+let string_of_extern_func_type
+    (strabs : 'absref -> string)
+    (ExternFuncSigType (ins, out, _)) =
+  let ins_str = string_of_extern_stack_type strabs ins in
+  let out_str = string_of_extern_stack_type strabs out in
+  ins_str ^ " -> " ^ out_str
+
+let annotation_of_extern_type
+    (strabs : 'absref -> string)
+    (et : 'absref extern_type) =
+  match et with
+  | ExternAbsType t -> ("abstype", strabs t)
+  | ExternFuncType t -> ("func", string_of_extern_func_type strabs t)
+  | ExternTableType t -> ("table", string_of_table_type t)
+  | ExternMemoryType t -> ("memory", string_of_memory_type t)
+  | ExternGlobalType t -> ("global", string_of_global_type t)
+
+let annotation_of_unresolved_extern_type =
+  annotation_of_extern_type string_of_unresolved_abstype
+
+let annotation_of_resolved_extern_type =
+  annotation_of_extern_type string_of_resolved_abstype
diff --git a/interpreter/runtime/instance.ml b/interpreter/runtime/instance.ml
index efc230e0f9..44971d082b 100644
--- a/interpreter/runtime/instance.ml
+++ b/interpreter/runtime/instance.ml
@@ -1,7 +1,18 @@
 open Types
 
+type module_inst_uid = ModuleInstUID of int32
+let lastID = ref 0l
+let issue_module_inst_uid () : module_inst_uid =
+  let newID = Int32.add !lastID 1l in
+  if newID < !lastID then assert false;
+  lastID := newID;
+  ModuleInstUID !lastID
+
 type module_inst =
 {
+  uid : module_inst_uid;
+  new_abstypes : value_type list;
+  sealed_abstypes : sealed_abstype_inst list;
   types : func_type list;
   funcs : func_inst list;
   tables : table_inst list;
@@ -12,6 +23,7 @@ type module_inst =
   datas : data_inst list;
 }
 
+and sealed_abstype_inst = module_inst_uid * int32
 and func_inst = module_inst ref Func.t
 and table_inst = Table.t
 and memory_inst = Memory.t
@@ -21,12 +33,18 @@ and elem_inst = Values.ref_ list ref
 and data_inst = string ref
 
 and extern =
+  | ExternAbsTypeInst of sealed_abstype_inst
   | ExternFunc of func_inst
   | ExternTable of table_inst
   | ExternMemory of memory_inst
   | ExternGlobal of global_inst
 
 
+type host_module_inst =
+  | HostInst
+  | ModuleInst of module_inst
+
+
 (* Reference types *)
 
 type Values.ref_ += FuncRef of func_inst
@@ -47,14 +65,10 @@ let () =
 (* Auxiliary functions *)
 
 let empty_module_inst =
-  { types = []; funcs = []; tables = []; memories = []; globals = [];
-    exports = []; elems = []; datas = [] }
-
-let extern_type_of = function
-  | ExternFunc func -> ExternFuncType (Func.type_of func)
-  | ExternTable tab -> ExternTableType (Table.type_of tab)
-  | ExternMemory mem -> ExternMemoryType (Memory.type_of mem)
-  | ExternGlobal glob -> ExternGlobalType (Global.type_of glob)
+  { uid = issue_module_inst_uid ();
+    new_abstypes = []; sealed_abstypes = []; types = []; funcs = [];
+    tables = []; memories = []; globals = []; exports = [];
+    elems = []; datas = [] }
 
 let export inst name =
   try Some (List.assoc name inst.exports) with Not_found -> None
diff --git a/interpreter/script/import.ml b/interpreter/script/import.ml
index c9e65eafcd..08f60d8631 100644
--- a/interpreter/script/import.ml
+++ b/interpreter/script/import.ml
@@ -1,5 +1,6 @@
 open Source
 open Ast
+open Extern_types
 
 module Unknown = Error.Make ()
 exception Unknown = Unknown.Error  (* indicates unknown import name *)
@@ -11,7 +12,7 @@ let register name lookup = registry := Registry.add name lookup !registry
 
 let lookup (m : module_) (im : import) : Instance.extern =
   let {module_name; item_name; idesc} = im.it in
-  let t = import_type m im in
+  let t = unresolved_import_type m im in
   try Registry.find module_name !registry item_name t with Not_found ->
     Unknown.error im.at
       ("unknown import \"" ^ string_of_name module_name ^
diff --git a/interpreter/script/import.mli b/interpreter/script/import.mli
index 7919297e16..15ffb979aa 100644
--- a/interpreter/script/import.mli
+++ b/interpreter/script/import.mli
@@ -4,5 +4,8 @@ val link : Ast.module_ -> Instance.extern list (* raises Unknown *)
 
 val register :
   Ast.name ->
-  (Ast.name -> Types.extern_type -> Instance.extern (* raises Not_found *)) ->
+  (Ast.name ->
+   Extern_types.unresolved_extern_type ->
+   Instance.extern (* raises Not_found *)
+  ) ->
   unit
diff --git a/interpreter/script/js.ml b/interpreter/script/js.ml
index f0eeb11441..f0af782498 100644
--- a/interpreter/script/js.ml
+++ b/interpreter/script/js.ml
@@ -2,6 +2,13 @@ open Types
 open Ast
 open Script
 open Source
+open Extern_types
+
+
+(* Abstract Types *)
+
+let raise_no_abstypes at = 
+  raise (Eval.Crash (at, "abstract types are not (yet) supported in JS"))
 
 
 (* Harness *)
@@ -176,12 +183,12 @@ function assert_return(action, expected) {
 module NameMap = Map.Make(struct type t = Ast.name let compare = compare end)
 module Map = Map.Make(String)
 
-type exports = extern_type NameMap.t
+type exports = unresolved_extern_type NameMap.t
 type modules = {mutable env : exports Map.t; mutable current : int}
 
 let exports m : exports =
   List.fold_left
-    (fun map exp -> NameMap.add exp.it.name (export_type m exp) map)
+    (fun map exp -> NameMap.add exp.it.name (unresolved_export_type m exp) map)
     NameMap.empty m.it.exports
 
 let modules () : modules = {env = Map.empty; current = 0}
@@ -248,6 +255,7 @@ let value v =
   | Values.Ref (HostRef n) ->
     [Const (Values.I32 n @@ v.at) @@ v.at; Call (hostref_idx @@ v.at) @@ v.at]
   | Values.Ref _ -> assert false
+  | Values.SealedAbs _ -> raise_no_abstypes v.at
 
 let invoke ft vs at =
   [ft @@ at], FuncImport (subject_type_idx @@ at) @@ at,
@@ -282,6 +290,8 @@ let assert_return ress ts at =
         BrIf (0l @@ at) @@ at ]
     | LitResult {it = Values.Ref _; _} ->
       assert false
+    | LitResult {it = Values.SealedAbs _; _} ->
+      raise_no_abstypes at
     | NanResult nanop ->
       let nan =
         match nanop.it with
@@ -315,11 +325,12 @@ let wrap item_name wrap_action wrap_assertion at =
   let itypes, idesc, action = wrap_action at in
   let locals, assertion = wrap_assertion at in
   let types =
+    let open Types_shorthand in
     (FuncType ([], []) @@ at) ::
-    (FuncType ([NumType I32Type], [RefType AnyRefType]) @@ at) ::
-    (FuncType ([RefType AnyRefType], [NumType I32Type]) @@ at) ::
-    (FuncType ([RefType AnyRefType], [NumType I32Type]) @@ at) ::
-    (FuncType ([RefType AnyRefType; RefType AnyRefType], [NumType I32Type]) @@ at) ::
+    (FuncType ([r (NumType I32Type)], [r (RefType AnyRefType)]) @@ at) ::
+    (FuncType ([r (RefType AnyRefType)], [r (NumType I32Type)]) @@ at) ::
+    (FuncType ([r (RefType AnyRefType)], [r (NumType I32Type)]) @@ at) ::
+    (FuncType ([r (RefType AnyRefType); r (RefType AnyRefType)], [r (NumType I32Type)]) @@ at) ::
     itypes
   in
   let imports =
@@ -354,16 +365,21 @@ let is_js_num_type = function
   | I32Type -> true
   | I64Type | F32Type | F64Type -> false
 
-let is_js_value_type = function
+let is_js_value_type at = function
   | NumType t -> is_js_num_type t
   | RefType t -> true
+  | SealedAbsType i -> raise_no_abstypes at
   | BotType -> assert false
 
-let is_js_global_type = function
-  | GlobalType (t, mut) -> is_js_value_type t && mut = Immutable
+let is_js_wrapped_value_type at = function
+  | RawValueType vt -> is_js_value_type at vt
+  | NewAbsType _ -> raise_no_abstypes at
+
+let is_js_global_type at = function
+  | GlobalType (t, mut) -> (is_js_value_type at) t && mut = Immutable
 
-let is_js_func_type = function
-  | FuncType (ins, out) -> List.for_all is_js_value_type (ins @ out)
+let is_js_func_type at = function
+  | FuncType (ins, out) -> List.for_all (is_js_wrapped_value_type at) (ins @ out)
 
 
 (* Script conversion *)
@@ -446,7 +462,8 @@ let of_action mods act =
     "call(" ^ of_var_opt mods x_opt ^ ", " ^ of_name name ^ ", " ^
       "[" ^ String.concat ", " (List.map of_value vs) ^ "])",
     (match lookup mods x_opt name act.at with
-    | ExternFuncType ft when not (is_js_func_type ft) ->
+    | ExternFuncType (ExternFuncSigType (_, _, ft))
+      when not (is_js_func_type act.at ft) ->
       let FuncType (_, out) = ft in
       Some (of_wrapper mods x_opt name (invoke ft vs), out)
     | _ -> None
@@ -454,9 +471,9 @@ let of_action mods act =
   | Get (x_opt, name) ->
     "get(" ^ of_var_opt mods x_opt ^ ", " ^ of_name name ^ ")",
     (match lookup mods x_opt name act.at with
-    | ExternGlobalType gt when not (is_js_global_type gt) ->
+    | ExternGlobalType gt when not (is_js_global_type act.at gt) ->
       let GlobalType (t, _) = gt in
-      Some (of_wrapper mods x_opt name (get gt), [t])
+      Some (of_wrapper mods x_opt name (get gt), [RawValueType t])
     | _ -> None
     )
 
diff --git a/interpreter/script/run.ml b/interpreter/script/run.ml
index 11764e43ab..d29c58602f 100644
--- a/interpreter/script/run.ml
+++ b/interpreter/script/run.ml
@@ -209,26 +209,18 @@ let input_stdin run =
 (* Printing *)
 
 let print_import m im =
-  let open Types in
+  let open Extern_types in
   let category, annotation =
-    match Ast.import_type m im with
-    | ExternFuncType t -> "func", string_of_func_type t
-    | ExternTableType t -> "table", string_of_table_type t
-    | ExternMemoryType t -> "memory", string_of_memory_type t
-    | ExternGlobalType t -> "global", string_of_global_type t
+    annotation_of_unresolved_extern_type (unresolved_import_type m im)
   in
   Printf.printf "  import %s \"%s\" \"%s\" : %s\n"
     category (Ast.string_of_name im.it.Ast.module_name)
       (Ast.string_of_name im.it.Ast.item_name) annotation
 
 let print_export m ex =
-  let open Types in
+  let open Extern_types in
   let category, annotation =
-    match Ast.export_type m ex with
-    | ExternFuncType t -> "func", string_of_func_type t
-    | ExternTableType t -> "table", string_of_table_type t
-    | ExternMemoryType t -> "memory", string_of_memory_type t
-    | ExternGlobalType t -> "global", string_of_global_type t
+    annotation_of_unresolved_extern_type (unresolved_export_type m ex)
   in
   Printf.printf "  export %s \"%s\" : %s\n"
     category (Ast.string_of_name ex.it.Ast.name) annotation
@@ -339,7 +331,7 @@ let run_action act : Values.value list =
       List.iter2 (fun v t ->
         if not (Types.match_value_type (Values.type_of_value v.it) t) then
           Script.error v.at "wrong type of argument"
-      ) vs ins;
+      ) vs (Types.unwrap_stack ins);
       Eval.invoke f (List.map (fun v -> v.it) vs)
     | Some _ -> Assert.error act.at "export is not a function"
     | None -> Assert.error act.at "undefined export"
diff --git a/interpreter/syntax/ast.ml b/interpreter/syntax/ast.ml
index 543469d820..582387822a 100644
--- a/interpreter/syntax/ast.ml
+++ b/interpreter/syntax/ast.ml
@@ -72,9 +72,9 @@ and instr' =
   | Nop                               (* do nothing *)
   | Drop                              (* forget a value *)
   | 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 *)
+  | Block of raw_stack_type * instr list  (* execute in sequence *)
+  | Loop of raw_stack_type * instr list   (* loop header *)
+  | If of raw_stack_type * instr list * instr list  (* conditional *)
   | Br of var                         (* break to n-th surrounding label *)
   | BrIf of var                       (* conditional break *)
   | BrTable of var list * var         (* indexed break *)
@@ -175,6 +175,7 @@ type type_ = func_type Source.phrase
 
 type export_desc = export_desc' Source.phrase
 and export_desc' =
+  | AbsTypeExport of var
   | FuncExport of var
   | TableExport of var
   | MemoryExport of var
@@ -189,6 +190,7 @@ and export' =
 
 type import_desc = import_desc' Source.phrase
 and import_desc' =
+  | AbsTypeImport of var
   | FuncImport of var
   | TableImport of table_type
   | MemoryImport of memory_type
@@ -205,6 +207,8 @@ and import' =
 type module_ = module_' Source.phrase
 and module_' =
 {
+  (* sealed_abstypes : abstype_id list;
+  open_abstypes :  *)
   types : type_ list;
   globals : global list;
   tables : table list;
@@ -222,6 +226,7 @@ and module_' =
 
 let empty_module =
 {
+  (* abstypes = []; *)
   types = [];
   globals = [];
   tables = [];
@@ -234,38 +239,6 @@ let empty_module =
   exports = [];
 }
 
-open Source
-
-let func_type_for (m : module_) (x : var) : func_type =
-  (Lib.List32.nth m.it.types x.it).it
-
-let import_type (m : module_) (im : import) : extern_type =
-  let {idesc; _} = im.it in
-  match idesc.it with
-  | FuncImport x -> ExternFuncType (func_type_for m x)
-  | TableImport t -> ExternTableType t
-  | MemoryImport t -> ExternMemoryType t
-  | GlobalImport t -> ExternGlobalType t
-
-let export_type (m : module_) (ex : export) : extern_type =
-  let {edesc; _} = ex.it in
-  let its = List.map (import_type m) m.it.imports in
-  let open Lib.List32 in
-  match edesc.it with
-  | FuncExport x ->
-    let fts =
-      funcs its @ List.map (fun f -> func_type_for m f.it.ftype) m.it.funcs
-    in ExternFuncType (nth fts x.it)
-  | TableExport x ->
-    let tts = tables its @ List.map (fun t -> t.it.ttype) m.it.tables in
-    ExternTableType (nth tts x.it)
-  | MemoryExport x ->
-    let mts = memories its @ List.map (fun m -> m.it.mtype) m.it.memories in
-    ExternMemoryType (nth mts x.it)
-  | GlobalExport x ->
-    let gts = globals its @ List.map (fun g -> g.it.gtype) m.it.globals in
-    ExternGlobalType (nth gts x.it)
-
 let string_of_name n =
   let b = Buffer.create 16 in
   let escape uc =
diff --git a/interpreter/syntax/free.ml b/interpreter/syntax/free.ml
index af322f672d..5bd16ccfff 100644
--- a/interpreter/syntax/free.ml
+++ b/interpreter/syntax/free.ml
@@ -109,6 +109,7 @@ let type_ (t : type_) = empty
 
 let export_desc (d : export_desc) =
   match d.it with
+  | AbsTypeExport x -> empty
   | FuncExport x -> funcs (var x)
   | TableExport x -> tables (var x)
   | MemoryExport x -> memories (var x)
@@ -116,6 +117,7 @@ let export_desc (d : export_desc) =
 
 let import_desc (d : import_desc) =
   match d.it with
+  | AbsTypeImport x -> empty
   | FuncImport x -> types (var x)
   | TableImport tt -> empty
   | MemoryImport mt -> empty
diff --git a/interpreter/syntax/types.ml b/interpreter/syntax/types.ml
index fb3f13b1ba..f68c7efe7f 100644
--- a/interpreter/syntax/types.ml
+++ b/interpreter/syntax/types.ml
@@ -2,21 +2,32 @@
 
 type num_type = I32Type | I64Type | F32Type | F64Type
 type ref_type = NullRefType | AnyRefType | FuncRefType
-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
+type value_type =
+  | NumType of num_type
+  | RefType of ref_type
+  (* Start: Abstract Types *)
+  | SealedAbsType of int32
+  (* End: Abstract Types *)
+  | BotType
+type raw_stack_type = value_type list
+
+type wrapped_value_type =
+  | RawValueType of value_type
+  | NewAbsType of value_type * int32
+type wrapped_stack_type = wrapped_value_type list
+type func_type = FuncType of wrapped_stack_type * wrapped_stack_type
 
 type 'a limits = {min : 'a; max : 'a option}
 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 extern_type =
-  | ExternFuncType of func_type
-  | ExternTableType of table_type
-  | ExternMemoryType of memory_type
-  | ExternGlobalType of global_type
 
+let unwrap = function
+  | RawValueType vt -> vt
+  | NewAbsType (vt, _) -> vt
+
+let unwrap_stack = List.map unwrap
 
 (* Attributes *)
 
@@ -40,6 +51,9 @@ 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'
+  (* Start: Abstract Types *)
+  | SealedAbsType a1, SealedAbsType a2 -> a1 = a2
+  (* End: Abstract Types *)
   | BotType, _ -> true
   | _, _ -> false
 
@@ -63,33 +77,19 @@ let match_global_type (GlobalType (t1, mut1)) (GlobalType (t2, mut2)) =
   mut1 = mut2 &&
   (t1 = t2 || mut2 = Immutable && match_value_type t1 t2)
 
-let match_extern_type et1 et2 =
-  match et1, et2 with
-  | ExternFuncType ft1, ExternFuncType ft2 -> match_func_type ft1 ft2
-  | ExternTableType tt1, ExternTableType tt2 -> match_table_type tt1 tt2
-  | ExternMemoryType mt1, ExternMemoryType mt2 -> match_memory_type mt1 mt2
-  | ExternGlobalType gt1, ExternGlobalType gt2 -> match_global_type gt1 gt2
-  | _, _ -> false
-
 let is_num_type = function
   | NumType _ | BotType -> true
   | RefType _ -> false
+  (* Start: Abstract Types *)
+  | SealedAbsType _ -> false
+  (* End: Abstract Types *)
 
 let is_ref_type = function
   | NumType _ -> false
   | RefType _ | BotType -> true
-
-
-(* Filters *)
-
-let funcs =
-  Lib.List.map_filter (function ExternFuncType t -> Some t | _ -> None)
-let tables =
-  Lib.List.map_filter (function ExternTableType t -> Some t | _ -> None)
-let memories =
-  Lib.List.map_filter (function ExternMemoryType t -> Some t | _ -> None)
-let globals =
-  Lib.List.map_filter (function ExternGlobalType t -> Some t | _ -> None)
+  (* Start: Abstract Types *)
+  | SealedAbsType _ -> false
+  (* End: Abstract Types *)
 
 
 (* String conversion *)
@@ -108,8 +108,15 @@ 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
+  (* Start: Abstract Types *)
+  | SealedAbsType i -> "abs{" ^ Int32.to_string i ^ "}"
+  (* End: Abstract Types *)
   | BotType -> "impossible"
 
+let string_of_wrapped_value_type = function
+  | RawValueType vt -> string_of_value_type vt
+  | NewAbsType (vt, i) -> "new abstype [" ^ string_of_value_type vt ^ "]"
+
 let string_of_value_types = function
   | [t] -> string_of_value_type t
   | ts -> "[" ^ String.concat " " (List.map string_of_value_type ts) ^ "]"
@@ -129,14 +136,11 @@ let string_of_global_type = function
   | GlobalType (t, Immutable) -> string_of_value_type t
   | GlobalType (t, Mutable) -> "(mut " ^ string_of_value_type t ^ ")"
 
-let string_of_stack_type ts =
+let string_of_raw_stack_type ts =
   "[" ^ String.concat " " (List.map string_of_value_type ts) ^ "]"
 
-let string_of_func_type (FuncType (ins, out)) =
-  string_of_stack_type ins ^ " -> " ^ string_of_stack_type out
+let string_of_wrapped_stack_type ts =
+  "[" ^ String.concat " " (List.map string_of_wrapped_value_type ts) ^ "]"
 
-let string_of_extern_type = function
-  | ExternFuncType ft -> "func " ^ string_of_func_type ft
-  | ExternTableType tt -> "table " ^ string_of_table_type tt
-  | ExternMemoryType mt -> "memory " ^ string_of_memory_type mt
-  | ExternGlobalType gt -> "global " ^ string_of_global_type gt
+let string_of_func_type (FuncType (ins, out)) =
+  string_of_wrapped_stack_type ins ^ " -> " ^ string_of_wrapped_stack_type out
diff --git a/interpreter/syntax/types_shorthand.ml b/interpreter/syntax/types_shorthand.ml
new file mode 100644
index 0000000000..f238e63189
--- /dev/null
+++ b/interpreter/syntax/types_shorthand.ml
@@ -0,0 +1,5 @@
+open Types
+
+let r vt = RawValueType vt
+
+let a vt i = NewAbsType (vt, i)
\ No newline at end of file
diff --git a/interpreter/syntax/values.ml b/interpreter/syntax/values.ml
index 6907ae75b9..41139688a9 100644
--- a/interpreter/syntax/values.ml
+++ b/interpreter/syntax/values.ml
@@ -11,7 +11,7 @@ type num = (I32.t, I64.t, F32.t, F64.t) op
 type ref_ = ..
 type ref_ += NullRef
 
-type value = Num of num | Ref of ref_
+type value = Num of num | Ref of ref_ | SealedAbs of int32
 
 
 (* Typing *)
@@ -28,17 +28,18 @@ let type_of_ref r = !type_of_ref' r
 let type_of_value = function
   | Num n -> NumType (type_of_num n)
   | Ref r -> RefType (type_of_ref r)
+  | SealedAbs i -> SealedAbsType i
 
 
 (* Projections *)
 
 let as_num = function
   | Num n -> n
-  | Ref _ -> failwith "as_num"
+  | _ -> failwith "as_num"
 
 let as_ref = function
-  | Num _ -> failwith "as_ref"
   | Ref r -> r
+  | _ -> failwith "as_ref"
 
 
 (* Defaults *)
@@ -55,6 +56,7 @@ let default_ref = function
 let default_value = function
   | NumType t' -> Num (default_num t')
   | RefType t' -> Ref (default_ref t')
+  | SealedAbsType i -> SealedAbs i
   | BotType -> assert false
 
 
@@ -71,9 +73,12 @@ let string_of_num = function
 let string_of_ref' = ref (function NullRef -> "null" | _ -> "ref")
 let string_of_ref r = !string_of_ref' r
 
+let string_of_sealedabs i = "must_init{" ^ Int32.to_string i ^ "}"
+
 let string_of_value = function
   | Num n -> string_of_num n
   | Ref r -> string_of_ref r
+  | SealedAbs i -> string_of_sealedabs i
 
 let string_of_values = function
   | [v] -> string_of_value v
diff --git a/interpreter/text/arrange.ml b/interpreter/text/arrange.ml
index 6fc76e9325..5de11e77f4 100644
--- a/interpreter/text/arrange.ml
+++ b/interpreter/text/arrange.ml
@@ -58,13 +58,15 @@ let break_string s =
 let num_type t = string_of_num_type t
 let ref_type t = string_of_ref_type t
 let value_type t = string_of_value_type t
+let wrapped_value_type t = string_of_wrapped_value_type t
 
 let decls kind ts = tab kind (atom value_type) ts
+let decls_wrapped kind ts = tab kind (atom wrapped_value_type) ts
 
-let stack_type ts = decls "result" ts
+let raw_stack_type ts = decls "result" ts
 
 let func_type (FuncType (ins, out)) =
-  Node ("func", decls "param" ins @ decls "result" out)
+  Node ("func", decls_wrapped "param" ins @ decls_wrapped "result" out)
 
 let struct_type = func_type
 
@@ -228,10 +230,10 @@ let rec instr e =
     | 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
+    | Block (ts, es) -> "block", raw_stack_type ts @ list instr es
+    | Loop (ts, es) -> "loop", raw_stack_type ts @ list instr es
     | If (ts, es1, es2) ->
-      "if", stack_type ts @
+      "if", raw_stack_type ts @
         [Node ("then", list instr es1); Node ("else", list instr es2)]
     | Br x -> "br " ^ var x, []
     | BrIf x -> "br_if " ^ var x, []
@@ -358,6 +360,7 @@ let typedef i ty =
 
 let import_desc fx tx mx gx d =
   match d.it with
+  | AbsTypeImport x -> Node ("abstype_sealed", [atom var x])
   | FuncImport x ->
     incr fx; Node ("func $" ^ nat (!fx - 1), [Node ("type", [atom var x])])
   | TableImport t ->
@@ -375,6 +378,7 @@ let import fx tx mx gx im =
 
 let export_desc d =
   match d.it with
+  | AbsTypeExport x -> Node ("abstype_new", [atom var x])
   | FuncExport x -> Node ("func", [atom var x])
   | TableExport x -> Node ("table", [atom var x])
   | MemoryExport x -> Node ("memory", [atom var x])
diff --git a/interpreter/text/lexer.mll b/interpreter/text/lexer.mll
index 3a1c3f1145..14c3b56089 100644
--- a/interpreter/text/lexer.mll
+++ b/interpreter/text/lexer.mll
@@ -183,6 +183,13 @@ rule token = parse
   | "ref.host" { REF_HOST }
   | "ref.is_null" { REF_IS_NULL }
 
+  (* Start: Abstract Types *)
+  | "abstype_new" { ABSTYPE_NEW }
+  | "abstype_new_ref" { ABSTYPE_NEW_REF }
+  | "abstype_sealed" { ABSTYPE_SEALED }
+  | "abstype_sealed_ref" { ABSTYPE_SEALED_REF }
+  (* End: Abstract Types *)
+
   | "nop" { NOP }
   | "unreachable" { UNREACHABLE }
   | "drop" { DROP }
diff --git a/interpreter/text/parser.mly b/interpreter/text/parser.mly
index 305765c69d..c992228a5e 100644
--- a/interpreter/text/parser.mly
+++ b/interpreter/text/parser.mly
@@ -70,17 +70,24 @@ let empty () = {map = VarMap.empty; count = 0l}
 type types = {space : space; mutable list : type_ list}
 let empty_types () = {space = empty (); list = []}
 
+type new_abstypes = {space : space; mutable list : value_type list} 
+let empty_new_abstypes () : new_abstypes = {space = empty (); list = []}
+
 type context =
   { types : types; tables : space; memories : space;
     funcs : space; locals : space; globals : space;
     data : space; elems : space;
-    labels : int32 VarMap.t }
+    labels : int32 VarMap.t;
+    new_abstypes : new_abstypes;
+    sealed_abstypes : space }
 
 let empty_context () =
   { types = empty_types (); tables = empty (); memories = empty ();
     funcs = empty (); locals = empty (); globals = empty ();
     data = empty (); elems = empty ();
-    labels = VarMap.empty }
+    labels = VarMap.empty;
+    new_abstypes = empty_new_abstypes ();
+    sealed_abstypes = empty () }
 
 let enter_func (c : context) =
   {c with labels = VarMap.empty; locals = empty ()}
@@ -89,6 +96,8 @@ let lookup category space x =
   try VarMap.find x.it space.map
   with Not_found -> error x.at ("unknown " ^ category ^ " " ^ x.it)
 
+let new_abstype (c : context) x = lookup "abstype_new" c.new_abstypes.space x
+let sealed_abstype (c : context) x = lookup "abstype_sealed" c.sealed_abstypes x
 let type_ (c : context) x = lookup "type" c.types.space x
 let func (c : context) x = lookup "function" c.funcs x
 let local (c : context) x = lookup "local" c.locals x
@@ -101,6 +110,10 @@ let label (c : context) x =
   try VarMap.find x.it c.labels
   with Not_found -> error x.at ("unknown label " ^ x.it)
 
+let unwrap_new_abstype (c : context) x : value_type =
+  try (Lib.List32.nth c.new_abstypes.list x.it)
+  with Failure _ -> error x.at ("unknown abstype_new " ^ Int32.to_string x.it)
+
 let func_type (c : context) x =
   try (Lib.List32.nth c.types.list x.it).it
   with Failure _ -> error x.at ("unknown type " ^ Int32.to_string x.it)
@@ -116,6 +129,10 @@ let bind category space x =
     error x.at ("too many " ^ category ^ " bindings");
   i
 
+let bind_new_abstype (c : context) x vt =
+  c.new_abstypes.list <- c.new_abstypes.list @ [vt];
+  bind "new abstype" c.new_abstypes.space x
+let bind_sealed_abstype (c : context) x = bind "sealed abstype" c.sealed_abstypes x
 let bind_type (c : context) x ty =
   c.types.list <- c.types.list @ [ty];
   bind "type" c.types.space x
@@ -136,11 +153,15 @@ let anon category space n =
     error no_region ("too many " ^ category ^ " bindings");
   i
 
+let anon_new_abstype (c : context) vt =
+  c.new_abstypes.list <- c.new_abstypes.list @ [vt];
+  anon "new abstype" c.new_abstypes.space 1l
+let anon_sealed_abstype (c : context) = anon "sealed abstype" c.sealed_abstypes 1l
 let anon_type (c : context) ty =
   c.types.list <- c.types.list @ [ty];
   anon "type" c.types.space 1l
 let anon_func (c : context) = anon "function" c.funcs 1l
-let anon_locals (c : context) ts =
+let anon_locals (c : context) (ts : value_type list) =
   ignore (anon "local" c.locals (Lib.List32.length ts))
 let anon_global (c : context) = anon "global" c.globals 1l
 let anon_table (c : context) = anon "table" c.tables 1l
@@ -174,6 +195,9 @@ let inline_type_explicit (c : context) x ft at =
 %token MEMORY_SIZE MEMORY_GROW MEMORY_FILL MEMORY_COPY MEMORY_INIT DATA_DROP
 %token LOAD STORE OFFSET_EQ_NAT ALIGN_EQ_NAT
 %token CONST UNARY BINARY TEST COMPARE CONVERT
+
+%token ABSTYPE_NEW ABSTYPE_NEW_REF ABSTYPE_SEALED ABSTYPE_SEALED_REF
+
 %token REF_ANY REF_NULL REF_FUNC REF_HOST REF_IS_NULL
 %token FUNC START TYPE PARAM RESULT LOCAL GLOBAL
 %token TABLE ELEM MEMORY DATA DECLARE OFFSET ITEM IMPORT EXPORT
@@ -232,31 +256,59 @@ ref_type :
   | NULLREF { NullRefType }
 
 value_type :
-  | NUM_TYPE { NumType $1 }
-  | ref_type { RefType $1 }
+  | NUM_TYPE { fun c -> NumType $1 }
+  | ref_type { fun c -> RefType $1 }
+  | LPAR ABSTYPE_SEALED_REF var RPAR
+    { fun c -> SealedAbsType ($3 c sealed_abstype).it }
+
+unwrapped_value_type :
+  | value_type { fun c -> $1 c }
+  | LPAR ABSTYPE_NEW_REF var RPAR
+    { fun c -> let x = $3 c new_abstype in
+      unwrap_new_abstype c x }
+
+unwrapped_value_type_list :
+  | /* empty */ { fun c -> [] }
+  | unwrapped_value_type unwrapped_value_type_list
+    { fun c -> ($1 c) :: ($2 c) }
 
-value_type_list :
-  | /* empty */ { [] }
-  | value_type value_type_list { $1 :: $2 }
+wrapped_value_type :
+  | value_type { fun c -> RawValueType ($1 c) }
+  | LPAR ABSTYPE_NEW_REF var RPAR
+    { fun c -> let x = $3 c new_abstype in
+      NewAbsType (unwrap_new_abstype c x, x.it) }
+
+wrapped_value_type_list :
+  | /* empty */ { fun c -> [] }
+  | wrapped_value_type wrapped_value_type_list
+    { fun c -> $1 c :: $2 c }
+
+abstype_new :
+  | LPAR ABSTYPE_NEW value_type RPAR
+    { let at = at () in fun c -> anon_new_abstype c ($3 c) @@ at }
+  | LPAR ABSTYPE_NEW bind_var value_type RPAR  /* Sugar */
+    { let at = at () in fun c -> bind_new_abstype c $3 ($4 c) @@ at }
 
 global_type :
-  | value_type { GlobalType ($1, Immutable) }
-  | LPAR MUT value_type RPAR { GlobalType ($3, Mutable) }
+  | unwrapped_value_type
+    { fun c -> GlobalType ($1 c, Immutable) }
+  | LPAR MUT unwrapped_value_type RPAR
+    { fun c -> GlobalType ($3 c, Mutable) }
 
 def_type :
-  | LPAR FUNC func_type RPAR { $3 }
+  | LPAR FUNC func_type RPAR { fun c -> $3 c }
 
 func_type :
   | /* empty */
-    { FuncType ([], []) }
-  | LPAR RESULT value_type_list RPAR func_type
-    { let FuncType (ins, out) = $5 in
+    { fun c -> FuncType ([], []) }
+  | LPAR RESULT wrapped_value_type_list RPAR func_type
+    { fun c -> let FuncType (ins, out) = $5 c in
       if ins <> [] then error (at ()) "result before parameter";
-      FuncType (ins, $3 @ out) }
-  | LPAR PARAM value_type_list RPAR func_type
-    { let FuncType (ins, out) = $5 in FuncType ($3 @ ins, out) }
-  | LPAR PARAM bind_var value_type RPAR func_type  /* Sugar */
-    { let FuncType (ins, out) = $6 in FuncType ($4 :: ins, out) }
+      FuncType (ins, ($3 c) @ out) }
+  | LPAR PARAM wrapped_value_type_list RPAR func_type
+    { fun c -> let FuncType (ins, out) = $5 c in FuncType ($3 c @ ins, out) }
+  | LPAR PARAM bind_var wrapped_value_type RPAR func_type  /* Sugar */
+    { fun c -> let FuncType (ins, out) = $6 c in FuncType ($4 c :: ins, out) }
 
 table_type :
   | limits ref_type { TableType ($1, $2) }
@@ -385,14 +437,14 @@ plain_instr :
 
 select_instr :
   | SELECT select_instr_results
-    { let at = at () in fun c -> let b, ts = $2 in
+    { let at = at () in fun c -> let b, ts = $2 c 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 }
+  | LPAR RESULT unwrapped_value_type_list RPAR select_instr_results
+    { fun c -> let _, ts = $5 c in true, $3 c @ ts }
   | /* empty */
-    { false, [] }
+    { fun c -> false, [] }
 
 select_instr_instr :
   | SELECT select_instr_results_instr
@@ -401,8 +453,8 @@ select_instr_instr :
       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 }
+  | LPAR RESULT unwrapped_value_type_list RPAR select_instr_results_instr
+    { fun c -> let _, ts, es = $5 c in true, $3 c @ ts, es }
   | instr
     { fun c -> false, [], $1 c }
 
@@ -424,14 +476,14 @@ call_instr_type :
     { let at = at () in fun c -> inline_type c ($1 c) at }
 
 call_instr_params :
-  | LPAR PARAM value_type_list RPAR call_instr_params
-    { fun c -> let FuncType (ts1, ts2) = $5 c in FuncType ($3 @ ts1, ts2) }
+  | LPAR PARAM wrapped_value_type_list RPAR call_instr_params
+    { fun c -> let FuncType (ts1, ts2) = $5 c in FuncType ($3 c @ ts1, ts2) }
   | call_instr_results
     { fun c -> FuncType ([], $1 c) }
 
 call_instr_results :
-  | LPAR RESULT value_type_list RPAR call_instr_results
-    { fun c -> $3 @ $5 c }
+  | LPAR RESULT wrapped_value_type_list RPAR call_instr_results
+    { fun c -> $3 c @ $5 c }
   | /* empty */
     { fun c -> [] }
 
@@ -456,15 +508,15 @@ call_instr_type_instr :
       fun c -> let ft, es = $1 c in inline_type c ft at, es }
 
 call_instr_params_instr :
-  | LPAR PARAM value_type_list RPAR call_instr_params_instr
+  | LPAR PARAM wrapped_value_type_list RPAR call_instr_params_instr
     { fun c ->
-      let FuncType (ts1, ts2), es = $5 c in FuncType ($3 @ ts1, ts2), es }
+      let FuncType (ts1, ts2), es = $5 c in FuncType ($3 c @ ts1, ts2), es }
   | call_instr_results_instr
     { fun c -> let ts, es = $1 c in FuncType ([], ts), es }
 
 call_instr_results_instr :
-  | LPAR RESULT value_type_list RPAR call_instr_results_instr
-    { fun c -> let ts, es = $5 c in $3 @ ts, es }
+  | LPAR RESULT wrapped_value_type_list RPAR call_instr_results_instr
+    { fun c -> let ts, es = $5 c in $3 c @ ts, es }
   | instr
     { fun c -> [], $1 c }
 
@@ -481,11 +533,11 @@ block_instr :
       let ts, es1 = $3 c' in if_ ts es1 ($6 c') }
 
 block_type :
-  | LPAR RESULT value_type RPAR { [$3] }
+  | LPAR RESULT unwrapped_value_type RPAR { fun c -> [$3 c] }
 
 block :
   | block_type instr_list
-    { fun c -> $1, $2 c }
+    { fun c -> $1 c, $2 c }
   | instr_list { fun c -> [], $1 c }
 
 expr :  /* Sugar */
@@ -510,8 +562,8 @@ expr1 :  /* Sugar */
       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 }
+  | LPAR RESULT unwrapped_value_type_list RPAR select_expr_results
+    { fun c -> let _, ts, es = $5 c in true, $3 c @ ts, es }
   | expr_list
     { fun c -> false, [], $1 c }
 
@@ -527,21 +579,21 @@ call_expr_type :
       fun c -> let ft, es = $1 c in inline_type c ft at1, es }
 
 call_expr_params :
-  | LPAR PARAM value_type_list RPAR call_expr_params
+  | LPAR PARAM wrapped_value_type_list RPAR call_expr_params
     { fun c ->
-      let FuncType (ts1, ts2), es = $5 c in FuncType ($3 @ ts1, ts2), es }
+      let FuncType (ts1, ts2), es = $5 c in FuncType ($3 c @ ts1, ts2), es }
   | call_expr_results
     { fun c -> let ts, es = $1 c in FuncType ([], ts), es }
 
 call_expr_results :
-  | LPAR RESULT value_type_list RPAR call_expr_results
-    { fun c -> let ts, es = $5 c in $3 @ ts, es }
+  | LPAR RESULT wrapped_value_type_list RPAR call_expr_results
+    { fun c -> let ts, es = $5 c in $3 c @ ts, es }
   | expr_list
     { fun c -> [], $1 c }
 
 
 if_block :
-  | block_type if_block { fun c c' -> let ts, ess = $2 c c' in $1 @ ts, ess }
+  | block_type if_block { fun c c' -> let ts, ess = $2 c c' in $1 c @ ts, ess }
   | if_ { fun c c' -> [], $1 c c' }
 
 if_ :
@@ -576,22 +628,22 @@ func :
 
 func_fields :
   | type_use func_fields_body
-    { fun c x at ->
-      let t = inline_type_explicit c ($1 c type_) (fst $2) at in
-      [{(snd $2 (enter_func c)) with ftype = t} @@ at], [], [] }
+    { fun c x at -> let ffb = $2 c in
+      let t = inline_type_explicit c ($1 c type_) (fst ffb) at in
+      [{(snd ffb (enter_func c)) with ftype = t} @@ at], [], [] }
   | func_fields_body  /* Sugar */
-    { fun c x at ->
-      let t = inline_type c (fst $1) at in
-      [{(snd $1 (enter_func c)) with ftype = t} @@ at], [], [] }
+    { fun c x at -> let ffb = $1 c in
+      let t = inline_type c (fst ffb) at in
+      [{(snd ffb (enter_func c)) with ftype = t} @@ at], [], [] }
   | inline_import type_use func_fields_import  /* Sugar */
     { fun c x at ->
-      let t = inline_type_explicit c ($2 c type_) $3 at in
+      let t = inline_type_explicit c ($2 c type_) ($3 c) at in
       [],
       [{ module_name = fst $1; item_name = snd $1;
          idesc = FuncImport t @@ at } @@ at ], [] }
   | inline_import func_fields_import  /* Sugar */
     { fun c x at ->
-      let t = inline_type c $2 at in
+      let t = inline_type c ($2 c) at in
       [],
       [{ module_name = fst $1; item_name = snd $1;
          idesc = FuncImport t @@ at } @@ at ], [] }
@@ -600,44 +652,46 @@ func_fields :
       let fns, ims, exs = $2 c x at in fns, ims, $1 (FuncExport x) c :: exs }
 
 func_fields_import :  /* Sugar */
-  | func_fields_import_result { $1 }
-  | LPAR PARAM value_type_list RPAR func_fields_import
-    { let FuncType (ins, out) = $5 in FuncType ($3 @ ins, out) }
-  | LPAR PARAM bind_var value_type RPAR func_fields_import  /* Sugar */
-    { let FuncType (ins, out) = $6 in FuncType ($4 :: ins, out) }
+  | func_fields_import_result { fun c -> $1 c }
+  | LPAR PARAM wrapped_value_type_list RPAR func_fields_import
+    { fun c -> let FuncType (ins, out) = $5 c in FuncType ($3 c @ ins, out) }
+  | LPAR PARAM bind_var wrapped_value_type RPAR func_fields_import  /* Sugar */
+    { fun c -> let FuncType (ins, out) = $6 c in FuncType ($4 c :: ins, out) }
 
 func_fields_import_result :  /* Sugar */
-  | /* empty */ { FuncType ([], []) }
-  | LPAR RESULT value_type_list RPAR func_fields_import_result
-    { let FuncType (ins, out) = $5 in FuncType (ins, $3 @ out) }
+  | /* empty */ { fun c -> FuncType ([], []) }
+  | LPAR RESULT wrapped_value_type_list RPAR func_fields_import_result
+    { fun c -> let FuncType (ins, out) = $5 c in FuncType (ins, $3 c @ out) }
 
 func_fields_body :
-  | func_result_body { $1 }
-  | LPAR PARAM value_type_list RPAR func_fields_body
-    { let FuncType (ins, out) = fst $5 in
-      FuncType ($3 @ ins, out),
-      fun c -> ignore (anon_locals c $3); snd $5 c }
-  | LPAR PARAM bind_var value_type RPAR func_fields_body  /* Sugar */
-    { let FuncType (ins, out) = fst $6 in
-      FuncType ($4 :: ins, out),
-      fun c -> ignore (bind_local c $3); snd $6 c }
+  | func_result_body { fun c -> $1 c }
+  | LPAR PARAM wrapped_value_type_list RPAR func_fields_body
+    { fun c -> let ffb = $5 c in
+      let FuncType (ins, out) = fst ffb in
+      FuncType ($3 c @ ins, out),
+      fun c' -> ignore (anon_locals c' (unwrap_stack ($3 c))); snd ffb c' }
+  | LPAR PARAM bind_var wrapped_value_type RPAR func_fields_body  /* Sugar */
+    { fun c -> let ffb = $6 c in
+      let FuncType (ins, out) = fst ffb in
+      FuncType ($4 c :: ins, out),
+      fun c' -> ignore (bind_local c' $3); snd ffb c' }
 
 func_result_body :
-  | func_body { FuncType ([], []), $1 }
-  | LPAR RESULT value_type_list RPAR func_result_body
-    { let FuncType (ins, out) = fst $5 in
-      FuncType (ins, $3 @ out), snd $5 }
+  | func_body { fun c -> FuncType ([], []), $1 }
+  | LPAR RESULT wrapped_value_type_list RPAR func_result_body
+    { fun c -> let FuncType (ins, out) = fst ($5 c) in
+      FuncType (ins, $3 c @ out), snd ($5 c) }
 
 func_body :
   | instr_list
     { fun c -> let c' = anon_label c in
       {ftype = -1l @@ at(); locals = []; body = $1 c'} }
-  | LPAR LOCAL value_type_list RPAR func_body
-    { fun c -> ignore (anon_locals c $3); let f = $5 c in
-      {f with locals = $3 @ f.locals} }
-  | LPAR LOCAL bind_var value_type RPAR func_body  /* Sugar */
+  | LPAR LOCAL unwrapped_value_type_list RPAR func_body
+    { fun c -> ignore (anon_locals c ($3 c)); let f = $5 c in
+      {f with locals = $3 c @ f.locals} }
+  | LPAR LOCAL bind_var unwrapped_value_type RPAR func_body  /* Sugar */
     { fun c -> ignore (bind_local c $3); let f = $6 c in
-      {f with locals = $4 :: f.locals} }
+      {f with locals = $4 c :: f.locals} }
 
 
 /* Tables, Memories & Globals */
@@ -790,12 +844,12 @@ global :
 
 global_fields :
   | global_type const_expr
-    { fun c x at -> [{gtype = $1; ginit = $2 c} @@ at], [], [] }
+    { fun c x at -> [{gtype = $1 c; ginit = $2 c} @@ at], [], [] }
   | inline_import global_type  /* Sugar */
     { fun c x at ->
       [],
       [{ module_name = fst $1; item_name = snd $1;
-         idesc = GlobalImport $2 @@ at } @@ at], [] }
+         idesc = GlobalImport ($2 c) @@ at } @@ at], [] }
   | inline_export global_fields  /* Sugar */
     { fun c x at -> let globs, ims, exs = $2 c x at in
       globs, ims, $1 (GlobalExport x) c :: exs }
@@ -804,13 +858,17 @@ global_fields :
 /* Imports & Exports */
 
 import_desc :
+  | LPAR ABSTYPE_SEALED bind_var_opt RPAR
+    { let at = at () in
+      fun c -> let i = $3 c anon_sealed_abstype bind_sealed_abstype in
+      fun () -> AbsTypeImport (i @@ at) }
   | LPAR FUNC bind_var_opt type_use RPAR
     { fun c -> ignore ($3 c anon_func bind_func);
       fun () -> FuncImport ($4 c type_) }
   | LPAR FUNC bind_var_opt func_type RPAR  /* Sugar */
     { let at4 = ati 4 in
       fun c -> ignore ($3 c anon_func bind_func);
-      fun () -> FuncImport (inline_type c $4 at4) }
+      fun () -> FuncImport (inline_type c ($4 c) at4) }
   | LPAR TABLE bind_var_opt table_type RPAR
     { fun c -> ignore ($3 c anon_table bind_table);
       fun () -> TableImport $4 }
@@ -819,7 +877,7 @@ import_desc :
       fun () -> MemoryImport $4 }
   | LPAR GLOBAL bind_var_opt global_type RPAR
     { fun c -> ignore ($3 c anon_global bind_global);
-      fun () -> GlobalImport $4 }
+      fun () -> GlobalImport ($4 c) }
 
 import :
   | LPAR IMPORT name name import_desc RPAR
@@ -831,6 +889,7 @@ inline_import :
   | LPAR IMPORT name name RPAR { $3, $4 }
 
 export_desc :
+  | LPAR ABSTYPE_NEW_REF var RPAR { fun c -> AbsTypeExport ($3 c new_abstype) }
   | LPAR FUNC var RPAR { fun c -> FuncExport ($3 c func) }
   | LPAR TABLE var RPAR { fun c -> TableExport ($3 c table) }
   | LPAR MEMORY var RPAR { fun c -> MemoryExport ($3 c memory) }
@@ -849,13 +908,13 @@ inline_export :
 /* Modules */
 
 type_ :
-  | def_type { $1 @@ at () }
+  | def_type { let at = at () in fun c -> $1 c @@ at }
 
 type_def :
   | LPAR TYPE type_ RPAR
-    { fun c -> anon_type c $3 }
+    { fun c -> anon_type c ($3 c) }
   | LPAR TYPE bind_var type_ RPAR  /* Sugar */
-    { fun c -> bind_type c $3 $4 }
+    { fun c -> bind_type c $3 ($4 c) }
 
 start :
   | LPAR START var RPAR
@@ -867,6 +926,8 @@ module_fields :
   | module_fields1 { $1 }
 
 module_fields1 :
+  | abstype_new module_fields
+    { fun c -> ignore ($1 c); $2 c }
   | type_def module_fields
     { fun c -> ignore ($1 c); $2 c }
   | global module_fields
diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml
index 9752bd928d..4dc270cfdc 100644
--- a/interpreter/valid/valid.ml
+++ b/interpreter/valid/valid.ml
@@ -1,6 +1,7 @@
 open Ast
 open Source
 open Types
+open Extern_types
 
 
 (* Errors *)
@@ -16,6 +17,13 @@ let require b at s = if not b then error at s
 
 type context =
 {
+  (* Start: Abstract Type *)
+  (* NOTE: since within-module abstract types are just treated as
+     normal value_types, this property is only used for SealedAbsTypes.
+     The int items in the list represent global IDs for the SealedAbsTypes.
+   *)
+  sealed_abstypes : unresolved_abstype_ref list;
+  (* End: Abstract Type *)
   types : func_type list;
   funcs : func_type list;
   tables : table_type list;
@@ -25,12 +33,15 @@ type context =
   datas : unit list;
   locals : value_type list;
   results : value_type list;
-  labels : stack_type list;
+  labels : raw_stack_type list;
   refs : Free.t;
 }
 
 let empty_context =
-  { types = []; funcs = []; tables = []; memories = [];
+  (* Start: Abstract Type *)
+  { sealed_abstypes = [];
+  (* End: Abstract Type *)
+    types = []; funcs = []; tables = []; memories = [];
     globals = []; elems = []; datas = [];
     locals = []; results = []; labels = [];
     refs = Free.empty
@@ -80,8 +91,8 @@ 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_value_type ts1 ts2) at
-    ("type mismatch: operator requires " ^ string_of_stack_type ts2 ^
-     " but stack has " ^ string_of_stack_type ts1)
+    ("type mismatch: operator requires " ^ string_of_raw_stack_type ts2 ^
+     " but stack has " ^ string_of_raw_stack_type ts1)
 
 let pop (ell1, ts1) (ell2, ts2) at =
   let n1 = List.length ts1 in
@@ -239,7 +250,7 @@ let rec check_instr (c : context) (e : instr) (s : infer_stack_type) : op_type =
 
   | Call x ->
     let FuncType (ins, out) = func c x in
-    ins --> out
+    unwrap_stack ins --> unwrap_stack out
 
   | CallIndirect (x, y) ->
     let TableType (lim, t) = table c x in
@@ -247,7 +258,7 @@ let rec check_instr (c : context) (e : instr) (s : infer_stack_type) : op_type =
     require (match_ref_type t FuncRefType) x.at
       ("type mismatch: instruction requires table of functions" ^
        " but table has " ^ string_of_ref_type t);
-    (ins @ [NumType I32Type]) --> out
+    (unwrap_stack ins @ [NumType I32Type]) --> unwrap_stack out
 
   | LocalGet x ->
     [] --> [local c x]
@@ -388,12 +399,12 @@ and check_seq (c : context) (es : instr list) : infer_stack_type =
     let {ins; outs} = check_instr c e s in
     push outs (pop ins s e.at)
 
-and check_block (c : context) (es : instr list) (ts : stack_type) at =
+and check_block (c : context) (es : instr list) (ts : raw_stack_type) at =
   let s = check_seq c es in
   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_stack_type (snd s))
+    ("type mismatch: operator requires " ^ string_of_raw_stack_type ts ^
+     " but stack has " ^ string_of_raw_stack_type (snd s))
 
 
 (* Types *)
@@ -417,12 +428,18 @@ 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
+  | SealedAbsType i -> ()
   | BotType -> ()
 
+let check_wrapped_value_type (t : wrapped_value_type) at =
+  match t with
+  | RawValueType vt -> check_value_type vt at
+  | NewAbsType (vt, i) -> check_value_type vt at
+
 let check_func_type (ft : func_type) at =
   let FuncType (ins, out) = ft in
-  List.iter (fun t -> check_value_type t at) ins;
-  List.iter (fun t -> check_value_type t at) out;
+  List.iter (fun t -> check_wrapped_value_type t at) ins;
+  List.iter (fun t -> check_wrapped_value_type t at) out;
   check_arity (List.length out) at
 
 let check_table_type (tt : table_type) at =
@@ -460,8 +477,10 @@ let check_type (t : type_) =
 let check_func (c : context) (f : func) =
   let {ftype; locals; body} = f.it in
   let FuncType (ins, out) = type_ c ftype in
-  let c' = {c with locals = ins @ locals; results = out; labels = [out]} in
-  check_block c' body out f.at
+  let raw_out = unwrap_stack out in
+  let c' = {c with locals = unwrap_stack ins @ locals;
+                   results = raw_out; labels = [raw_out]} in
+  check_block c' body raw_out f.at
 
 
 let is_const (c : context) (e : instr) =
@@ -530,8 +549,10 @@ let check_start (c : context) (start : var option) =
   ) start
 
 let check_import (im : import) (c : context) : context =
-  let {module_name = _; item_name = _; idesc} = im.it in
+  let {module_name = mname; item_name = iname; idesc} = im.it in
   match idesc.it with
+  | AbsTypeImport x ->
+    {c with sealed_abstypes = NamedModuleAbsRef (mname, iname) :: c.sealed_abstypes }
   | FuncImport x ->
     {c with funcs = type_ c x :: c.funcs}
   | TableImport tt ->
@@ -549,6 +570,7 @@ module NameSet = Set.Make(struct type t = Ast.name let compare = compare end)
 let check_export (c : context) (set : NameSet.t) (ex : export) : NameSet.t =
   let {name; edesc} = ex.it in
   (match edesc.it with
+  | AbsTypeExport x -> () (* new abstypes can only be created within export statements *)
   | FuncExport x -> ignore (func c x)
   | TableExport x -> ignore (table c x)
   | MemoryExport x -> ignore (memory c x)
@@ -559,6 +581,7 @@ let check_export (c : context) (set : NameSet.t) (ex : export) : NameSet.t =
 
 let check_module (m : module_) =
   let
+    (* Start: Abstract Types *)
     { types; imports; tables; memories; globals; funcs; start; elems; datas;
       exports } = m.it
   in
@@ -566,7 +589,8 @@ let check_module (m : module_) =
     List.fold_right check_import imports
       { empty_context with
         refs = Free.list Free.elem elems;
-        types = List.map (fun ty -> ty.it) types;
+        (* `types` must be declared up front because the FuncImports in check_import may reference them *)
+        types = List.map (fun ty -> ty.it) types; 
       }
   in
   let c1 =
diff --git a/interpreter/winmake.bat b/interpreter/winmake.bat
index 6ff7e8caae..839e46c3a5 100644
--- a/interpreter/winmake.bat
+++ b/interpreter/winmake.bat
@@ -3,8 +3,8 @@ set NAME=wasm
 if '%1' neq '' set NAME=%1
 ocamlc.opt -c -w +a-3-4-27-42-44-45 -warn-error +a -I exec -I main -I syntax -I text -I binary -I script -I runtime -I util -I host -I valid -o exec/numeric_error.cmo exec/numeric_error.ml
 ocamlc.opt -c -w +a-3-4-27-42-44-45 -warn-error +a -I exec -I main -I syntax -I text -I binary -I script -I runtime -I util -I host -I valid -o exec/int.cmo exec/int.ml
-ocamlc.opt -c -w +a-3-4-27-42-44-45 -warn-error +a -I util -I main -I syntax -I text -I binary -I exec -I script -I runtime -I host -I valid -o util/lib.cmi util/lib.mli
 ocamlc.opt -c -w +a-3-4-27-42-44-45 -warn-error +a -I exec -I main -I syntax -I text -I binary -I script -I runtime -I util -I host -I valid -o exec/i32.cmo exec/i32.ml
+ocamlc.opt -c -w +a-3-4-27-42-44-45 -warn-error +a -I util -I main -I syntax -I text -I binary -I exec -I script -I runtime -I host -I valid -o util/lib.cmi util/lib.mli
 ocamlc.opt -c -w +a-3-4-27-42-44-45 -warn-error +a -I exec -I main -I syntax -I text -I binary -I script -I runtime -I util -I host -I valid -o exec/float.cmo exec/float.ml
 ocamlc.opt -c -w +a-3-4-27-42-44-45 -warn-error +a -I syntax -I main -I text -I binary -I exec -I script -I runtime -I util -I host -I valid -o syntax/types.cmo syntax/types.ml
 ocamlc.opt -c -w +a-3-4-27-42-44-45 -warn-error +a -I exec -I main -I syntax -I text -I binary -I script -I runtime -I util -I host -I valid -o exec/f32.cmo exec/f32.ml
@@ -19,7 +19,9 @@ ocamlc.opt -c -w +a-3-4-27-42-44-45 -warn-error +a -I runtime -I main -I syntax
 ocamlc.opt -c -w +a-3-4-27-42-44-45 -warn-error +a -I runtime -I main -I syntax -I text -I binary -I exec -I script -I util -I host -I valid -o runtime/table.cmi runtime/table.mli
 ocamlc.opt -c -w +a-3-4-27-42-44-45 -warn-error +a -I runtime -I main -I syntax -I text -I binary -I exec -I script -I util -I host -I valid -o runtime/instance.cmo runtime/instance.ml
 ocamlc.opt -c -w +a-3-4-27-42-44-45 -warn-error +a -I exec -I main -I syntax -I text -I binary -I script -I runtime -I util -I host -I valid -o exec/eval.cmi exec/eval.mli
+ocamlc.opt -c -w +a-3-4-27-42-44-45 -warn-error +a -I runtime -I main -I syntax -I text -I binary -I exec -I script -I util -I host -I valid -o runtime/extern_types.cmo runtime/extern_types.ml
 ocamlc.opt -c -w +a-3-4-27-42-44-45 -warn-error +a -I binary -I main -I syntax -I text -I exec -I script -I runtime -I util -I host -I valid -o binary/utf8.cmi binary/utf8.mli
+ocamlc.opt -c -w +a-3-4-27-42-44-45 -warn-error +a -I syntax -I main -I text -I binary -I exec -I script -I runtime -I util -I host -I valid -o syntax/types_shorthand.cmo syntax/types_shorthand.ml
 ocamlc.opt -c -w +a-3-4-27-42-44-45 -warn-error +a -I host -I main -I syntax -I text -I binary -I exec -I script -I runtime -I util -I valid -o host/env.cmo host/env.ml
 ocamlc.opt -c -w +a-3-4-27-42-44-45 -warn-error +a -I main -I syntax -I text -I binary -I exec -I script -I runtime -I util -I host -I valid -o main/flags.cmo main/flags.ml
 ocamlc.opt -c -w +a-3-4-27-42-44-45 -warn-error +a -I script -I main -I syntax -I text -I binary -I exec -I runtime -I util -I host -I valid -o script/import.cmi script/import.mli
@@ -55,6 +57,7 @@ ocamlc.opt -c -w +a-3-4-27-42-44-45 -warn-error +a -I runtime -I main -I syntax
 ocamlc.opt -c -w +a-3-4-27-42-44-45 -warn-error +a -I exec -I main -I syntax -I text -I binary -I script -I runtime -I util -I host -I valid -o exec/f32_convert.cmo exec/f32_convert.ml
 ocamlc.opt -c -w +a-3-4-27-42-44-45 -warn-error +a -I exec -I main -I syntax -I text -I binary -I script -I runtime -I util -I host -I valid -o exec/f64_convert.cmo exec/f64_convert.ml
 ocamlc.opt -c -w +a-3-4-27-42-44-45 -warn-error +a -I exec -I main -I syntax -I text -I binary -I script -I runtime -I util -I host -I valid -o exec/i32_convert.cmo exec/i32_convert.ml
+ocamlc.opt -c -w +a-3-4-27-42-44-45 -warn-error +a -I syntax -I main -I text -I binary -I exec -I script -I runtime -I util -I host -I valid -o syntax/free.cmi syntax/free.mli
 ocamlc.opt -c -w +a-3-4-27-42-44-45 -warn-error +a -I syntax -I main -I text -I binary -I exec -I script -I runtime -I util -I host -I valid -o syntax/operators.cmo syntax/operators.ml
 ocamlyacc text/parser.mly
 ocamlc.opt -c -w +a-3-4-27-42-44-45 -warn-error +a -I text -I main -I syntax -I binary -I exec -I script -I runtime -I util -I host -I valid -o text/parser.cmi text/parser.mli
@@ -67,9 +70,10 @@ ocamlc.opt -c -w +a-3-4-27-42-44-45 -warn-error +a -I script -I main -I syntax -
 ocamlc.opt -c -w +a-3-4-27-42-44-45 -warn-error +a -I text -I main -I syntax -I binary -I exec -I script -I runtime -I util -I host -I valid -o text/parse.cmo text/parse.ml
 ocamlc.opt -c -w +a-3-4-27-42-44-45 -warn-error +a -I text -I main -I syntax -I binary -I exec -I script -I runtime -I util -I host -I valid -o text/print.cmo text/print.ml
 ocamlc.opt -c -w +a-3-4-27-42-44-45 -warn-error +a -I valid -I main -I syntax -I text -I binary -I exec -I script -I runtime -I util -I host -o valid/valid.cmo valid/valid.ml
+ocamlc.opt -c -w +a-3-4-27-42-44-45 -warn-error +a -I syntax -I main -I text -I binary -I exec -I script -I runtime -I util -I host -I valid -o syntax/free.cmo syntax/free.ml
 ocamllex.opt -q text/lexer.mll
 ocamlc.opt -c -w +a-3-4-27-42-44-45 -warn-error +a -I text -I main -I syntax -I binary -I exec -I script -I runtime -I util -I host -I valid -o text/lexer.cmo text/lexer.ml
 ocamlc.opt -c -w +a-3-4-27-42-44-45 -warn-error +a -I text -I main -I syntax -I binary -I exec -I script -I runtime -I util -I host -I valid -o text/parser.cmo text/parser.ml
 ocamlc.opt -c -w +a-3-4-27-42-44-45 -warn-error +a -I text -I main -I syntax -I binary -I exec -I script -I runtime -I util -I host -I valid -o text/arrange.cmo text/arrange.ml
 ocamlc.opt -c -w +a-3-4-27-42-44-45 -warn-error +a -I util -I main -I syntax -I text -I binary -I exec -I script -I runtime -I host -I valid -o util/sexpr.cmo util/sexpr.ml
-ocamlc.opt bigarray.cma -I util -I binary -I exec -I syntax -I runtime -I host -I main -I script -I text -I valid util/lib.cmo binary/utf8.cmo exec/float.cmo exec/f32.cmo exec/f64.cmo exec/numeric_error.cmo exec/int.cmo exec/i32.cmo exec/i64.cmo exec/i32_convert.cmo exec/f32_convert.cmo exec/i64_convert.cmo exec/f64_convert.cmo syntax/types.cmo syntax/values.cmo runtime/memory.cmo util/source.cmo syntax/ast.cmo exec/eval_numeric.cmo runtime/func.cmo runtime/global.cmo runtime/table.cmo runtime/instance.cmo util/error.cmo exec/eval.cmo host/env.cmo host/spectest.cmo main/flags.cmo script/import.cmo binary/encode.cmo syntax/operators.cmo binary/decode.cmo script/script.cmo text/parser.cmo text/lexer.cmo text/parse.cmo script/js.cmo util/sexpr.cmo text/arrange.cmo text/print.cmo valid/valid.cmo script/run.cmo main/main.cmo -o main/main.byte
+ocamlc.opt bigarray.cma -I util -I binary -I exec -I syntax -I runtime -I main -I host -I script -I text -I valid util/lib.cmo binary/utf8.cmo exec/float.cmo exec/f32.cmo exec/f64.cmo exec/numeric_error.cmo exec/int.cmo exec/i32.cmo exec/i64.cmo exec/i32_convert.cmo exec/f32_convert.cmo exec/i64_convert.cmo exec/f64_convert.cmo syntax/types.cmo syntax/values.cmo runtime/memory.cmo util/source.cmo syntax/ast.cmo exec/eval_numeric.cmo main/flags.cmo runtime/func.cmo runtime/global.cmo runtime/table.cmo runtime/instance.cmo runtime/extern_types.cmo util/error.cmo exec/eval.cmo host/env.cmo syntax/types_shorthand.cmo host/spectest.cmo script/import.cmo syntax/free.cmo binary/encode.cmo syntax/operators.cmo binary/decode.cmo script/script.cmo text/parser.cmo text/lexer.cmo text/parse.cmo script/js.cmo util/sexpr.cmo text/arrange.cmo text/print.cmo valid/valid.cmo script/run.cmo main/main.cmo -o main/main.byte
diff --git a/test/core/abstract-types.wast b/test/core/abstract-types.wast
new file mode 100644
index 0000000000..ebca71a2c6
--- /dev/null
+++ b/test/core/abstract-types.wast
@@ -0,0 +1,200 @@
+;; Abstract Types
+
+(module $Mf
+  (abstype_new $a i32)
+  (export "a" (abstype_new_ref $a))
+  (func (export "out") (result (abstype_new_ref $a)) (i32.const 42))
+  (func (export "in") (param (abstype_new_ref $a)))
+)
+(register "Mf" $Mf)
+
+(assert_unlinkable
+  (module (import "Mf" "out" (func $out (result i32))))
+  "incompatible import type"
+)
+
+(assert_unlinkable
+  (module (import "Mf" "in" (func $in (param i32))))
+  "incompatible import type"
+)
+
+
+
+(module
+  (import "Mf" "a" (abstype_sealed $a))
+  (import "Mf" "out" (func $out (result (abstype_sealed_ref $a))))
+  (import "Mf" "in" (func $in (param (abstype_sealed_ref $a))))
+)
+
+(assert_invalid
+  (module
+    (import "Mf" "a" (abstype_sealed $a))
+    (import "Mf" "out" (func $out (result (abstype_sealed_ref $a))))
+    (func $invalid_call
+      (i32.add (i32.const 17) (call $out)))
+  )
+  "type mismatch: operator requires [i32 i32] but stack has [i32 abs{0}]"
+)
+
+(assert_invalid
+  (module
+    (import "Mf" "a" (abstype_sealed $a))
+    (import "Mf" "in" (func $in (param (abstype_sealed_ref $a))))
+    (func $invalid_call
+      (call $in (i32.const 0)))
+  )
+  "type mismatch: operator requires [abs{0}] but stack has [i32]"
+)
+
+(module
+  (import "Mf" "a" (abstype_sealed $a))
+  (import "Mf" "out" (func $out (result (abstype_sealed_ref $a))))
+  (import "Mf" "in" (func $in (param (abstype_sealed_ref $a))))
+  (func $call
+    (call $in (call $out)))
+)
+
+
+
+(module $Nf
+  (import "Mf" "a" (abstype_sealed $a))
+  (func (export "use_a") (param (abstype_sealed_ref $a)))
+)
+(register "Nf" $Nf)
+
+(assert_unlinkable
+  (module (import "Nf" "use_a" (func $use_a (param i32))))
+  "incompatible import type"
+)
+
+(module
+  (import "Mf" "a" (abstype_sealed $_a))
+  (import "Nf" "use_a" (func $use_a (param (abstype_sealed_ref $_a))))
+)
+
+
+
+;; NOTICE: sealed abstract types can't be exported; i.e. abstypes can't be reexported (to
+;; simplify resolving abstype references for equality checks; see notes in extern_types.ml
+;; about how abstract types are tied to module instances).
+;;
+;; (module $reexport_a
+;;   (import "Mf" "a" (abstype_sealed $a))
+;;   (export "a2" (abstype_sealed_ref $a))
+;; )
+;; 
+;; (module
+;;   (import "Mf" "a" (abstype_sealed $a))
+;;   (import "reexport_a" "a2" (abstype_sealed $a2))
+;;   (import "Mf" "out" (func $out (result (abstype_sealed_ref $a))))
+;;   (import "Mf" "in" (func $in (param (abstype_sealed_ref $a2))))
+;;   (func $call
+;;     (call $in (call $out)))
+;; )
+
+
+
+;; FIXME: 3rd-party modules are able to use double-sealed abstract types
+;; as if they are the original sealed abstract type, and visa-versa.
+;;
+;; (module $Mf_wrapped
+;;   (import "Mf" "a" (abstype_sealed $a))
+;;   (abstype_new $a_w (abstype_sealed_ref $a))
+;;   (export "a_w" (abstype_new_ref $a_w))
+;;   (import "Mf" "out" (func $Mf_out (result (abstype_sealed_ref $a))))
+;;   (import "Mf" "in" (func $Mf_in (param (abstype_sealed_ref $a))))
+;;   (func (export "out_w") (result (abstype_sealed_ref $a)) (call $Mf_out))
+;;   (func (export "in_w") (param (abstype_sealed_ref $a)) (call $Mf_in (local.get 0)))
+;; )
+;; (register "Mf_wrapped" $Mf_wrapped)
+;; 
+;; (assert_unlinkable
+;;   (module
+;;     (import "Mf_wrapped" "out_w" (func $out (result i32)))
+;;   )
+;;   "incompatible import type"
+;; )
+;; 
+;; (assert_unlinkable
+;;   (module
+;;     (import "Mf_wrapped" "a_w" (abstype_sealed $a_w))
+;;     (import "Mf" "out" (func $out (result (abstype_sealed_ref $a_w))))
+;;   )
+;;   "incompatible import type"
+;; )
+;; 
+;; (assert_unlinkable
+;;   (module
+;;     (import "Mf" "a" (abstype_sealed $a))
+;;     (import "Mf_wrapped" "out_w" (func $out (result (abstype_sealed_ref $a))))
+;;   )
+;;   "incompatible import type"
+;; )
+
+
+
+(module $M2f
+  (abstype_new $a i32)
+  (export "a1" (abstype_new_ref $a))
+  (export "a2" (abstype_new_ref $a))
+  (func (export "out") (result (abstype_new_ref $a)) (i32.const 42))
+  (func (export "in") (param (abstype_new_ref $a)))
+)
+(register "M2f" $M2f)
+
+;; TODO: should abstypes depend on imports or should they resolve be fully resolved to
+;; their (Module Instance * abstype_new) declarations before being compared? If the latter,
+;; then this test module would not be invalid.
+(assert_invalid
+  (module
+    (import "M2f" "a1" (abstype_sealed $a1))
+    (import "M2f" "a2" (abstype_sealed $a2))
+    (import "M2f" "out" (func $M2f_out (result (abstype_sealed_ref $a1))))
+    (import "M2f" "in" (func $M2f_in (param (abstype_sealed_ref $a2))))
+    (func (call $M2f_in (call $M2f_out)))
+  )
+  "type mismatch: operator requires [abs{1}] but stack has [abs{0}]"
+)
+
+
+
+(module $Mt
+  (abstype_new $a i32)
+  (export "a" (abstype_new_ref $a))
+  (type $f_abs (func (result (abstype_new_ref $a))))
+  (func $out (type $f_abs) (i32.const 42))
+  (table (export "table") 10 funcref)
+  (elem (i32.const 0) $out)
+)
+(register "Mt" $Mt)
+
+(module $Mt_no_abs
+  (type $f_raw (func (result i32)))
+  (table (import "Mt" "table") 10 funcref)
+  (func (export "call") (result i32)
+    (call_indirect (type $f_raw) (i32.const 0)))
+)
+(assert_trap (invoke $Mt_no_abs "call") "indirect call type mismatch")
+
+(module $Mt_abs
+  (import "Mt" "a" (abstype_sealed $a))
+  (type $f_abs (func (result (abstype_sealed_ref $a))))
+  (table (import "Mt" "table") 10 funcref)
+  (func (export "call") (result (abstype_sealed_ref $a))
+    (call_indirect (type $f_abs) (i32.const 0)))
+)
+
+
+
+;; FIXME: global imports aren't enforcing abstract types.
+;;
+;; (module $Mg
+;;   (abstype_new $a1 i32)
+;;   (global $g1 (export "g1") (abstype_new_ref $a1) (i32.const 0))
+;; )
+;; (register "Mg" $Mg)
+;; 
+;; (assert_unlinkable
+;;   (module (global $Mg_g1 (import "Mg" "g1") i32))
+;;   "incompatible import type"
+;; )