diff --git a/collects/typed-scheme/env/type-environments.ss b/collects/typed-scheme/env/type-environments.ss
index 57c04ee6..a5cf6e46 100644
--- a/collects/typed-scheme/env/type-environments.ss
+++ b/collects/typed-scheme/env/type-environments.ss
@@ -10,6 +10,9 @@
          dotted-env
          initial-tvar-env
          env-map
+         env-filter
+         env-vals
+         env-keys+vals
          with-dotted-env/extend)
 
 (require (prefix-in r: "../utils/utils.ss"))
@@ -19,6 +22,17 @@
 ;; eq? has the type of equal?, and l is an alist (with conses!)
 (define-struct env (eq? l))
 
+(define (env-vals e)
+  (map cdr (env-l e)))
+
+(define (env-keys+vals e)
+  (env-l e))
+
+(define (env-filter f e)
+  (match e
+    [(struct env (eq? l))
+    (make-env eq? (filter f l))]))
+
 ;; the initial type variable environment - empty
 ;; this is used in the parsing of types
 (define initial-tvar-env (make-env eq? '()))
diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss
index 98793c5a..2ce97160 100644
--- a/collects/typed-scheme/private/base-env.ss
+++ b/collects/typed-scheme/private/base-env.ss
@@ -102,10 +102,14 @@
 [fold-right (-polydots (c a b) ((list ((list c a) (b b) . ->... . c) c (-lst a))
                                 ((-lst b) b) . ->... . c))]
 [foldl
- (-poly (a b c)
+ (-poly (a b c d)
         (cl-> [((a b . -> . b) b (-lst a)) b]
-              [((a b c . -> . c) c (-lst a) (-lst b)) c]))]
-[foldr  (-poly (a b c) ((a b . -> . b) b (-lst a) . -> . b))]
+              [((a b c . -> . c) c (-lst a) (-lst b)) c]
+              [((a b c d . -> . d) d (-lst a) (-lst b) (-lst d)) d]))]
+[foldr  (-poly (a b c d)
+               (cl-> [((a b . -> . b) b (-lst a)) b]
+                     [((a b c . -> . c) c (-lst a) (-lst b)) c]
+                     [((a b c d . -> . d) d (-lst a) (-lst b) (-lst d)) d]))]
 [filter (-poly (a b) (cl->*
                       ((make-pred-ty (list a) B b)
                        (-lst a)
@@ -537,6 +541,10 @@
 
 [maybe-print-message (-String . -> . -Void)]
 
+[list->string ((-lst -Char) . -> . -String)]
+[string->list (-String . -> . (-lst -Char))]
+[sort (-poly (a) ((-lst a) (a a . -> . B) . -> . (-lst a)))]
+
 ;; scheme/list
 [last-pair (-poly (a) ((-mu x (Un a (-val '()) (-pair a x)))
                        . -> . 
@@ -567,3 +575,28 @@
 [real->decimal-string (N [-Nat] . ->opt .  -String)]
 
 [current-continuation-marks (-> -Cont-Mark-Set)]
+
+;; scheme/path
+
+[explode-path (-Pathlike . -> . (-lst (Un -Path (-val 'up) (-val 'same))))]
+[find-relative-path (-Pathlike -Pathlike . -> . -Path)]
+[simple-form-path (-Pathlike . -> . -Path)]
+[normalize-path (cl->* (-Pathlike . -> . -Path)
+                       (-Pathlike -Pathlike . -> . -Path))]
+[filename-extension (-Pathlike . -> . (-opt -Bytes))]
+[file-name-from-path (-Pathlike . -> . (-opt -Path))]
+[path-only (-Pathlike . -> . -Path)]
+[some-system-path->string (-Path . -> . -String)]
+[string->some-system-path 
+ (-String (Un (-val 'unix) (-val 'windows)) . -> . -Path)]
+
+;; scheme/math
+
+[sgn (-Real . -> . -Real)]
+[pi N]
+[sqr (N . -> . N)]
+[sgn (N . -> . N)]
+[conjugate (N . -> . N)]
+[sinh (N . -> . N)]
+[cosh (N . -> . N)]
+[tanh (N . -> . N)]
\ No newline at end of file
diff --git a/collects/typed-scheme/private/parse-type.ss b/collects/typed-scheme/private/parse-type.ss
index c3e9438e..0f8be85b 100644
--- a/collects/typed-scheme/private/parse-type.ss
+++ b/collects/typed-scheme/private/parse-type.ss
@@ -346,6 +346,26 @@
                                                                           (current-tvars))])
                                   (parse-type #'rest))
                                 (syntax-e #'bound)))))))]
+      [(dom ... rest ::: -> rng)
+       (and (eq? (syntax-e #'->) '->) 
+            (eq? (syntax-e #':::) '...))
+       (begin
+         (add-type-name-reference #'->)
+         (let ([bounds (filter (compose Dotted? cdr) (env-keys+vals (current-tvars)))])
+           (when (null? bounds)
+             (tc-error/stx stx "No type variable bound with ... in scope for ... type"))
+           (unless (null? (cdr bounds))
+             (tc-error/stx stx "Cannot infer bound for ... type"))
+           (match-let ([(cons var (struct Dotted (t))) (car bounds)])
+             (make-Function
+              (list
+               (make-arr-dots (map parse-type (syntax->list #'(dom ...)))
+                              (parse-type #'rng)
+                              (parameterize ([current-tvars (extend-env (list var)
+                                                                        (list (make-DottedBoth t))
+                                                                        (current-tvars))])
+                                (parse-type #'rest))
+                              var))))))]
       ;; has to be below the previous one
       [(dom ... -> rng) 
        (eq? (syntax-e #'->) '->)
@@ -365,6 +385,23 @@
                                                                         (current-tvars))])
                                 (parse-type #'dty))
                               (syntax-e #'bound))))]
+      [(values tys ... dty dd)
+       (and (eq? (syntax-e #'values) 'values) 
+            (eq? (syntax-e #'dd) '...))
+       (begin
+         (add-type-name-reference #'values)
+         (let ([bounds (filter (compose Dotted? cdr) (env-keys+vals (current-tvars)))])
+           (when (null? bounds)
+             (tc-error/stx stx "No type variable bound with ... in scope for ... type"))
+           (unless (null? (cdr bounds))
+             (tc-error/stx stx "Cannot infer bound for ... type"))
+           (match-let ([(cons var (struct Dotted (t))) (car bounds)])
+             (make-ValuesDots (map parse-type (syntax->list #'(tys ...)))
+                              (parameterize ([current-tvars (extend-env (list var) 
+                                                                        (list (make-DottedBoth t))
+                                                                        (current-tvars))])
+                                            (parse-type #'dty))
+                              var))))]
       [(values tys ...) 
        (eq? (syntax-e #'values) 'values)
        (-values (map parse-type (syntax->list #'(tys ...))))]
diff --git a/collects/typed-scheme/private/type-contract.ss b/collects/typed-scheme/private/type-contract.ss
index 2b0491ea..930437b7 100644
--- a/collects/typed-scheme/private/type-contract.ss
+++ b/collects/typed-scheme/private/type-contract.ss
@@ -17,7 +17,7 @@
  mzlib/trace
  scheme/list
  (only-in scheme/contract -> ->* case-> cons/c flat-rec-contract provide/contract any/c)
- (for-template scheme/base scheme/contract (only-in scheme/class object% is-a?/c subclass?/c)))
+ (for-template scheme/base scheme/contract (utils poly-c) (only-in scheme/class object% is-a?/c subclass?/c)))
 
 (define (define/fixup-contract? stx)
   (or (syntax-property stx 'typechecker:contract-def)
@@ -51,7 +51,9 @@
 (define (type->contract ty fail)
   (define vars (make-parameter '()))
   (let/cc exit
-    (let t->c ([ty ty])
+    (let loop ([ty ty] [pos? #t])
+      (define (t->c t) (loop t pos?))
+      (define (t->c/neg t) (loop t (not pos?)))
       (match ty
         [(or (App: _ _ _) (Name: _)) (t->c (resolve-once ty))]
         [(Univ:) #'any/c]
@@ -71,13 +73,13 @@
              (define-values (dom* rngs* rst)
                (match a
                  [(arr: dom (Values: rngs) #f #f '())
-                  (values (map t->c dom) (map t->c rngs) #f)]
+                  (values (map t->c/neg dom) (map t->c rngs) #f)]
                  [(arr: dom rng #f #f '())
-                  (values (map t->c dom) (list (t->c rng)) #f)]
+                  (values (map t->c/neg dom) (list (t->c rng)) #f)]
                  [(arr: dom (Values: rngs) rst #f '() )
-                  (values (map t->c dom) (map t->c rngs) (t->c rst))]
+                  (values (map t->c/neg dom) (map t->c rngs) (t->c/neg rst))]
                  [(arr: dom rng rst #f '())
-                  (values (map t->c dom) (list (t->c rng)) (t->c rst))]))
+                  (values (map t->c/neg dom) (list (t->c rng)) (t->c/neg rst))]))
              (with-syntax 
                  ([(dom* ...) dom*]
                   [rng* (match rngs*
@@ -99,12 +101,22 @@
          #`(cons/c #,(t->c t1) #,(t->c t2))]
         [(Opaque: p? cert)
          #`(flat-contract #,(cert p?))]
-        [(F: v) (cond [(assoc v (vars)) => cadr]
+        [(F: v) (cond [(assoc v (vars)) => (if pos? second third)]
                       [else (int-err "unknown var: ~a" v)])]
+	[(Poly: vs (and b (Function: _)))
+         (match-let ([(Poly-names: vs-nm _) ty])
+           (with-syntax ([(vs+ ...) (generate-temporaries (for/list ([v vs-nm]) (symbol-append v '+)))]
+			 [(vs- ...) (generate-temporaries (for/list ([v vs-nm]) (symbol-append v '-)))])
+             (parameterize ([vars (append (map list
+					       vs
+					       (syntax->list #'(vs+ ...))
+					       (syntax->list #'(vs- ...)))
+					  (vars))])
+               #`(poly/c ([vs- vs+] ...) #,(t->c b)))))]
         [(Mu: n b)
          (match-let ([(Mu-name: n-nm _) ty])
            (with-syntax ([(n*) (generate-temporaries (list n-nm))])
-             (parameterize ([vars (cons (list n #'n*) (vars))])
+             (parameterize ([vars (cons (list n #'n* #'n*) (vars))])
                #`(flat-rec-contract n* #,(t->c b)))))]
         [(Value: #f) #'false/c]    
         [(Instance: _) #'(is-a?/c object%)]
@@ -112,10 +124,7 @@
         [(Value: '()) #'null?]
         [(Struct: _ _ _ _ #f pred? cert) (cert pred?)]
         [(Syntax: (Base: 'Symbol _)) #'identifier?]
-        [(Syntax: t)
-         (if (equal? ty t:Any-Syntax)
-             #`syntax?
-             #`(syntax/c #,(t->c t)))]
+        [(Syntax: t) #`(syntax/c #,(t->c t))]
         [(Value: v) #`(flat-named-contract #,(format "~a" v) (lambda (x) (equal? x '#,v)))]
         [(Param: in out) #`(parameter/c #,(t->c out))]
 	[(Hashtable: k v) #`hash?]
diff --git a/collects/typed-scheme/ts-reference.scrbl b/collects/typed-scheme/ts-reference.scrbl
index 102a13e9..c2982e25 100644
--- a/collects/typed-scheme/ts-reference.scrbl
+++ b/collects/typed-scheme/ts-reference.scrbl
@@ -1,7 +1,10 @@
 #lang scribble/doc
 
-@begin[(require scribble/manual)
-       (require (for-label typed-scheme))]
+@begin[(require scribble/manual scribble/eval
+                scheme/sandbox)
+       (require (for-label typed-scheme
+                           scheme/list srfi/14
+                           version/check))]
 
 @begin[
 (define (item* header . args) (apply item @bold[header]{: } args))
@@ -52,6 +55,8 @@ The following base types are parameteric in their type arguments.
                                the first is the type the parameter accepts, and the second is the type returned.}
 @defform[(Pair s t)]{is the pair containing @scheme[s] as the @scheme[car]
   and @scheme[t] as the @scheme[cdr]}
+@defform[(HashTable k v)]{is the type of a @rtech{hash table} with key type
+   @scheme[k] and value type @scheme[v].}
 
 @subsubsub*section{Type Constructors}
 
@@ -245,3 +250,47 @@ known to Typed Scheme, either via @scheme[define-struct:] or
 Like @scheme[do], but each @scheme[id] having the associated type @scheme[t], and 
 the final body @scheme[expr] having the type @scheme[u].
 }
+
+@section{Libraries Provided With Typed Scheme}
+
+The @schememodname[typed-scheme] language corresponds to the
+@schememodname[scheme/base] language---that is, any identifier provided
+by @schememodname[scheme/base], such as @scheme[mod] is available by default in
+@schememodname[typed-scheme].  
+
+@schememod[typed-scheme
+(modulo 12 2)
+]
+
+Any value provided by @schememodname[scheme] is available by simply
+@scheme[require]ing it; use of @scheme[require/typed] is not
+neccessary.  
+
+@schememod[typed-scheme
+(require scheme/list)
+(display (first (list 1 2 3)))
+]
+
+Some libraries have counterparts in the @schemeidfont{typed}
+collection, which provide the same exports as the untyped versions.
+Such libraries include @schememodname[srfi/14],
+@schememodname[net/url], and many others.  
+
+@schememod[typed-scheme
+(require typed/srfi/14)
+(char-set= (string->char-set "hello")
+           (string->char-set "olleh"))
+]
+
+To participate in making more libraries available, please visit 
+@link["http://www.ccs.neu.edu/home/samth/adapt/"]{here}.
+
+
+Other libraries can be used with Typed Scheme via
+@scheme[require/typed].
+
+@schememod[typed-scheme
+(require/typed version/check
+               [check-version (-> (U Symbol (Listof Any)))])
+(check-version)
+]
diff --git a/collects/typed-scheme/typecheck/provide-handling.ss b/collects/typed-scheme/typecheck/provide-handling.ss
index 791d6384..66b3576a 100644
--- a/collects/typed-scheme/typecheck/provide-handling.ss
+++ b/collects/typed-scheme/typecheck/provide-handling.ss
@@ -54,15 +54,18 @@
                             (define/contract cnt-id #,cnt id)
                             (define-syntax export-id
                               (if (unbox typed-context?)
-                                  (make-rename-transformer #'id)
-                                  (make-rename-transformer #'cnt-id)))
+                                  (make-rename-transformer (syntax-property #'id 
+                                                                            'not-free-identifier=? #t))
+                                  (make-rename-transformer (syntax-property #'cnt-id
+                                                                            'not-free-identifier=? #t))))
                             (#%provide (rename export-id out-id)))))]
                    [else 
                     (with-syntax ([(export-id) (generate-temporaries #'(id))])
                       #`(begin                             
                           (define-syntax export-id
                             (if (unbox typed-context?)
-                                (make-rename-transformer #'id)
+                                (make-rename-transformer (syntax-property #'id 
+                                                                          'not-free-identifier=? #t))
                                 (lambda (stx) (tc-error/stx stx "The type of ~a cannot be converted to a contract" (syntax-e #'id)))))
                           (provide (rename-out [export-id out-id]))))])))]
         [(mem? internal-id stx-defs) 
@@ -76,7 +79,8 @@
                      (if (unbox typed-context?)
                          (begin
                            (add-alias #'export-id #'id)
-                           (make-rename-transformer #'id))
+                           (make-rename-transformer (syntax-property #'id 
+                                                                     'not-free-identifier=? #t)))
                          (lambda (stx)
                            (tc-error/stx stx "Macro ~a from typed module used in untyped code" (syntax-e #'out-id)))))
                    (provide (rename-out [export-id out-id]))))))]
diff --git a/collects/typed-scheme/typecheck/tc-app-unit.ss b/collects/typed-scheme/typecheck/tc-app-unit.ss
index dbe864f1..61b4f54b 100644
--- a/collects/typed-scheme/typecheck/tc-app-unit.ss
+++ b/collects/typed-scheme/typecheck/tc-app-unit.ss
@@ -342,6 +342,19 @@
                                              drest-bound
                                              (subst-all (alist-delete drest-bound substitution eq?)
                                                         (car rngs*)))))]
+               ;; ... function, (List A B C etc) arg
+               [(and (car drests*)
+                     (not tail-bound)
+                     (eq? (cdr (car drests*)) dotted-var)
+                     (= (length (car doms*))
+                        (length arg-tys))
+                     (untuple tail-ty)
+                     (infer/dots fixed-vars dotted-var (append arg-tys (untuple tail-ty)) (car doms*)
+                                 (car (car drests*)) (car rngs*) (fv (car rngs*))))
+                => (lambda (substitution) 
+                     (define drest-bound (cdr (car drests*)))
+                     (do-apply-log substitution 'dots 'dots)
+                     (ret (subst-all substitution (car rngs*))))]
                ;; if nothing matches, around the loop again
                [else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))]
     [(tc-result: (PolyDots: vars (Function: '())))
diff --git a/collects/typed-scheme/types/abbrev.ss b/collects/typed-scheme/types/abbrev.ss
index 9db1bd41..07e03627 100644
--- a/collects/typed-scheme/types/abbrev.ss
+++ b/collects/typed-scheme/types/abbrev.ss
@@ -96,6 +96,7 @@
 (define Err (make-Error))
 
 (define -Nat -Integer)
+(define -Real -Number)
 
 (define Any-Syntax
   (-mu x
diff --git a/collects/typed-scheme/utils/utils.ss b/collects/typed-scheme/utils/utils.ss
index 658c581b..a2503c86 100644
--- a/collects/typed-scheme/utils/utils.ss
+++ b/collects/typed-scheme/utils/utils.ss
@@ -20,7 +20,9 @@ at least theoretically.
          in-list-forever
          extend
          debug
-         in-syntax)
+         in-syntax
+	 symbol-append
+	 rep utils typecheck infer env private)
 
 (define-syntax (define-requirer stx)
   (syntax-parse stx