diff --git a/Semantics/AdministrativeSyntax.rkt b/Semantics/AdministrativeSyntax.rkt
index 33e66ca..c6ca066 100755
--- a/Semantics/AdministrativeSyntax.rkt
+++ b/Semantics/AdministrativeSyntax.rkt
@@ -13,7 +13,9 @@
   (L ::= hole (v ... (label n (e ...) L) e ...))
 
   (s ::= ((inst ...) (tabinst ...) (meminst ...)))
-  (cl ::= (i (func tf (local (t ...) (e ...)))))
+  (cl ::= (i (func tf (local (t ...) (e ...))))
+      (host-func tf (side-condition any_1 (procedure? (term any_1))))
+      uninit)
   (inst ::= ((cl ...) (v ...) (i ...) (i ...)))
 
   (tabinst ::= (cl ...))
diff --git a/Semantics/Instantiation.rkt b/Semantics/Instantiation.rkt
new file mode 100644
index 0000000..38971bc
--- /dev/null
+++ b/Semantics/Instantiation.rkt
@@ -0,0 +1,137 @@
+#lang racket
+
+(require redex/reduction-semantics
+         "RacketFFI.rkt"
+         "Semantics.rkt")
+
+(provide empty-store wasm-instantiate)
+
+(define empty-store (term (() () ())))
+
+;; s (listof (WASM mod)) import-dict -> s export-dict
+;; takes a WASM module, a start function name, and returns a store and a list of exports
+(define (wasm-instantiate s mod imports)
+
+  (define (lookup-import ns name)
+    (dict-ref (dict-ref imports
+                        ns
+                        (thunk (error (format "Link error: namespace ~a not in imports" ns)))
+              name
+              (thunk (error (format "Link error: imported object ~a not in namespace ~a" name ns))))))
+
+  (define (create-exports exs obj)
+    (map (λ (ex)
+           (match-let ([`(export ,name) ex])
+             (cons name obj)))
+         exs))
+  
+  (match-let ([`(,insts ,tabinsts ,meminsts) s]
+              [`(module ,fs ,globs ,tab? ,mem?) mod])
+    (let ([inst-num (length insts)])
+
+      (define (instantiate-funcs fs (i 0))
+        (if (empty? fs)
+            (values '() '())
+            (let-values ([(cl cl-exs)
+                          (match (first fs)
+                            [`(,exs (func ,tf (import ,ns ,name)))
+                             (values (match (lookup-import ns name)
+                                       [(? procedure? proc)
+                                        (term (host-func ,tf ,proc))]
+                                       [(wasm-func import-inst import-index)
+                                        ;; lookup the cl from the previous store
+                                        (match-let ([`(,s-cls ,_ ,_ ,_) (list-ref insts import-inst)])
+                                          (list-ref s-cls import-index))]
+                                       [_ (error "Link error: imported object is not a function")])
+                                     exs)]
+                            [`(,exs (func ,tf (local ,ts ,es)))
+                             (values (term (,inst-num (func ,tf (local ,ts ,es)))) exs)])]
+                         
+                         [(cls exports) (instantiate-funcs (rest fs) (add1 i))])
+          
+              (values (cons cl cls)
+                      (append (create-exports cl-exs (wasm-func inst-num i)) exports)))))
+
+      (define (instantiate-globs globs (i 0) (vs '()) (exports '()))
+        (if (empty? globs)
+            (values vs exports)
+            (let-values ([(vs-new v-exs)
+                          (match (first globs)
+                            [`(,exs (global (,_ ,t) (import ,ns ,name)))
+                             (values (match (lookup-import ns name)
+                                       [(? real? num)
+                                        (term (,t const ,(coerce-value t num)))]
+                                       [(wasm-global import-inst import-index)
+                                        ;; lookup the v from the previous store
+                                        (match-let ([`(,_ ,s-vs ,_ ,_) (list-ref insts import-inst)])
+                                          (list-ref s-vs import-index))]
+                                       [_ (error "Link error: imported object is not a global variable")])
+                                     exs)]
+                            [`(,exs (global ,_ ,es))
+                             (match-let ([`(((((() ,vs-new () ())) () ()) () (,v)))
+                                          (apply-reduction-relation*
+                                           (-> 0)
+                                           (term ((((() ,vs () ())) () ()) () ,es)))])
+                               (if (equal? v 'trap)
+                                   (error "Evaluating global initial value trapped")
+                                   (values (append vs-new (list v)) exs)))])])
+              (instantiate-globs
+               (rest globs)
+               (add1 i)
+               vs-new
+               (append exports (create-exports v-exs (wasm-global inst-num i)))))))
+
+      (define (instantiate-tab tab? cls)
+        (if (empty? tab?)
+            (values '() '() '())
+            (let-values ([(index tabinst tab-exs)
+                          (match (first tab?)
+                            [`(,exs (table ,n (import ,ns ,name)))
+                             (values (match (lookup-import ns name)
+                                       [(wasm-table import-index)
+                                        (unless (<= n (length (list-ref tabinsts import-index)))
+                                          (error "Link error: imported table does not have the right length"))
+                                        import-index]
+                                       [_ (error "Link error: imported object is not a table")])
+                                     '()
+                                     exs)]
+                            [`(,exs (table ,n ,is ...))
+                             (values (length tabinsts)
+                                     (map (curry list-ref cls) is)
+                                     exs)])])
+              (values (list index)
+                      (list tabinst)
+                      (create-exports tab-exs (wasm-table index))))))
+
+      (define (instantiate-mem mem?)
+        (if (empty? mem?)
+            (values '() '() '())
+            (let-values ([(index meminst mem-exs)
+                          (match (first mem?)
+                            [`(,exs (memory ,n (import ,ns ,name)))
+                             (values (match (lookup-import ns name)
+                                       [(wasm-memory import-index)
+                                        (unless (<= (* n (memory-page-size)) (bytes-length (list-ref meminsts import-index)))
+                                          (error "Link error: imported memory does not have the right length"))
+                                        import-index]
+                                       [_ (error "Link error: imported object is not a memory")])
+                                     '()
+                                     exs)]
+                            [`(,exs (memory ,n))
+                             (values (length meminsts)
+                                     (make-bytes (* n (memory-page-size)) 0)
+                                     exs)])])
+              (values (list index)
+                      (list meminst)
+                      (create-exports mem-exs (wasm-memory index))))))
+      
+      (let*-values ([(cls fs-exports) (instantiate-funcs fs)]
+                    [(vs globs-exports) (instantiate-globs globs)]
+                    [(tab-index mod-tabinsts tab-exports) (instantiate-tab tab? cls)]
+                    [(mem-index mod-meminsts mem-exports) (instantiate-mem mem?)]
+                    [(inst) (term (,cls ,vs ,tab-index ,mem-index))])
+        
+        (values (term (,(append insts (list inst))
+                       ,(append tabinsts mod-tabinsts)
+                       ,(append meminsts mod-meminsts)))
+                (append fs-exports globs-exports tab-exports mem-exports))))))
\ No newline at end of file
diff --git a/Semantics/RacketFFI.rkt b/Semantics/RacketFFI.rkt
new file mode 100644
index 0000000..9c6a5fc
--- /dev/null
+++ b/Semantics/RacketFFI.rkt
@@ -0,0 +1,159 @@
+#lang racket
+
+(require racket/flonum
+         redex/reduction-semantics
+         "AdministrativeSyntax.rkt"
+         "../Utilities.rkt"
+         "StoreUtilities.rkt"
+         "SizedOps.rkt")
+
+(provide racket-trampoline
+         memory-page-size
+         wasm-grow-memory
+         wasm-mem-read-integer
+         wasm-mem-write-integer!
+         wasm-grow-table!
+         wasm-table-get
+         wasm-table-set!
+         wasm-lookup-export
+
+         coerce-value
+
+         ;; These structs are provided so instantiation can use them,
+         ;; but they should not be constructed by ffi functions
+         (struct-out wasm-memory)
+         (struct-out wasm-table)
+         (struct-out wasm-func)
+         (struct-out wasm-global))
+
+
+(define memory-page-size (make-parameter 65536))
+
+;; these parameters are set when calling racket ffi procedures as the getter/setter for the wasm store
+(define get-store (make-parameter #f))
+(define set-store! (make-parameter #f))
+
+(define wasm-exports (make-parameter #f))
+
+(struct wasm-memory (index))
+
+;; wasm-memory natural -> void
+(define (wasm-grow-memory mem n)
+  (let ([i (wasm-memory-index mem)])
+    (match-let ([`(,insts ,tabinsts ,meminsts) ((get-store))])
+      ((set-store!) (term (,insts ,tabinsts (with-index ,meminsts ,i ,(bytes-append (list-ref meminsts i) (make-bytes (* (memory-page-size) n) 0)))))))))
+
+;; wasm-memory natural natural boolean -> integer
+(define (wasm-mem-read-integer mem offset width signed?)
+  (unless (or (= width 1) (= width 2) (= width 4) (= width 8))
+    (error "Integer width must be one of 1, 2, 4, 8"))
+  (match-let ([`(,_ ,_ ,meminsts) ((get-store))])
+    (let ([mem-bytes (list-ref meminsts (wasm-memory-index mem))])
+      (integer-bytes->integer mem-bytes signed? #f offset (+ offset width)))))
+
+;; wasm-memory natural natural integer -> void
+(define (wasm-mem-write-integer! mem offset width value)
+  (unless (or (= width 1) (= width 2) (= width 4) (= width 8))
+    (error "Integer width must be one of 1, 2, 4, 8"))
+  (match-let ([`(,insts ,tabinsts ,meminsts) ((get-store))])
+    (let* ([i (wasm-memory-index mem)]
+           [mem-bytes (bytes-copy (list-ref meminsts i))])
+      ((set-store!) (term (,insts ,tabinsts (with-index ,meminsts ,i ,(integer->integer-bytes value width (< value 0) #f mem-bytes offset))))))))
+
+(struct wasm-table (index))
+
+;; wasm-table natural -> void
+(define (wasm-grow-table! table n)
+  (let ([i (wasm-table-index table)])
+    (match-let ([`(,insts ,tabinsts ,meminsts) ((get-store))])
+      ((set-store!) (term (,insts (with-index ,tabinsts ,i ,(append (list-ref tabinsts i) (build-list n (λ (_) (term uninit))))) ,meminsts))))))
+
+;; wasm-table natural -> cl
+(define (wasm-table-get table n)
+  (let ([i (wasm-table-index table)])
+    (match-let ([`(,insts ,tabinsts ,meminsts) ((get-store))])
+      (list-ref (list-ref tabinsts i) n))))
+
+(struct wasm-func (inst index))
+
+;; wasm-table natural (or/c wasm-func 'uninit) -> void
+(define (wasm-table-set! table n func)
+  (unless (or (wasm-func? func) (equal? func 'uninit))
+    (error "Table entry must be an exported function or 'uninit"))
+  (let* ([i (wasm-table-index table)]
+         [s ((get-store))]
+         [cl (if (wasm-func? func)
+                 (term (store-func ,s ,(wasm-func-inst func) ,(wasm-func-index func)))
+                 'uninit)])
+    (match-let ([`(,insts ,tabinsts ,meminsts) s])
+      ((set-store!) (term (,insts (with-index ,tabinsts ,i (with-index ,(list-ref tabinsts i) n cl)) ,meminsts))))))
+
+
+;; wasm-func . args -> e e
+#;(define (wasm-func-call func . args)
+  ; need to change trampoline code to return es, then produce a local call and foreign call with the continuation
+  'TODO)
+
+(struct wasm-global (inst index))
+
+;; wasm-global real -> void
+;; commented out since you can't export mutable globals with the current WASM version modelled
+#;(define (wasm-set-global! global v)
+  (let ([inst (wasm-global-inst global)]
+        [i (wasm-global-index global)])
+    (match-let* ([`(,insts ,tabinsts ,meminsts) ((get-store))]
+                 [`(,cls ,globs ,tab ,mem) (list-ref insts inst)]
+                 [`(,t const ,_) (list-ref globs i)])
+      ((set-store!) (term ((with-index ,insts ,inst
+                             (,cls (with-index ,globs ,i (,t const ,(coerce-value t v))) ,tab ,mem))
+                           ,tabinsts
+                           ,meminsts))))))
+
+;; wasm-global -> real
+(define (wasm-get-global global)
+  (match-let* ([`(,insts ,_ ,_) ((get-store))]
+               [`(,_ ,globs ,_ ,_) (list-ref insts (wasm-global-inst global))]
+               [`(,_ const ,v) (list-ref globs (wasm-global-index global))])
+    v))
+      
+
+;; Exports are assumed to be valid
+(define (wasm-lookup-export name)
+  (dict-ref (wasm-exports) name))
+
+(define (racket-trampoline post exports proc s args)
+  (let* ([s-box (box s)]
+         [ret-vals (filter (λ (rv) (not (void? rv)))
+                           (call-with-values (thunk
+                                              (parameterize ([get-store (λ () (unbox s-box))]
+                                                             [set-store! (λ (s-new) (set-box! s-box s-new))]
+                                                             [wasm-exports exports])
+                                                (apply proc args)))
+                                             list))])
+    (unless (= (length post) (length ret-vals))
+      (error "Racket procedure produced an incorrect number of values"))
+
+    (term (,(unbox s-box) ,(map coerce-value post ret-vals)))))
+
+(define (coerce-value t n)
+  (unless (real? n)
+    (error "Cannot coerce a non-real value"))
+  (match t
+    ['i32
+     (unless (exact? n)
+       (error "Cannot coerce an inexact to an i32"))
+     (unless (<= (- (expt 2 31)) n (sub1 (expt 2 32)))
+       (error "Value outside of i32 range"))
+     (to-unsigned-sized 32 n)]
+    
+    ['i64
+     (unless (exact? n)
+       (error "Cannot coerce an inexact to an i64"))
+     (unless (<= (- (expt 2 63)) n (sub1 (expt 2 64)))
+       (error "Value outside of i64 range"))
+     (to-unsigned-sized 64 n)]
+    
+    ['f32 (flsingle (real->double-flonum n))]
+    
+    ['f64 (real->double-flonum n)]))
+
diff --git a/Semantics/Semantics.rkt b/Semantics/Semantics.rkt
index 3ab35da..2e10aaa 100644
--- a/Semantics/Semantics.rkt
+++ b/Semantics/Semantics.rkt
@@ -6,16 +6,15 @@
          "Utilities.rkt"
          "SimpleOps.rkt"
          "StoreUtilities.rkt"
-         "ConstUtilities.rkt")
+         "ConstUtilities.rkt"
+         "RacketFFI.rkt")
 
 (provide -> memory-page-size)
 
-(define memory-page-size (make-parameter 65536))
-
 ;; TL;DR about stack: the stack is implicit in the stream of instructions being processed.
 ;; This is because v \subset e, so although we say (e ...) it ends up looking like (v ... e ...).
 ;; Thus, the next instruction to execute is the head of e ..., and the stack is v ...
-(define (-> i)
+(define (-> i (exports '()))
   (reduction-relation
    WASM-Admin
    #:domain (s (v ...) (e ...))
@@ -157,7 +156,7 @@
 
    (c-> (s (v_l ...) (in-hole L (v_0 ... (i32 const j) (call-indirect tf) e_0 ...)))
         (s (v_l ...) (in-hole L (v_0 ... (call (store-tab s ,i j)) e_0 ...)))
-        (where (func tf (local (t ...) (e ...))) (cl-code-opt (store-tab s ,i j))))
+        (where (func tf _) (cl-code-opt (store-tab s ,i j))))
 
    (c-> (s (v_l ...) (in-hole L (v_0 ... (i32 const j) (call-indirect tf) e_0 ...)))
         (s (v_l ...) (in-hole L (v_0 ... trap e_0 ...)))
@@ -178,6 +177,12 @@
         (side-condition (= (length (term (v ...))) (length (term (t_1 ...)))))
         (where m ,(length (term (t_2 ...)))))
 
+   ;; Foreign function calls
+   (c-> (s (v_l ...) (in-hole L (v_0 ... (t_1 const c_1) ... (call cl) e_0 ...)))
+        (s_new (v_l ...) (in-hole L (v_0 ... (t_2 const c_2) ... e_0 ...)))
+        (where (host-func ((t_1 ...) -> (t_2 ...)) (name proc any)) cl)
+        (where (s_new (c_2 ...)) ,(racket-trampoline (term (t_2 ...)) exports (term proc) (term s) (term (c_1 ...)))))
+
    ;; Stuff inside functions calls!
    (c-> (s (v_l ...) (in-hole L (v_0 ... (local n (j (v_1 ...)) (v ...)) e_0 ...)))
         (s (v_l ...) (in-hole L (v_0 ... v ... e_0 ...)))
diff --git a/Semantics/StoreUtilities.rkt b/Semantics/StoreUtilities.rkt
index 77db358..df8cc54 100755
--- a/Semantics/StoreUtilities.rkt
+++ b/Semantics/StoreUtilities.rkt
@@ -9,9 +9,11 @@
 ; closure accessors
 ;; implements cl_code
 (define-metafunction WASM-Admin
-  cl-code : cl -> (func tf (local (t ...) (e ...)))
+  cl-code : cl -> any
   [(cl-code (i (func tf (local (t ...) (e ...)))))
-   (func tf (local (t ...) (e ...)))])
+   (func tf (local (t ...) (e ...)))]
+  ;; all other cl cases are undefined
+  [(cl-code _) #f])
 
 ;; returns the cl_code field if the input is a well-defined cl
 ;; otherwise returns #f
diff --git a/Semantics/Tests/FFITests.rkt b/Semantics/Tests/FFITests.rkt
new file mode 100644
index 0000000..c09e6fa
--- /dev/null
+++ b/Semantics/Tests/FFITests.rkt
@@ -0,0 +1,198 @@
+#lang racket
+
+(module+ test
+  (require rackunit
+           racket/flonum
+           redex/reduction-semantics
+           "../RacketFFI.rkt"
+           "../Semantics.rkt"
+           "../StoreUtilities.rkt")
+
+  (define (racket-add a b)
+    (+ a b))
+
+  (define (racket-sub1 a)
+    (sub1 a))
+
+  ;; basic ffi usage
+  (test-->>E (-> 0)
+             (term ((((((host-func ((i32 i32) -> (i32)) ,racket-add))
+                       () () ()))
+                     ()
+                     ()) ; store
+                    () ; locals
+                    ((i32 const 0) (i32 const 1) (i32 const 2) (call 0))))
+             (term ((((((host-func ((i32 i32) -> (i32)) ,racket-add))
+                       () () ()))
+                     ()
+                     ()) ; store
+                    () ; locals
+                    ((i32 const 0) (i32 const 3)))))
+
+  ;; ffi coercion i64
+  (test-->>E (-> 0)
+             (term ((((((host-func ((i32 i32) -> (i64)) ,racket-add))
+                       () () ()))
+                     ()
+                     ()) ; store
+                    () ; locals
+                    ((i32 const 0) (i32 const 1) (i32 const 2) (call 0))))
+             (term ((((((host-func ((i32 i32) -> (i64)) ,racket-add))
+                       () () ()))
+                     ()
+                     ()) ; store
+                    () ; locals
+                    ((i32 const 0) (i64 const 3)))))
+
+  ;; ffi coercion f64
+  (test-->>E (-> 0)
+             (term ((((((host-func ((i32 i32) -> (f64)) ,racket-add))
+                       () () ()))
+                     ()
+                     ()) ; store
+                    () ; locals
+                    ((i32 const 0) (i32 const 1) (i32 const 2) (call 0))))
+             (term ((((((host-func ((i32 i32) -> (f64)) ,racket-add))
+                       () () ()))
+                     ()
+                     ()) ; store
+                    () ; locals
+                    ((i32 const 0) (f64 const 3.0)))))
+
+  ;; ffi coercion f32
+  (test-->>E (-> 0)
+             (term ((((((host-func ((f64 f64) -> (f32)) ,racket-add))
+                       () () ()))
+                     ()
+                     ()) ; store
+                    () ; locals
+                    ((i32 const 0) (f64 const 0.1) (f64 const 0.2) (call 0))))
+             (term ((((((host-func ((f64 f64) -> (f32)) ,racket-add))
+                       () () ()))
+                     ()
+                     ()) ; store
+                    () ; locals
+                    ((i32 const 0) (f32 const ,(flsingle 0.3))))))
+
+  ;; ffi coercion -1 i32
+  (test-->>E (-> 0)
+             (term ((((((host-func ((i32) -> (i32)) ,racket-sub1))
+                       () () ()))
+                     ()
+                     ()) ; store
+                    () ; locals
+                    ((i32 const 0) (call 0))))
+             (term ((((((host-func ((i32) -> (i32)) ,racket-sub1))
+                       () () ()))
+                     ()
+                     ()) ; store
+                    () ; locals
+                    ((i32 const #xFFFFFFFF)))))
+
+  (define (make-memory size)
+    (make-bytes (* (memory-page-size) size) 0))
+  
+  (define (store-integer mem offset width value)
+    (integer->integer-bytes value width #f #f mem offset))
+
+  (define (racket-store-test)
+    (let ([mem (wasm-lookup-export "mem")])
+      (wasm-mem-write-integer! mem 0 4 -1)))
+
+  ;; ffi writes a value into memory
+  (parameterize ([memory-page-size 64])
+    (test-->>E (-> 0 `(("mem" . ,(wasm-memory 0))))
+               (term ((((((host-func (() -> ()) ,racket-store-test))
+                         () () (0)))
+                       ()
+                       (,(make-memory 1)))
+                      ()
+                      ((call 0))))
+               (term ((((((host-func (() -> ()) ,racket-store-test))
+                         () () (0)))
+                       ()
+                       (,(store-integer (make-memory 1) 0 4 #xFFFFFFFF)))
+                      ()
+                      ())))
+    )
+
+  ;; racket produced incorrect number of arguments
+  (check-exn
+   #rx".*"
+   (thunk
+    (apply-reduction-relation*
+     (-> 0)
+     (term ((((((host-func ((i32 i32) -> ()) ,racket-add))
+               () () ()))
+             ()
+             ()) ; store
+            () ; locals
+            ((i32 const 0) (i32 const 1) (i32 const 2) (call 0)))))))
+
+  ;; racket produced a value that can't be coerced
+  (check-exn
+   #rx".*"
+   (thunk
+    (apply-reduction-relation*
+     (-> 0)
+     (term ((((((host-func (() -> (i32)) ,(λ (s) (values s (list "hello world")))))
+               () () ()))
+             ()
+             ()) ; store
+            () ; locals
+            ((i32 const 0) (call 0)))))))
+
+  ;; racket produces an inexact when it expects an i32
+  (check-exn
+   #rx".*"
+   (thunk
+    (apply-reduction-relation*
+     (-> 0)
+     (term ((((((host-func (() -> (i32)) ,(λ (s) (values s (list 0.5)))))
+               () () ()))
+             ()
+             ()) ; store
+            () ; locals
+            ((call 0)))))))
+
+  ;; racket produces a value outside i32 range
+  (check-exn
+   #rx".*"
+   (thunk
+    (apply-reduction-relation*
+     (-> 0)
+     (term ((((((host-func (() -> (i32)) ,(λ (s) (values s (list (expt 2 32))))))
+               () () ()))
+             ()
+             ()) ; store
+            () ; locals
+            ((call 0)))))))
+
+  ;; racket produces an inexact when it expects an i64
+  (check-exn
+   #rx".*"
+   (thunk
+    (apply-reduction-relation*
+     (-> 0)
+     (term ((((((host-func (() -> (i64)) ,(λ (s) (values s (list 0.5)))))
+               () () ()))
+             ()
+             ()) ; store
+            () ; locals
+            ((call 0)))))))
+
+  ;; racket produces a value outside i64 range
+  (check-exn
+   #rx".*"
+   (thunk
+    (apply-reduction-relation*
+     (-> 0)
+     (term ((((((host-func (() -> (i64)) ,(λ (s) (values s (list (expt 2 64))))))
+               () () ()))
+             ()
+             ()) ; store
+            () ; locals
+            ((call 0)))))))
+
+  ;; TODO: more tests
+  )
\ No newline at end of file
diff --git a/Semantics/Tests/InstantiationTests.rkt b/Semantics/Tests/InstantiationTests.rkt
new file mode 100644
index 0000000..57caaec
--- /dev/null
+++ b/Semantics/Tests/InstantiationTests.rkt
@@ -0,0 +1,29 @@
+#lang racket
+
+(module+ test
+  (require rackunit
+           redex/reduction-semantics
+           "../Instantiation.rkt")
+
+  ;; Basic empty module instantiation
+  (let-values ([(s exs) (wasm-instantiate
+                         empty-store
+                         (term (module () () () ()))
+                         empty)])
+    (check-equal? s (term (((() () () ())) () ())))
+    (check-equal? exs empty))
+
+  ;; Chain module instantiation
+  (let-values ([(s exs) (wasm-instantiate
+                         (term (((() () () ())) () ()))
+                         (term (module () () () ()))
+                         empty)])
+    (check-equal? s (term (((() () () ())
+                            (() () () ()))
+                           ()
+                           ())))
+    (check-equal? exs empty))
+
+  ;; TODO: more tests
+  
+  )
\ No newline at end of file
diff --git a/Semantics/Tests/SemanticTests.rkt b/Semantics/Tests/SemanticTests.rkt
index a700f64..37d88cc 100644
--- a/Semantics/Tests/SemanticTests.rkt
+++ b/Semantics/Tests/SemanticTests.rkt
@@ -3,8 +3,7 @@
 (module+ test
   (require racket/flonum
            redex/reduction-semantics
-           "../Semantics.rkt"
-           rackunit)
+           "../Semantics.rkt")
 
   ;; Tests of unops
   (test-->>E (-> 0) ;; clz 0
@@ -723,6 +722,28 @@
                     ()
                     (trap))))
 
+  (test-->>E (-> 0) ;; call_indirect uninitialized cl
+             (term ((((() () (1) ()))
+                    (((0 (func ((i32) -> (i32)) (local () ((get-local 0) return))))
+                      uninit
+                      (2 (func ((i32 i32 i32) -> (i32)) (local () ((get-local 2) return)))))
+                     ((3 (func ((i32) -> (i32)) (local () ((get-local 0) return))))
+                      (4 (func ((i32 i32) -> (i32)) (local () ((get-local 1) return))))
+                      (5 (func ((i32 i32 i32) -> (i32)) (local () ((get-local 2) return))))))
+                    ())
+                    ()
+                    ((i32 const 2) (i32 const 1) (call-indirect ((i32) -> (i32))))))
+             (term ((((() () (1) ()))
+                    (((0 (func ((i32) -> (i32)) (local () ((get-local 0) return))))
+                      uninit
+                      (2 (func ((i32 i32 i32) -> (i32)) (local () ((get-local 2) return)))))
+                     ((3 (func ((i32) -> (i32)) (local () ((get-local 0) return))))
+                      (4 (func ((i32 i32) -> (i32)) (local () ((get-local 1) return))))
+                      (5 (func ((i32 i32 i32) -> (i32)) (local () ((get-local 2) return))))))
+                    ())
+                    ()
+                    (trap))))
+
   ;; Helper function for testing stores
 (define (make-memory size)
   (make-bytes (* (memory-page-size) size) 0))
diff --git a/Validation/InstructionTyping.rkt b/Validation/InstructionTyping.rkt
index 0361203..503a46e 100644
--- a/Validation/InstructionTyping.rkt
+++ b/Validation/InstructionTyping.rkt
@@ -19,10 +19,10 @@
 
 (define-judgment-form WASM-Typing
   #:contract (⊢ C (e ...) tf)
-
-  [------------------------------
-  (⊢ C ((t const c)) (() -> (t)))]
-
+  
+  [-------------------------------
+   (⊢ C ((t const c)) (() -> (t)))]
+  
   [-----------------------------
    (⊢ C ((t unop)) ((t) -> (t)))]