diff --git a/tapl/README.md b/tapl/README.md
index d2e6588..27c641d 100644
--- a/tapl/README.md
+++ b/tapl/README.md
@@ -9,4 +9,5 @@ A file extends its immediate parent file.
          - stlc+var.rkt
            - stlc+cons.rkt
              - stlc+box.rkt
-     - stlc+sub.rkt
\ No newline at end of file
+     - stlc+sub.rkt
+       - stlc+rec+var+sub.rkt
\ No newline at end of file
diff --git a/tapl/stlc+lit.rkt b/tapl/stlc+lit.rkt
index 97f7fbd..c4d6ab7 100644
--- a/tapl/stlc+lit.rkt
+++ b/tapl/stlc+lit.rkt
@@ -2,12 +2,9 @@
 (require
   (for-syntax racket/base syntax/parse)
   "typecheck.rkt")
-(require (prefix-in stlc: (only-in "stlc.rkt" #%app λ))
-         (except-in "stlc.rkt" #%app λ))
-(provide (rename-out [datum/tc #%datum]
-                     [stlc:#%app #%app]
-                     [stlc:λ λ]))
+(require "stlc.rkt")
 (provide (all-from-out "stlc.rkt"))
+(provide (rename-out [datum/tc #%datum]))
  
 ;; Simply-Typed Lambda Calculus, plus numeric literals and primitives
 ;; Types:
diff --git a/tapl/stlc+rec+sub.rkt b/tapl/stlc+rec+sub.rkt
new file mode 100644
index 0000000..5dd4389
--- /dev/null
+++ b/tapl/stlc+rec+sub.rkt
@@ -0,0 +1,50 @@
+#lang racket/base
+(require
+  (for-syntax racket/base syntax/parse racket/string syntax/stx racket/set "stx-utils.rkt")
+  "typecheck.rkt")
+(require (except-in "stlc+sub.rkt" #%app #%datum sub?)
+         (prefix-in stlc: (only-in "stlc+sub.rkt" #%app #%datum sub?))
+         (except-in "stlc+var.rkt" #%app #%datum +)
+         (prefix-in var: (only-in "stlc+var.rkt" #%datum)))
+(provide (rename-out [stlc:#%app #%app]
+                     [datum/tc #%datum]))
+(provide (except-out (all-from-out "stlc+sub.rkt") stlc:#%app)
+         (all-from-out "stlc+var.rkt"))
+(provide (for-syntax sub?))
+
+;; Simply-Typed Lambda Calculus, plus subtyping, plus records
+;; Types:
+;; - types from stlc+sub.rkt
+;; Type relations:
+;; - sub? extended to records
+;; Terms:
+;; - terms from stlc+sub.rkt, can leave record form as is
+
+(define-syntax (datum/tc stx)
+  (syntax-parse stx
+    [(_ . n:number) #'(stlc:#%datum . n)]
+    [(_ . x) #'(var:#%datum . x)]))
+(begin-for-syntax
+  (define (sub? τ1 τ2)
+    (or
+     (syntax-parse (list τ1 τ2) #:literals (× ∨)
+       [((× [k:str τk] ...) (× [l:str τl] ...))
+        #:when (subset? (stx-map syntax-e (syntax->list #'(l ...)))
+                        (stx-map syntax-e (syntax->list #'(k ...))))
+        (stx-andmap
+         (syntax-parser
+           [(l:str τl)
+            #:with (k_match τk_match) (str-stx-assoc #'l #'([k τk] ...))
+            (sub? #'τk_match #'τl)])
+         #'([l τl] ...))]
+       [((∨ [k:str τk] ...) (∨ [l:str τl] ...))
+        #:when (subset? (stx-map syntax-e (syntax->list #'(l ...)))
+                        (stx-map syntax-e (syntax->list #'(k ...))))
+        (stx-andmap
+         (syntax-parser
+           [(l:str τl)
+            #:with (k_match τk_match) (str-stx-assoc #'l #'([k τk] ...))
+            (sub? #'τk_match #'τl)])
+         #'([l τl] ...))]
+       [_ #f])
+     (stlc:sub? τ1 τ2))))
\ No newline at end of file
diff --git a/tapl/stlc+sub.rkt b/tapl/stlc+sub.rkt
index 18bbac7..d27bab0 100644
--- a/tapl/stlc+sub.rkt
+++ b/tapl/stlc+sub.rkt
@@ -5,14 +5,12 @@
 (require (except-in "stlc+lit.rkt" #%app #%datum +)
          (prefix-in stlc: (only-in "stlc+lit.rkt" #%datum)))
 (provide (rename-out [app/tc #%app] [datum/tc #%datum]))
-(provide (all-from-out "stlc+lit.rkt"))
-(provide (for-syntax sub?))
-
-;; can't write any terms with no base types
+(provide (except-out (all-from-out "stlc+lit.rkt") stlc:#%datum))
+(provide (for-syntax sub? subs?))
 
 ;; Simply-Typed Lambda Calculus, plus subtyping
 ;; Types:
-;; - types from stlc.rkt and stlc+lit.rkt
+;; - types from and stlc+lit.rkt
 ;; - Top, Num, Nat
 ;; Type relations:
 ;; - sub?
@@ -21,7 +19,7 @@
 ;;   - Int <: Num
 ;;   - →
 ;; Terms:
-;; - terms from stlc.rkt, stlc+lit.rkt, except redefined: app and datum
+;; - terms from stlc+lit.rkt, except redefined: app, datum, +
 
 (define-base-type Top)
 (define-base-type Num)
@@ -30,6 +28,9 @@
 ;(define-subtype Int <: Num)
 ;(define-subtype Nat <: Int)
 
+(define-primop + : (→ Num Num Num))
+(define-primop * : (→ Num Num Num))
+
 (define-syntax (datum/tc stx)
   (syntax-parse stx
     [(_ . n:nat) (⊢ (syntax/loc stx (#%datum . n)) #'Nat)]
@@ -37,8 +38,6 @@
     [(_ . n:number) (⊢ (syntax/loc stx (#%datum . n)) #'Num)]
     [(_ . x) #'(stlc:#%datum . x)]))
 
-(define-primop + : (→ Num Num Num))
-
 (begin-for-syntax
   (define (sub? τ1 τ2)
     (or (type=? τ1 τ2)
@@ -48,11 +47,11 @@
           [(Int τ) (sub? #'Num #'τ)]
           [(τ Num) (sub? #'τ #'Int)]
           [(τ Int) (sub? #'τ #'Nat)]
-          [((→ s1 s2) (→ t1 t2))
-           (and (sub? #'t1 #'s1)
+          [((→ s1 ... s2) (→ t1 ... t2))
+           (and (subs? #'(t1 ...) #'(s1 ...))
                 (sub? #'s2 #'t2))]
           [_ #f])))
-  (define (subs? τs1 τs2) (stx-andmap sub? τs1 τs2)))
+  (define (subs? τs1 τs2) (stx-andmap (eval-syntax (datum->syntax τs1 'sub?)) τs1 τs2)))
   ;(define (subs? ts1 ts2) (stx-andmap (λ (t1 t2) (printf "~a <: ~a: ~a\n" (syntax->datum t1) (syntax->datum t2) (sub? t1 t2)) (sub? t1 t2)) ts1 ts2)))
 
 (define-syntax (app/tc stx)
diff --git a/tapl/stlc+var.rkt b/tapl/stlc+var.rkt
index 70833c9..9effa14 100644
--- a/tapl/stlc+var.rkt
+++ b/tapl/stlc+var.rkt
@@ -7,7 +7,7 @@
 (require (prefix-in stlc: (only-in "stlc+tup.rkt" #%app λ tup proj let))
          (except-in "stlc+tup.rkt" #%app λ tup proj let))
 (provide (rename-out [stlc:#%app #%app] [stlc:λ λ] [stlc:let let]))
-(provide (all-from-out "stlc+tup.rkt"))
+(provide (except-out (all-from-out "stlc+tup.rkt") stlc:#%app stlc:#%datum))
 ;(provide define-type-alias define-variant module quote submod)
 (provide tup proj var case)
 
diff --git a/tapl/stx-utils.rkt b/tapl/stx-utils.rkt
index 4764b31..f01d0f5 100644
--- a/tapl/stx-utils.rkt
+++ b/tapl/stx-utils.rkt
@@ -28,4 +28,7 @@
   (list-ref (syntax->list stx) i))
 
 (define (stx-str=? s1 s2)
-  (string=? (syntax-e s1) (syntax-e s2)))
\ No newline at end of file
+  (string=? (syntax-e s1) (syntax-e s2)))
+
+(define (stx-sort stx cmp)
+  (sort (syntax->list stx) (λ (stx1 stx2) (cmp (syntax-e (stx-car stx1)) (syntax-e (stx-car stx2))))))
\ No newline at end of file
diff --git a/tapl/tests/stlc+rec+sub-tests.rkt b/tapl/tests/stlc+rec+sub-tests.rkt
new file mode 100644
index 0000000..efa0f09
--- /dev/null
+++ b/tapl/tests/stlc+rec+sub-tests.rkt
@@ -0,0 +1,86 @@
+#lang s-exp "../stlc+rec+sub.rkt"
+(require "rackunit-typechecking.rkt")
+
+;; record subtyping tests
+(check-type "coffee" : String)
+(check-type (tup ["coffee" = 3]) : (× ["coffee" Int])) ; element subtyping
+(check-type (tup ["coffee" = 3]) : (× ["coffee" Nat]))
+(check-type (tup ["coffee" = 3]) : (× ["coffee" Top]))
+(check-type (tup ["coffee" = 3]) : (× ["coffee" Num]))
+(check-not-type (tup ["coffee" = -3]) : (× ["coffee" Nat]))
+(check-type (tup ["coffee" = -3]) : (× ["coffee" Num]))
+(check-type (tup ["coffee" = -3] ["tea" = 3]) : (× ["coffee" Int])) ; width subtyping
+(check-type (tup ["coffee" = -3] ["tea" = 3]) : (× ["coffee" Num])) ; width+element subtyping
+
+;; record + fns
+(check-type (tup ["plus" = +]) : (× ["plus" (→ Num Num Num)]))
+(check-type + : (→ Num Num Num))
+(check-type (tup ["plus" = +]) : (× ["plus" (→ Int Num Num)]))
+(check-type (tup ["plus" = +]) : (× ["plus" (→ Int Num Top)]))
+(check-type (tup ["plus" = +] ["mul" = *]) : (× ["plus" (→ Int Num Top)]))
+
+;; previous record tests
+;; records (ie labeled tuples)
+(check-type "Stephen" : String)
+(check-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
+            (× ["name" String] ["phone" Int] ["male?" Bool]))
+(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name")
+            : String ⇒ "Stephen")
+(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name")
+            : String ⇒ "Stephen")
+(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "phone")
+            : Int ⇒ 781)
+(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "male?")
+            : Bool ⇒ #t)
+(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
+                (× ["my-name" String] ["phone" Int] ["male?" Bool]))
+(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
+                (× ["name" String] ["my-phone" Int] ["male?" Bool]))
+(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
+                (× ["name" String] ["phone" Int] ["is-male?" Bool]))
+
+
+;; previous basic subtyping tests ------------------------------------------------------
+(check-type 1 : Top)
+(check-type 1 : Num)
+(check-type 1 : Int)
+(check-type 1 : Nat)
+(check-type -1 : Top)
+(check-type -1 : Num)
+(check-type -1 : Int)
+(check-not-type -1 : Nat)
+(check-type ((λ ([x : Top]) x) 1) : Top ⇒ 1)
+(check-type ((λ ([x : Top]) x) -1) : Top ⇒ -1)
+(check-type ((λ ([x : Num]) x) -1) : Num ⇒ -1)
+(check-type ((λ ([x : Int]) x) -1) : Int ⇒ -1)
+(typecheck-fail ((λ ([x : Nat]) x) -1))
+(check-type (λ ([x : Int]) x) : (→ Int Int))
+(check-type (λ ([x : Int]) x) : (→ Int Num)) ; covariant output
+(check-not-type (λ ([x : Int]) x) : (→ Int Nat))
+(check-type (λ ([x : Int]) x) : (→ Nat Int)) ; contravariant input
+(check-not-type (λ ([x : Int]) x) : (→ Num Int))
+
+;; previous tests -------------------------------------------------------------
+;; some change due to more specific types
+(check-type 1 : Int)
+(check-not-type 1 : (→ Int Int))
+;(typecheck-fail "one") ; unsupported literal
+;(typecheck-fail #f) ; unsupported literal
+(check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int))
+(check-not-type (λ ([x : Int]) x) : Int)
+(check-type (λ ([x : Int]) x) : (→ Int Int))
+(check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int))
+(check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1)
+; Bool now defined
+;(typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool is not valid type
+;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is not valid type
+(typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type
+(check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y))
+            : (→ (→ Int Int Int) Int Int Int))
+;(check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3)
+;; changed test
+(check-type ((λ ([f : (→ Num Num Num)] [x : Int] [y : Int]) (f x y)) + 1 2) : Num ⇒ 3)
+(typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int
+(typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int
+(typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args
+(check-type ((λ ([x : Int]) (+ x x)) 10) : Num ⇒ 20)
diff --git a/tapl/tests/stlc+sub-tests.rkt b/tapl/tests/stlc+sub-tests.rkt
index 19fc3b1..4ecbf4a 100644
--- a/tapl/tests/stlc+sub-tests.rkt
+++ b/tapl/tests/stlc+sub-tests.rkt
@@ -21,6 +21,13 @@
 (check-type (λ ([x : Int]) x) : (→ Nat Int)) ; contravariant input
 (check-not-type (λ ([x : Int]) x) : (→ Num Int))
 
+(check-type + : (→ Num Num Num))
+(check-type + : (→ Int Num Num))
+(check-type + : (→ Int Int Num))
+(check-not-type + : (→ Top Int Num))
+(check-not-type + : (→ Top Int Int))
+(check-type + : (→ Nat Int Top))
+
 ;; previous tests -------------------------------------------------------------
 ;; some change due to more specific types
 (check-type 1 : Int)
diff --git a/tapl/tests/stlc+var-tests.rkt b/tapl/tests/stlc+var-tests.rkt
index 1ce002b..be5c30e 100644
--- a/tapl/tests/stlc+var-tests.rkt
+++ b/tapl/tests/stlc+var-tests.rkt
@@ -30,7 +30,7 @@
 (check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
                 (× ["name" String] ["phone" Int] ["is-male?" Bool]))
 
-
+;; variants
 (check-type (var "coffee" = (void) as (∨ ["coffee" Unit])) : (∨ ["coffee" Unit]))
 (check-not-type (var "coffee" = (void) as (∨ ["coffee" Unit])) : (∨ ["coffee" Unit] ["tea" Unit]))
 (typecheck-fail ((λ ([x : (∨ ["coffee" Unit] ["tea" Unit])]) x)