diff --git a/collects/typed-scheme/info.ss b/collects/typed-scheme/info.ss
index e245bb52..c18cc35e 100644
--- a/collects/typed-scheme/info.ss
+++ b/collects/typed-scheme/info.ss
@@ -1,4 +1,4 @@
 #lang setup/infotab
 
-(define scribblings '(("ts-reference.scrbl" ())
-		      ("ts-guide.scrbl" ())))
+(define scribblings '(("scribblings/ts-reference.scrbl" ())
+		      ("scribblings/ts-guide.scrbl" (multi-page))))
diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss
index e044a4c0..24d39f9d 100644
--- a/collects/typed-scheme/private/base-env.ss
+++ b/collects/typed-scheme/private/base-env.ss
@@ -641,6 +641,7 @@
 
 ;; unsafe
 
+[unsafe-vector-ref (-poly (a) ((-vec a) -Nat . -> . a))]
 [unsafe-vector-length (-poly (a) ((-vec a) . -> . -Nat))]
 [unsafe-car (-poly (a b) 
               (cl->*
@@ -649,6 +650,42 @@
               (cl->*
                (->acc (list (-pair a b)) b (list -cdr))))]
 
+[unsafe-fx+
+ (cl->
+  [(-Integer -Integer) -Integer]
+  [(-Nat -Nat) -Nat])]
+[unsafe-fx- (-Integer -Integer . -> . -Integer)]
+[unsafe-fx*
+ (cl->
+  [(-Integer -Integer) -Integer]
+  [(-Nat -Nat) -Nat])]
+[unsafe-fxquotient (-Integer -Integer . -> . -Integer)]
+[unsafe-fxremainder (-Integer -Integer . -> . -Integer)]
+[unsafe-fxmodulo (-Integer -Integer . -> . -Integer)]
+[unsafe-fxabs (-Integer . -> . -Nat)]
+
+[unsafe-fxand (-Integer -Integer . -> . -Integer)]
+[unsafe-fxior (-Integer -Integer . -> . -Integer)]
+[unsafe-fxxor (-Integer -Integer . -> . -Integer)]
+[unsafe-fxnot (-Integer . -> . -Integer)]
+[unsafe-fxlshift (-Integer -Integer . -> . -Integer)]
+[unsafe-fxrshift (-Integer -Integer . -> . -Integer)]
+
+[unsafe-fx= (-Integer -Integer . -> . -Boolean)]
+[unsafe-fx< (-Integer -Integer . -> . -Boolean)]
+[unsafe-fx> (-Integer -Integer . -> . -Boolean)]
+[unsafe-fx<= (-Integer -Integer . -> . -Boolean)]
+[unsafe-fx>= (-Integer -Integer . -> . -Boolean)]
+[unsafe-fxmin
+ (cl->
+  [(-Integer -Integer) -Integer]
+  [(-Nat -Nat) -Nat])]
+[unsafe-fxmax
+ (cl->
+  [(-Integer -Integer) -Integer]
+  [(-Nat -Nat) -Nat])]
+
+
 ;; scheme/vector
 [vector-count (-polydots (a b)
                          ((list
diff --git a/collects/typed-scheme/scribblings/begin.scrbl b/collects/typed-scheme/scribblings/begin.scrbl
new file mode 100644
index 00000000..7bc686a5
--- /dev/null
+++ b/collects/typed-scheme/scribblings/begin.scrbl
@@ -0,0 +1,132 @@
+#lang scribble/manual
+
+@begin[(require (for-label (only-meta-in 0 typed/scheme)) scribble/eval
+		"utils.ss" (only-in "quick.scrbl" typed-mod))]
+
+@(define the-eval (make-base-eval))
+@(the-eval '(require typed/scheme))
+
+@title[#:tag "beginning"]{Beginning Typed Scheme}
+
+Recall the typed module from @secref["quick"]:                 
+
+@|typed-mod|
+
+Let us consider each element of this program in turn.
+
+@schememod[typed/scheme]
+
+This specifies that the module is written in the
+@schememodname[typed/scheme] language, which is a typed version of the
+@schememodname[scheme] language.  Typed versions of other languages
+are provided as well; for example, the
+@schememodname[typed/scheme/base] language corresponds to
+@schememodname[scheme/base].   
+
+@schemeblock[(define-struct: pt ([x : Real] [y : Real]))]
+
+@margin-note{Many forms in Typed Scheme have the same name as the
+untyped forms, with a @scheme[:] suffix.}
+This defines a new structure, name @scheme[pt], with two fields,
+@scheme[x] and @scheme[y].  Both fields are specified to have the type
+@scheme[Real], which corresponds to the @rtech{real numbers}.
+ The
+@scheme[define-struct:] form corresponds to the @scheme[define-struct]
+form from @schememodname[scheme]---when porting a program from
+@schememodname[scheme] to @schememodname[typed/scheme], uses of
+@scheme[define-struct] should be changed to @scheme[define-struct:].
+
+@schemeblock[(: mag (pt -> Real))]
+
+This declares that @scheme[mag] has the type @scheme[(pt -> Real)].
+@;{@scheme[mag] must be defined at the top-level of the module containing
+the declaration.}
+
+The type @scheme[(pt -> Real)] is a function type, that is, the type
+of a procedure.  The input type, or domain, is a single argument of
+type @scheme[pt], which refers to an instance of the @scheme[pt]
+structure.  The @scheme[->] both indicates that this is a function
+type and separates the domain from  the range, or output type, in this
+case @scheme[Real].
+
+@schemeblock[
+(define (mag p)
+  (sqrt (sqr (pt-x p)) (sqr (pt-y p))))
+]
+
+This definition is unchanged from the untyped version of the code.
+The goal of Typed Scheme is to  allow almost all definitions to be
+typechecked without change.  The typechecker verifies that the body of
+the function has the type @scheme[Real], under the assumption that
+@scheme[p] has the type @scheme[pt], taking these types from the
+earlier type declaration.  Since the body does have this type, the
+program is accepted.
+
+
+@section{Datatypes and Unions}
+
+Many data structures involve multiple variants.  In Typed Scheme, we
+represent these using @italic{union types}, written @scheme[(U t1 t2 ...)].
+
+@schememod[
+typed/scheme
+(define-type-alias Tree (U leaf node))
+(define-struct: leaf ([val : Number]))
+(define-struct: node ([left : Tree] [right : Tree]))
+
+(: tree-height (Tree -> Number))
+(define (tree-height t)
+  (cond [(leaf? t) 1]
+        [else (max (+ 1 (tree-height (node-left t)))
+                   (+ 1 (tree-height (node-right t))))]))
+
+(: tree-sum (Tree -> Number))
+(define (tree-sum t)
+  (cond [(leaf? t) (leaf-val t)]
+        [else (+ (tree-sum (node-left t))
+                 (tree-sum (node-right t)))]))
+]
+
+In this module, we have defined two new datatypes: @scheme[leaf] and
+@scheme[node].  We've also defined the type alias @scheme[Tree] to be
+@scheme[(U node leaf)], which represents a binary tree of numbers.  In
+essence, we are saying that the @scheme[tree-height] function accepts
+a @scheme[Tree], which is either a @scheme[node] or a @scheme[leaf],
+and produces a number.
+
+In order to calculate interesting facts about trees, we have to take
+them apart and get at their contents.  But since accessors such as
+@scheme[node-left] require a @scheme[node] as input, not a
+@scheme[Tree], we have to determine which kind of input we
+were passed.  
+
+For this purpose, we use the predicates that come with each defined
+structure.  For example, the @scheme[leaf?] predicate distinguishes
+@scheme[leaf]s from all other Typed Scheme values.  Therefore, in the
+first branch of the @scheme[cond] clause in @scheme[tree-sum], we know
+that @scheme[t] is a @scheme[leaf], and therefore we can get its value
+with the @scheme[leaf-val] function.
+
+In the else clauses of both functions, we know that @scheme[t] is not
+a @scheme[leaf], and since the type of @scheme[t] was @scheme[Tree] by
+process of elimination we can determine that @scheme[t] must be a
+@scheme[node].  Therefore, we can use accessors such as
+@scheme[node-left] and @scheme[node-right] with @scheme[t] as input.
+
+
+@section{Type Errors}
+
+When Typed Scheme detects a type error in the module, it raises an
+error before running the program.  
+
+@examples[#:eval the-eval
+(add1 "not a number")
+]
+
+@;{
+Typed Scheme also attempts to detect more than one error in the module.
+
+@examples[#:eval the-eval
+(string-append "a string" (add1 "not a number"))
+]
+}
\ No newline at end of file
diff --git a/collects/typed-scheme/scribblings/more.scrbl b/collects/typed-scheme/scribblings/more.scrbl
new file mode 100644
index 00000000..998148c6
--- /dev/null
+++ b/collects/typed-scheme/scribblings/more.scrbl
@@ -0,0 +1,160 @@
+#lang scribble/manual
+
+@begin[(require "utils.ss"
+		scribble/core scribble/eval
+		(for-label (only-meta-in 0 typed/scheme) mzlib/etc))]
+
+@title[#:tag "more"]{Specifying Types}
+
+@(define the-eval (make-base-eval))
+@(the-eval '(require typed/scheme))
+
+
+The previous section introduced the basics of the Typed Scheme type
+system.  In this section, we will see several new features of the
+language, allowing types to be specified and used.
+
+@section{Type Annotation and Binding Forms}
+
+In general, variables in Typed Scheme must be annotated with their
+type.  
+
+@subsection{Annotating Definitions}
+
+We have already seen the @scheme[:] type annotation form.  This is
+useful for definitions, at both the top level of a module
+
+@schemeblock[
+(: x Number)
+(define x 7)]
+
+and in an internal definition
+
+@schemeblock[
+(let ()
+  (: x Number)
+  (define x 7)
+  (add1 x))
+]
+
+In addition to the @scheme[:] form, almost all binding forms from
+@schememodname[scheme] have counterparts which allow the specification
+of types. The @scheme[define:] form allows the definition of variables
+in both top-level and internal contexts.
+
+@schemeblock[
+(define: x : Number 7)
+(define: (id [z : Number]) z)]
+
+Here, @scheme[x] has the type @scheme[Number], and @scheme[id] has the
+type @scheme[(Number -> Number)].  In the body of @scheme[id],
+@scheme[z] has the type @scheme[Number]. 
+
+@subsection{Annotating Local Binding}
+
+@schemeblock[
+(let: ([x : Number 7])
+  (add1 x))
+]
+
+The @scheme[let:] form is exactly like @scheme[let], but type
+annotations are provided for each variable bound.  Here, @scheme[x] is
+given the type @scheme[Number].  The @scheme[let*:] and
+@scheme[letrec:] are similar.
+
+@schemeblock[
+(let-values: ([([x : Number] [y : String]) (values 7 "hello")])
+  (+ x (string-length y)))
+]
+
+The @scheme[let*-values:] and @scheme[letrec-values:] forms are similar.
+
+@subsection{Annotating Functions}
+
+Function expressions also bind variables, which can be annotated with
+types. This function expects two arguments, a @scheme[Number] and a
+@scheme[String]: 
+
+@schemeblock[(lambda: ([x : Number] [y : String]) (+ x 5))]
+
+This function accepts at least one @scheme[String], followed by
+arbitrarily many @scheme[Number]s.  In the body, @scheme[y] is a list
+of @scheme[Number]s.
+
+@schemeblock[(lambda: ([x : String] (unsyntax @tt["."]) [y : Number #,**]) (apply + y))]
+
+This function has the type @scheme[(String Number #,** -> Number)].
+Functions defined by cases may also be annotated:
+
+@schemeblock[(case-lambda: [() 0]
+			   [([x : Number]) x])]
+
+This function has the type 
+@scheme[(case-lambda (-> Number) (Number -> Number))].   
+
+@subsection{Annotating Single Variables}
+
+When a single variable binding needs annotation, the annotation can be
+applied to a single variable using a reader extension:
+
+@schemeblock[
+(let ([#,(annvar x Number) 7]) (add1 x))]
+
+This is equivalent to the earlier use of @scheme[let:]. This is
+especially useful for binding forms which do not have counterparts
+provided by Typed Scheme, such as @scheme[let+]:
+
+@schemeblock[
+(let+ ([val #,(annvar x Number) (+ 6 1)]) 
+  (* x x))]
+
+@subsection{Annotating Expressions}
+
+It is also possible to provide an expected type for a particular
+expression.   
+
+@schemeblock[(ann (+ 7 1) Number)]
+
+This ensures that the expression, here @scheme[(+ 7 1)], has the
+desired type, here @scheme[Number].  Otherwise, the type checker
+signals an error.  For example:
+
+@interaction[#:eval the-eval
+(ann "not a number" Number)]
+
+@section{Type Inference}
+
+In many cases, type annotations can be avoided where Typed Scheme can
+infer them.  For example, the types of all local bindings using
+@scheme[let] and @scheme[let*] can be inferred.
+
+@schemeblock[(let ([x 7]) (add1 x))]
+
+In this example, @scheme[x] has the type
+@scheme[Exact-Positive-Integer].  
+
+Similarly, top-level constant definitions do not require annotation:
+
+@schemeblock[(define y "foo")]
+
+In this examples, @scheme[y] has the type @scheme[String].
+
+Finally, the parameter types for loops are inferred from their initial
+values.  
+
+@schemeblock[
+(let loop ([x 0] [y (list 1 2 3)])
+  (if (null? y) x (loop (+ x (car y)) (cdr y))))]
+
+Here @scheme[x] has the inferred type @scheme[Integer], and @scheme[y]
+has the inferred type @scheme[(Listof Integer)].  The @scheme[loop]
+variable has type @scheme[(Integer (Listof Integer) -> Integer)].
+
+@section{New Type Names}
+
+Any type can be given a name with @scheme[define-type-alias].  
+
+@schemeblock[(define-type-alias NN (Number -> Number))]
+
+Anywhere the name @scheme[NN] is used, it is expanded to
+@scheme[(Number -> Number)].   Type aliases may not be recursive.
\ No newline at end of file
diff --git a/collects/typed-scheme/scribblings/quick.scrbl b/collects/typed-scheme/scribblings/quick.scrbl
new file mode 100644
index 00000000..a46bcc31
--- /dev/null
+++ b/collects/typed-scheme/scribblings/quick.scrbl
@@ -0,0 +1,48 @@
+#lang scribble/manual
+
+@(require "utils.ss" (for-label (only-meta-in 0 typed/scheme)))
+@(provide typed-mod)
+
+@title[#:tag "quick"]{Quick Start}
+
+Given a module written in the @schememodname[scheme] language, using
+Typed Scheme requires the following steps:
+
+@itemize[#:style 
+         'ordered
+         @item{Change the language to @schememodname[typed/scheme].}
+         @item{Change the uses of @scheme[(require mod)] to
+           @scheme[(require typed/mod)].} 
+         @item{Annotate structure definitions and top-level
+           definitions with their types.} ]
+
+Then, when the program is run, it will automatically be typechecked
+before any execution, and any type errors will be reported.  If there
+are any type errors, the program will not run.
+
+Here is an example program, written in the @schememodname[scheme]
+language:
+
+@(define typed-mod
+@schememod[
+typed/scheme
+(define-struct: pt ([x : Real] [y : Real]))
+
+(: mag (pt -> Real))
+(define (mag p)
+  (sqrt (sqr (pt-x p)) (sqr (pt-y p))))
+]
+)
+
+@schememod[
+scheme
+(define-struct pt (x y))
+
+(code:contract mag : pt -> number)
+(define (mag p)
+  (sqrt (sqr (pt-x p)) (sqr (pt-y p))))
+]
+
+Here is the same program, in @schememodname[typed/scheme]:
+
+@|typed-mod|
diff --git a/collects/typed-scheme/scribblings/ts-guide.scrbl b/collects/typed-scheme/scribblings/ts-guide.scrbl
new file mode 100644
index 00000000..1c160a26
--- /dev/null
+++ b/collects/typed-scheme/scribblings/ts-guide.scrbl
@@ -0,0 +1,299 @@
+#lang scribble/manual
+
+@begin[(require "utils.ss" (for-label (only-meta-in 0 typed/scheme)))]
+
+@title[#:tag "top"]{@bold{Typed Scheme}: Scheme with Static Types}
+
+@author["Sam Tobin-Hochstadt"]
+
+@section-index["typechecking" "typechecker" "typecheck"]
+
+Typed Scheme is a family of languages, each of which enforce
+that programs written in the language obey a type system that ensures
+the absence of many common errors.  This guide is intended for programmers familiar 
+with PLT Scheme.  For an introduction to PLT Scheme, see the @(other-manual '(lib "scribblings/guide/guide.scrbl")).
+
+@local-table-of-contents[]
+
+@include-section["quick.scrbl"]
+@include-section["begin.scrbl"]
+@include-section["more.scrbl"]
+@include-section["types.scrbl"]
+
+@;@section{How the Type System Works}
+
+@;@section{Integrating with Untyped Code}
+
+@;{
+@section{Starting with Typed Scheme}
+
+If you already know PLT Scheme, or even some other Scheme, it should be
+easy to start using Typed Scheme.
+
+@subsection{A First Function}
+
+The following program defines the Fibonacci function in PLT Scheme:
+
+@schememod[
+scheme
+(define (fib n)
+  (cond [(= 0 n) 1]
+	[(= 1 n) 1]
+	[else (+ (fib (- n 1)) (fib (- n 2)))]))
+]
+
+This program defines the same program using Typed Scheme.
+ 
+@schememod[
+typed-scheme
+(: fib (Number -> Number))
+(define (fib n)
+  (cond [(= 0 n) 1]
+        [(= 1 n) 1]
+        [else (+ (fib (- n 1)) (fib (- n 2)))]))
+]
+
+There are two differences between these programs:
+
+@itemize[
+  @item*[@elem{The Language}]{@schememodname[scheme] has been replaced by @schememodname[typed-scheme].}
+
+  @item*[@elem{The Type Annotation}]{We have added a type annotation
+for the @scheme[fib] function, using the @scheme[:] form.}  ]
+
+In general, these are most of the changes that have to be made to a
+PLT Scheme program to transform it into a Typed Scheme program.
+@margin-note{Changes to uses of @scheme[require] may also be necessary
+- these are described later.}
+
+@subsection[#:tag "complex"]{Adding more complexity}
+
+Other typed binding forms are also available.  For example, we could have
+rewritten our fibonacci program as follows:
+
+@schememod[
+typed-scheme
+(: fib (Number -> Number))
+(define (fib n)
+  (let ([base? (or (= 0 n) (= 1 n))])
+    (if base? 
+	1
+        (+ (fib (- n 1)) (fib (- n 2))))))
+]
+
+This program uses the @scheme[let] binding form, but no new type
+annotations are required.  Typed Scheme infers the type of
+@scheme[base?].  
+
+We can also define mutually-recursive functions:
+
+@schememod[
+typed-scheme
+(: my-odd? (Number -> Boolean))
+(define (my-odd? n)
+  (if (= 0 n) #f
+      (my-even? (- n 1))))
+
+(: my-even? (Number -> Boolean))
+(define (my-even? n)
+  (if (= 0 n) #t
+      (my-odd? (- n 1))))
+
+(my-even? 12)
+]
+
+As expected, this program prints @schemeresult[#t].
+
+
+@subsection{Defining New Datatypes}
+
+If our program requires anything more than atomic data, we must define
+new datatypes.  In Typed Scheme, structures can be defined, similarly
+to PLT Scheme structures.  The following program defines a date
+structure and a function that formats a date as a string, using PLT
+Scheme's built-in @scheme[format] function.
+
+@schememod[
+typed-scheme
+(define-struct: Date ([day : Number] [month : String] [year : Number]))
+
+(: format-date (Date -> String))
+(define (format-date d)
+  (format "Today is day ~a of ~a in the year ~a" 
+          (Date-day d) (Date-month d) (Date-year d)))
+
+(format-date (make-Date 28 "November" 2006))
+]
+
+Here we see the built-in type @scheme[String] as well as a definition
+of the new user-defined type @scheme[Date].  To define
+@scheme[Date], we provide all the information usually found in a
+@scheme[define-struct], but added type annotations to the fields using
+the @scheme[define-struct:] form.
+Then we can use the functions that this declaration creates, just as
+we would have with @scheme[define-struct].  
+
+
+@subsection{Recursive Datatypes and Unions}
+
+Many data structures involve multiple variants.  In Typed Scheme, we
+represent these using @italic{union types}, written @scheme[(U t1 t2 ...)].
+
+@schememod[
+typed-scheme
+(define-type-alias Tree (U leaf node))
+(define-struct: leaf ([val : Number]))
+(define-struct: node ([left : Tree] [right : Tree]))
+
+(: tree-height (Tree -> Number))
+(define (tree-height t)
+  (cond [(leaf? t) 1]
+        [else (max (+ 1 (tree-height (node-left t)))
+                   (+ 1 (tree-height (node-right t))))]))
+
+(: tree-sum (Tree -> Number))
+(define (tree-sum t)
+  (cond [(leaf? t) (leaf-val t)]
+        [else (+ (tree-sum (node-left t))
+                 (tree-sum (node-right t)))]))
+]
+
+In this module, we have defined two new datatypes: @scheme[leaf] and
+@scheme[node].  We've also defined the type alias @scheme[Tree] to be
+@scheme[(U node leaf)], which represents a binary tree of numbers.  In
+essence, we are saying that the @scheme[tree-height] function accepts
+a @scheme[Tree], which is either a @scheme[node] or a @scheme[leaf],
+and produces a number.
+
+In order to calculate interesting facts about trees, we have to take
+them apart and get at their contents.  But since accessors such as
+@scheme[node-left] require a @scheme[node] as input, not a
+@scheme[Tree], we have to determine which kind of input we
+were passed.  
+
+For this purpose, we use the predicates that come with each defined
+structure.  For example, the @scheme[leaf?] predicate distinguishes
+@scheme[leaf]s from all other Typed Scheme values.  Therefore, in the
+first branch of the @scheme[cond] clause in @scheme[tree-sum], we know
+that @scheme[t] is a @scheme[leaf], and therefore we can get its value
+with the @scheme[leaf-val] function.
+
+In the else clauses of both functions, we know that @scheme[t] is not
+a @scheme[leaf], and since the type of @scheme[t] was @scheme[Tree] by
+process of elimination we can determine that @scheme[t] must be a
+@scheme[node].  Therefore, we can use accessors such as
+@scheme[node-left] and @scheme[node-right] with @scheme[t] as input.
+
+@section[#:tag "poly"]{Polymorphism}
+
+Typed Scheme offers abstraction over types as well as values.
+
+@subsection{Polymorphic Data Structures}
+
+Virtually every Scheme program uses lists and sexpressions.  Fortunately, Typed
+Scheme can handle these as well.  A simple list processing program can be
+written like this:
+
+@schememod[
+typed-scheme
+(: sum-list ((Listof Number) -> Number))
+(define (sum-list l)
+  (cond [(null? l) 0]
+        [else (+ (car l) (sum-list (cdr l)))]))
+]
+
+This looks similar to our earlier programs --- except for the type
+of @scheme[l], which looks like a function application.  In fact, it's
+a use of the @italic{type constructor} @scheme[Listof], which takes
+another type as its input, here @scheme[Number].  We can use
+@scheme[Listof] to construct the type of any kind of list we might
+want.  
+
+We can define our own type constructors as well.  For example, here is
+an analog of the @tt{Maybe} type constructor from Haskell:
+
+@schememod[
+typed-scheme
+(define-struct: Nothing ())
+(define-struct: (a) Just ([v : a]))
+
+(define-type-alias (Maybe a) (U Nothing (Just a)))
+
+(: find (Number (Listof Number) -> (Maybe Number)))
+(define (find v l)
+  (cond [(null? l) (make-Nothing)]
+        [(= v (car l)) (make-Just v)]
+        [else (find v (cdr l))]))
+]
+
+The first @scheme[define-struct:] defines @scheme[Nothing] to be
+a structure with no contents.  
+
+The second definition
+
+@schemeblock[
+(define-struct: (a) Just ([v : a]))
+]
+
+creates a parameterized type, @scheme[Just], which is a structure with
+one element, whose type is that of the type argument to
+@scheme[Just].  Here the type parameters (only one, @scheme[a], in
+this case) are written before the type name, and can be referred to in
+the types of the fields.
+
+The type alias definiton
+@schemeblock[
+  (define-type-alias (Maybe a) (U Nothing (Just a)))
+]
+creates a parameterized alias --- @scheme[Maybe] is a potential
+container for whatever type is supplied.
+
+The @scheme[find] function takes a number @scheme[v] and list, and
+produces @scheme[(make-Just v)] when the number is found in the list,
+and @scheme[(make-Nothing)] otherwise.  Therefore, it produces a
+@scheme[(Maybe Number)], just as the annotation specified.  
+
+@subsection{Polymorphic Functions}
+
+Sometimes functions over polymorphic data structures only concern
+themselves with the form of the structure.  For example, one might
+write a function that takes the length of a list of numbers:
+
+@schememod[
+typed-scheme
+(: list-number-length ((Listof Number) -> Integer))
+(define (list-number-length l)
+  (if (null? l)
+      0
+      (add1 (list-number-length (cdr l)))))]
+
+and also a function that takes the length of a list of strings:
+
+@schememod[
+typed-scheme
+(: list-string-length ((Listof String) -> Integer))
+(define (list-string-length l)
+  (if (null? l)
+      0
+      (add1 (list-string-length (cdr l)))))]
+
+Notice that both of these functions have almost exactly the same
+definition; the only difference is the name of the function.  This
+is because neither function uses the type of the elements in the
+definition.
+
+We can abstract over the type of the element as follows:
+
+@schememod[
+typed-scheme
+(: list-length (All (A) ((Listof A) -> Integer)))
+(define (list-length l)
+  (if (null? l)
+      0
+      (add1 (list-length (cdr l)))))]
+
+The new type constructor @scheme[All] takes a list of type
+variables and a body type.  The type variables are allowed to
+appear free in the body of the @scheme[All] form.
+
+}
\ No newline at end of file
diff --git a/collects/typed-scheme/scribblings/ts-reference.scrbl b/collects/typed-scheme/scribblings/ts-reference.scrbl
new file mode 100644
index 00000000..6387cf56
--- /dev/null
+++ b/collects/typed-scheme/scribblings/ts-reference.scrbl
@@ -0,0 +1,332 @@
+#lang scribble/manual
+
+@begin[(require "utils.ss" scribble/eval
+                scheme/sandbox)
+       (require (for-label (only-meta-in 0 typed/scheme)
+                           scheme/list srfi/14
+                           version/check))]
+
+
+@title[#:tag "top"]{The Typed Scheme Reference} 
+
+@author["Sam Tobin-Hochstadt"]
+
+@(defmodulelang* (typed/scheme/base typed/scheme)
+                 #:use-sources (typed-scheme/typed-scheme typed-scheme/private/prims))
+
+@section[#:tag "type-ref"]{Type Reference}
+
+@subsubsub*section{Base Types}
+@deftogether[(
+@defidform[Number]
+@defidform[Real]
+@defidform[Integer]
+@defidform[Natural]
+@defidform[Exact-Positive-Integer]
+@defidform[Boolean]
+@defidform[True]
+@defidform[False]
+@defidform[String]
+@defidform[Keyword]
+@defidform[Symbol]
+@defidform[Void]
+@defidform[Input-Port]
+@defidform[Output-Port]
+@defidform[Path]
+@defidform[Regexp]
+@defidform[PRegexp]
+@defidform[Syntax]
+@defidform[Identifier]
+@defidform[Bytes]
+@defidform[Namespace]
+@defidform[EOF]
+@defidform[Continuation-Mark-Set]
+@defidform[Char])]{
+These types represent primitive Scheme data.  Note that @scheme[Integer] represents exact integers.}
+
+@defidform[Any]{Any Scheme value. All other types are subtypes of @scheme[Any].}
+
+@defidform[Nothing]{The empty type.  No values inhabit this type, and
+any expression of this type will not evaluate to a value.}
+
+
+The following base types are parameteric in their type arguments.
+
+@defform[(Listof t)]{Homogenous @rtech{lists} of @scheme[t]}
+@defform[(Boxof t)]{A @rtech{box} of @scheme[t]}
+@defform[(Syntaxof t)]{A @rtech{syntax object} containing a @scheme[t]}
+@defform[(Vectorof t)]{Homogenous @rtech{vectors} of @scheme[t]}
+@defform[(Option t)]{Either @scheme[t] of @scheme[#f]}
+@defform*[[(Parameter t)
+           (Parameter s t)]]{A @rtech{parameter} of @scheme[t].  If two type arguments are supplied, 
+                               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}
+
+@defform*[#:id -> #:literals (* ...)
+	       [(dom ... -> rng)
+	        (dom ... rest * -> rng)
+		(dom ... rest ... bound -> rng)
+                (dom -> rng : pred)]]{is the type of functions from the (possibly-empty)
+  sequence @scheme[dom ...] to the @scheme[rng] type.  The second form
+  specifies a uniform rest argument of type @scheme[rest], and the
+  third form specifies a non-uniform rest argument of type
+  @scheme[rest] with bound @scheme[bound].  In the third form, the
+  second occurrence of @scheme[...] is literal, and @scheme[bound]
+  must be an identifier denoting a type variable. In the fourth form, 
+  there must be only one @scheme[dom] and @scheme[pred] is the type 
+  checked by the predicate.}
+@defform[(U t ...)]{is the union of the types @scheme[t ...]}
+@defform[(case-lambda fun-ty ...)]{is a function that behaves like all of
+  the @scheme[fun-ty]s.  The @scheme[fun-ty]s must all be function
+  types constructed with @scheme[->].}
+@defform/none[(t t1 t2 ...)]{is the instantiation of the parametric type
+  @scheme[t] at types @scheme[t1 t2 ...]}
+@defform[(All (v ...) t)]{is a parameterization of type @scheme[t], with
+  type variables @scheme[v ...]}
+@defform[(List t ...)]{is the type of the list with one element, in order, 
+  for each type provided to the @scheme[List] type constructor.}
+@defform[(values t ...)]{is the type of a sequence of multiple values, with
+types @scheme[t ...].  This can only appear as the return type of a
+function.}
+@defform/none[v]{where @scheme[v] is a number, boolean or string, is the singleton type containing only that value}
+@defform/none[(quote val)]{where @scheme[val] is a Scheme value, is the singleton type containing only that value}
+@defform/none[i]{where @scheme[i] is an identifier can be a reference to a type
+name or a type variable}
+@defform[(Rec n t)]{is a recursive type where @scheme[n] is bound to the
+recursive type in the body @scheme[t]}
+
+Other types cannot be written by the programmer, but are used
+internally and may appear in error messages.
+
+@defform/none[(struct:n (t ...))]{is the type of structures named
+@scheme[n] with field types @scheme[t].  There may be multiple such
+types with the same printed representation.}
+@defform/none[<n>]{is the printed representation of a reference to the
+type variable @scheme[n]}
+
+@section[#:tag "special-forms"]{Special Form Reference}
+
+Typed Scheme provides a variety of special forms above and beyond
+those in PLT Scheme.  They are used for annotating variables with types,
+creating new types, and annotating expressions.
+
+@subsection{Binding Forms}
+
+@scheme[_loop], @scheme[_f], @scheme[_a], and @scheme[_v] are names, @scheme[_t] is a type.
+ @scheme[_e] is an expression and @scheme[_body] is a block.
+
+@defform*[[
+  (let: ([v : t e] ...) . body)
+  (let: loop : t0 ([v : t e] ...) . body)]]{
+Local bindings, like @scheme[let], each with
+associated types.  In the second form, @scheme[_t0] is the type of the
+result of @scheme[_loop] (and thus the result of the entire
+			      expression as well as the final
+				expression in @scheme[body]).}
+@deftogether[[
+@defform[(letrec: ([v : t e] ...) . body)]
+@defform[(let*: ([v : t e] ...) . body)]
+@defform[(let-values: ([([v : t] ...) e] ...) . body)]
+@defform[(letrec-values: ([([v : t] ...) e] ...) . body)]
+@defform[(let*-values: ([([v : t] ...) e] ...) . body)]]]{
+Type-annotated versions of
+@scheme[letrec], @scheme[let*], @scheme[let-values],
+  @scheme[letrec-values], and @scheme[let*-values].}  
+
+@deftogether[[
+@defform[(let/cc: v : t . body)]
+@defform[(let/ec: v : t . body)]]]{Type-annotated versions of
+@scheme[let/cc] and @scheme[let/ec].}
+
+@subsection{Anonymous Functions}
+
+@defform/subs[(lambda: formals . body)
+([formals ([v : t] ...) 
+	  ([v : t] ... . [v : t])])]{
+A function of the formal arguments @scheme[v], where each formal
+argument has the associated type.  If a rest argument is present, then
+it has type @scheme[(Listof t)].}
+@defform[(λ: formals . body)]{
+An alias for the same form using @scheme[lambda:].}
+@defform[(plambda: (a ...) formals . body)]{
+A polymorphic function, abstracted over the type variables
+@scheme[a]. The type variables @scheme[a] are bound in both the types
+of the formal, and in any type expressions in the @scheme[body].}
+@defform[(case-lambda: [formals body] ...)]{
+A function of multiple arities.  Note that each @scheme[formals] must have a
+different arity.}
+@defform[(pcase-lambda: (a ...) [formals body] ...)]{
+A polymorphic function of multiple arities.}
+
+@subsection{Loops}
+
+@defform/subs[(do: : u ([id : t init-expr step-expr-maybe] ...)
+                       (stop?-expr finish-expr ...)
+                expr ...+)
+              ([step-expr-maybe code:blank
+                                step-expr])]{
+Like @scheme[do], but each @scheme[id] having the associated type @scheme[t], and 
+the final body @scheme[expr] having the type @scheme[u].
+}
+
+
+@subsection{Definitions}
+
+@defform*[[(define: v : t e)
+	   (define: (f . formals) : t . body)	   
+	   (define: (a ...) (f . formals) : t . body)]]{
+These forms define variables, with annotated types.  The first form
+defines @scheme[v] with type @scheme[t] and value @scheme[e].  The
+second and third forms defines a function @scheme[f] with appropriate
+types.  In most cases, use of @scheme[:] is preferred to use of @scheme[define:].}
+
+
+
+@subsection{Structure Definitions}
+@defform/subs[
+(define-struct: maybe-type-vars name-spec ([f : t] ...))
+([maybe-type-vars code:blank (v ...)]
+ [name-spec name (name parent)])]{
+ Defines a @rtech{structure} with the name @scheme[name], where the
+ fields @scheme[f] have types @scheme[t].  When @scheme[parent], the
+structure is a substructure of @scheme[parent].  When
+@scheme[maybe-type-vars] is present, the structure is polymorphic in the type
+ variables @scheme[v].}
+                                 
+@defform/subs[
+(define-struct/exec: name-spec ([f : t] ...) [e : proc-t])
+([name-spec name (name parent)])]{
+ Like @scheme[define-struct:], but defines an procedural structure.  
+ The procdure @scheme[e] is used as the value for @scheme[prop:procedure], and must have type @scheme[proc-t].}
+
+@subsection{Type Aliases}
+@defform*[[(define-type-alias name t)
+	   (define-type-alias (name v ...) t)]]{
+The first form defines @scheme[name] as type, with the same meaning as
+@scheme[t].  The second form is equivalent to
+@scheme[(define-type-alias name (All (v ...) t))].  Type aliases may
+refer to other type aliases or types defined in the same module, but
+cycles among type aliases are prohibited.}
+
+
+@subsection{Type Annotation and Instantiation}
+
+@defform[(: v t)]{This declares that @scheme[v] has type @scheme[t].
+The definition of @scheme[v] must appear after this declaration.  This
+can be used anywhere a definition form may be used.}
+
+@defform[(provide: [v t] ...)]{This declares that the @scheme[v]s have
+the types @scheme[t], and also provides all of the @scheme[v]s.}
+
+@litchar{#{v : t}} This declares that the variable @scheme[v] has type
+@scheme[t].  This is legal only for binding occurences of @scheme[_v].
+
+@defform[(ann e t)]{Ensure that @scheme[e] has type @scheme[t], or
+some subtype.  The entire expression has type @scheme[t].
+This is legal only in expression contexts.}
+
+@litchar{#{e :: t}} This is identical to @scheme[(ann e t)].
+
+@defform[(inst e t ...)]{Instantiate the type of @scheme[e] with types
+@scheme[t ...].  @scheme[e] must have a polymorphic type with the
+appropriate number of type variables. This is legal only in expression
+contexts.}
+
+@litchar|{#{e @ t ...}}| This is identical to @scheme[(inst e t ...)].
+
+@subsection{Require}
+
+Here, @scheme[_m] is a module spec, @scheme[_pred] is an identifier
+naming a predicate, and @scheme[_r] is an optionally-renamed identifier.
+
+@defform/subs[#:literals (struct opaque)
+(require/typed m rt-clause ...)
+([rt-clause [r t]
+	    [struct name ([f : t] ...)]
+	    [struct (name parent) ([f : t] ...)]
+	    [opaque t pred]])
+]{This form requires identifiers from the module @scheme[m], giving
+them the specified types.   
+
+The first form requires @scheme[r], giving it type @scheme[t].
+
+@index["struct"]{The second and third forms} require the struct with name @scheme[name]
+with fields @scheme[f ...], where each field has type @scheme[t].  The
+third form allows a @scheme[parent] structure type to be specified.
+The parent type must already be a structure type known to Typed
+Scheme, either built-in or via @scheme[require/typed].  The
+structure predicate has the appropriate Typed Scheme filter type so
+that it may be used as a predicate in @scheme[if] expressions in Typed
+Scheme.
+
+@index["opaque"]{The fourth case} defines a new type @scheme[t].  @scheme[pred], imported from
+module @scheme[m], is a predicate for this type.  The type is defined
+as precisely those values to which @scheme[pred] produces
+@scheme[#t].  @scheme[pred] must have type @scheme[(Any -> Boolean)].  
+Opaque types must be required lexically before they are used.
+
+In all cases, the identifiers are protected with @rtech{contracts} which
+enforce the specified types.  If this contract fails, the module
+@scheme[m] is blamed. 
+
+Some types, notably polymorphic types constructed with @scheme[All],
+cannot be converted to contracts and raise a static error when used in
+a @scheme[require/typed] form.}
+
+@section{Libraries Provided With Typed Scheme}
+
+The @schememodname[typed/scheme] language corresponds to the
+@schememodname[scheme] language---that is, any identifier provided
+by @schememodname[scheme], such as @scheme[modulo] is available by default in
+@schememodname[typed/scheme].  
+
+@schememod[typed/scheme
+(modulo 12 2)
+]
+
+The @schememodname[typed/scheme/base] language corresponds to the
+@schememodname[scheme/base] language.
+
+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)
+]
+
+@section{Typed Scheme Syntax Without Type Checking}
+
+@defmodulelang[typed-scheme/no-check]
+
+On occasions where the Typed Scheme syntax is useful, but actual
+typechecking is not desired, the @schememodname[typed-scheme/no-check]
+language is useful.  It provides the same bindings and syntax as Typed
+Scheme, but does no type checking.
+
+Examples:
+
+@schememod[typed-scheme/no-check
+(: x Number)
+(define x "not-a-number")]
diff --git a/collects/typed-scheme/scribblings/types.scrbl b/collects/typed-scheme/scribblings/types.scrbl
new file mode 100644
index 00000000..bb22b878
--- /dev/null
+++ b/collects/typed-scheme/scribblings/types.scrbl
@@ -0,0 +1,260 @@
+#lang scribble/manual
+
+@begin[(require "utils.ss"
+		scribble/core scribble/eval
+		(for-label (only-meta-in 0 typed/scheme) mzlib/etc))]
+
+@(define the-eval (make-base-eval))
+@(the-eval '(require typed/scheme))
+
+@title[#:tag "types"]{Types in Typed Scheme}
+
+Typed Scheme provides a rich variety of types to describe data. This
+section introduces them.  
+
+@section{Basic Types}
+
+The most basic types in Typed Scheme are those for primitive data,
+such as @scheme[True] and @scheme[False] for booleans, @scheme[String]
+for strings, and @scheme[Char] for characters.
+
+@interaction[#:eval the-eval
+'"hello, world"
+#\f
+#t
+#f]
+
+Each symbol is given a unique type containing only that symbol.  The
+@scheme[Symbol] type includes all symbols.
+
+@interaction[#:eval the-eval
+'foo
+'bar]
+
+Typed Scheme also provides a rich hierarchy for describing particular
+kinds of numbers.
+
+@interaction[#:eval the-eval
+0
+-7
+14
+3.2
+7+2.8i]
+
+Finally, any value is itself a type:
+
+@interaction[#:eval the-eval
+(ann 23 : 23)]
+
+@section{Function Types}
+
+We have already seen some examples of function types.  Function types
+are constructed using @scheme[->], with the argument types before the
+arrow and the result type after.  Here are some example function
+types:
+
+@schemeblock[
+(Number -> Number)
+(String String -> Boolean)
+(Char -> (values String Natural))
+]
+
+The first type requires a @scheme[Number] as input, and produces a
+@scheme[Number].  The second requires two arguments.  The third takes
+one argument, and produces  @rtech{multiple values}, of types
+@scheme[String] and @scheme[Natural].  Here are example functions for
+each of these types.
+
+@interaction[#:eval the-eval
+(lambda: ([x : Number]) x)
+(lambda: ([a : String] [b : String]) (equal? a b))
+(lambda: ([c : Char]) (values (string c) (char->integer c)))]
+
+
+@section{Union Types}
+
+Sometimes a value can be one of several types.  To specify this, we
+can use a union type, written with the type constructor @scheme[U].  
+
+@interaction[#:eval the-eval
+(let ([a-number 37])
+  (if (even? a-number)
+      'yes
+      'no))]
+
+Any number of types can be combined together in a union, and nested
+unions are flattened.  
+
+@schemeblock[(U Number String Boolean Char)]
+
+@section{Recursive Types}
+
+@deftech{Recursive types} can refer to themselves.  This allows a type
+to describe an infinite family of data.  For example, this is the type
+of binary trees of numbers.  
+
+@schemeblock[
+(Rec BT (U Number (Pair BT BT)))]
+
+The @scheme[Rec] type constructor specifies that the type @scheme[BT]
+refers to the whole binary tree type within the body of the
+@scheme[Rec] form.
+
+@section{Structure Types}
+
+Using @scheme[define-struct:] introduces new types, distinct from any
+previous type.    
+
+@schemeblock[(define-struct: point ([x : Real] [y : Real]))]
+
+Instances of this structure, such as @scheme[(make-point 7 12)], have type @scheme[point].
+
+@section{Subtyping}
+
+In Typed Scheme, all types are placed in a hierarchy, based on what
+values are included in the type.  When an element of a larger type is
+expected, an element of a smaller type may be provided.  The smaller
+type is called a @deftech{subtype} of the larger type.  The larger
+type is called a @deftech{supertype}. For example,
+@scheme[Integer] is a subtype of @scheme[Real], since every integer is
+a real number.  Therefore, the following code is acceptable to the
+type checker:
+
+@schemeblock[
+(: f (Real -> Real))
+(define (f x) (* x 0.75))
+
+(: x Integer)
+(define x -125)
+
+(f x)
+]
+
+All types are subtypes of the @scheme[Any] type.
+
+The elements of a union type are individually subtypes of the whole
+union, so @scheme[String] is a subtype of @scheme[(U String Number)].
+One function type is a subtype of another if they have the same number
+of arguments, the subtype's arguments are more permissive (is a supertype), and the
+subtype's result type is less permissive (is a subtype).
+For example, @scheme[(Any -> String)] is a subtype of @scheme[(Number
+-> (U String #f))].
+
+@;@section{Occurrence Typing}
+
+@section{Polymorphism}
+
+Typed Scheme offers abstraction over types as well as values.
+
+@subsection{Polymorphic Data Structures}
+
+Virtually every Scheme program uses lists and sexpressions.  Fortunately, Typed
+Scheme can handle these as well.  A simple list processing program can be
+written like this:
+
+@schememod[
+typed/scheme
+(: sum-list ((Listof Number) -> Number))
+(define (sum-list l)
+  (cond [(null? l) 0]
+        [else (+ (car l) (sum-list (cdr l)))]))
+]
+
+This looks similar to our earlier programs --- except for the type
+of @scheme[l], which looks like a function application.  In fact, it's
+a use of the @italic{type constructor} @scheme[Listof], which takes
+another type as its input, here @scheme[Number].  We can use
+@scheme[Listof] to construct the type of any kind of list we might
+want.  
+
+We can define our own type constructors as well.  For example, here is
+an analog of the @tt{Maybe} type constructor from Haskell:
+
+@schememod[
+typed/scheme
+(define-struct: None ())
+(define-struct: (a) Some ([v : a]))
+
+(define-type-alias (Opt a) (U None (Some a)))
+
+(: find (Number (Listof Number) -> (Opt Number)))
+(define (find v l)
+  (cond [(null? l) (make-None)]
+        [(= v (car l)) (make-Some v)]
+        [else (find v (cdr l))]))
+]
+
+The first @scheme[define-struct:] defines @scheme[None] to be
+a structure with no contents.  
+
+The second definition
+
+@schemeblock[
+(define-struct: (a) Some ([v : a]))
+]
+
+creates a parameterized type, @scheme[Just], which is a structure with
+one element, whose type is that of the type argument to
+@scheme[Just].  Here the type parameters (only one, @scheme[a], in
+this case) are written before the type name, and can be referred to in
+the types of the fields.
+
+The type alias definiton
+@schemeblock[
+  (define-type-alias (Opt a) (U None (Some a)))
+]
+creates a parameterized alias --- @scheme[Opt] is a potential
+container for whatever type is supplied.
+
+The @scheme[find] function takes a number @scheme[v] and list, and
+produces @scheme[(make-Some v)] when the number is found in the list,
+and @scheme[(make-None)] otherwise.  Therefore, it produces a
+@scheme[(Opt Number)], just as the annotation specified.  
+
+@subsection{Polymorphic Functions}
+
+Sometimes functions over polymorphic data structures only concern
+themselves with the form of the structure.  For example, one might
+write a function that takes the length of a list of numbers:
+
+@schememod[
+typed/scheme
+(: list-number-length ((Listof Number) -> Integer))
+(define (list-number-length l)
+  (if (null? l)
+      0
+      (add1 (list-number-length (cdr l)))))]
+
+and also a function that takes the length of a list of strings:
+
+@schememod[
+typed/scheme
+(: list-string-length ((Listof String) -> Integer))
+(define (list-string-length l)
+  (if (null? l)
+      0
+      (add1 (list-string-length (cdr l)))))]
+
+Notice that both of these functions have almost exactly the same
+definition; the only difference is the name of the function.  This
+is because neither function uses the type of the elements in the
+definition.
+
+We can abstract over the type of the element as follows:
+
+@schememod[
+typed/scheme
+(: list-length (All (A) ((Listof A) -> Integer)))
+(define (list-length l)
+  (if (null? l)
+      0
+      (add1 (list-length (cdr l)))))]
+
+The new type constructor @scheme[All] takes a list of type
+variables and a body type.  The type variables are allowed to
+appear free in the body of the @scheme[All] form.
+
+
+@include-section["varargs.scrbl"]
+
+@;@section{Refinement Types}
diff --git a/collects/typed-scheme/scribblings/utils.ss b/collects/typed-scheme/scribblings/utils.ss
new file mode 100644
index 00000000..885f82c6
--- /dev/null
+++ b/collects/typed-scheme/scribblings/utils.ss
@@ -0,0 +1,23 @@
+#lang at-exp scheme
+
+(require scribble/manual scribble/core)
+(provide (all-defined-out))
+
+(define (item* header . args) (apply item @bold[header]{: } args))
+(define-syntax-rule (tmod forms ...) (schememod typed-scheme forms ...))
+(define (gtech . x)
+  (apply tech x #:doc '(lib "scribblings/guide/guide.scrbl")))
+(define (rtech . x)
+  (apply tech x #:doc '(lib "scribblings/reference/reference.scrbl")))
+
+(define ** (let ([* #f]) @scheme[*]))
+
+(define-syntax-rule (annvar x t)
+  (make-element #f (list @schemeparenfont["#{"]
+			 @scheme[x : t]
+			 @schemeparenfont["}"])))
+
+(define-syntax-rule (annexpr x t)
+  (make-element #f (list @schemeparenfont["#{"]
+			 @scheme[x :: t]
+			 @schemeparenfont["}"])))
diff --git a/collects/typed-scheme/scribblings/varargs.scrbl b/collects/typed-scheme/scribblings/varargs.scrbl
new file mode 100644
index 00000000..61b52b65
--- /dev/null
+++ b/collects/typed-scheme/scribblings/varargs.scrbl
@@ -0,0 +1,105 @@
+#lang scribble/manual
+
+@begin[(require "utils.ss" (for-label typed/scheme/base))]
+
+@title[#:tag "varargs"]{Variable-Arity Functions: Programming with Rest Arguments}
+
+Typed Scheme can handle some uses of rest arguments.
+
+@section{Uniform Variable-Arity Functions}
+
+In Scheme, one can write a function that takes an arbitrary
+number of arguments as follows:
+
+@schememod[
+scheme
+(define (sum . xs)
+  (if (null? xs)
+      0
+      (+ (car xs) (apply sum (cdr xs)))))
+
+(sum)
+(sum 1 2 3 4)
+(sum 1 3)]
+
+The arguments to the function that are in excess to the
+non-rest arguments are converted to a list which is assigned
+to the rest parameter.  So the examples above evaluate to
+@schemeresult[0], @schemeresult[10], and @schemeresult[4].
+
+We can define such functions in Typed Scheme as well:
+
+@schememod[
+typed/scheme
+(: sum (Number * -> Number))
+(define (sum . xs)
+  (if (null? xs)
+      0
+      (+ (car xs) (apply sum (cdr xs)))))]
+
+This type can be assigned to the function when each element
+of the rest parameter is used at the same type.
+
+@section{Non-Uniform Variable-Arity Functions}
+
+However, the rest argument may be used as a heterogeneous list.
+Take this (simplified) definition of the Scheme function @scheme[map]:
+
+@schememod[
+scheme
+(define (map f as . bss)
+  (if (or (null? as)
+          (ormap null? bss))
+      null
+      (cons (apply f (car as) (map car bss))
+            (apply map f (cdr as) (map cdr bss)))))
+
+(map add1 (list 1 2 3 4))
+(map cons (list 1 2 3) (list (list 4) (list 5) (list 6)))
+(map + (list 1 2 3) (list 2 3 4) (list 3 4 5) (list 4 5 6))]
+
+Here the different lists that make up the rest argument @scheme[bss]
+can be of different types, but the type of each list in @scheme[bss]
+corresponds to the type of the corresponding argument of @scheme[f].
+We also know that, in order to avoid arity errors, the length of
+@scheme[bss] must be one less than the arity of @scheme[f] (as
+@scheme[as] corresponds to the first argument of @scheme[f]).
+                                                            
+The example uses of @scheme[map] evaluate to @schemeresult[(list 2 3 4 5)],
+@schemeresult[(list (list 1 4) (list 2 5) (list 3 6))], and
+@schemeresult[(list 10 14 18)].
+
+In Typed Scheme, we can define @scheme[map] as follows:
+
+@schememod[
+typed/scheme
+(: map 
+   (All (C A B ...)
+        ((A B ... B -> C) (Listof A) (Listof B) ... B
+         ->
+         (Listof C))))
+(define (map f as . bss)
+  (if (or (null? as)
+          (ormap null? bss))
+      null
+      (cons (apply f (car as) (map car bss))
+            (apply map f (cdr as) (map cdr bss)))))]
+
+Note that the type variable @scheme[B] is followed by an
+ellipsis.  This denotes that B is a dotted type variable
+which corresponds to a list of types, much as a rest
+argument corresponds to a list of values.  When the type
+of @scheme[map] is instantiated at a list of types, then
+each type @scheme[t] which is bound by @scheme[B] (notated by
+the dotted pre-type @scheme[t ... B]) is expanded to a number
+of copies of @scheme[t] equal to the length of the sequence
+assigned to @scheme[B].  Then @scheme[B] in each copy is
+replaced with the corresponding type from the sequence.
+
+So the type of @scheme[(inst map Integer Boolean String Number)]
+is
+
+@scheme[((Boolean String Number -> Integer)
+         (Listof Boolean) (Listof String) (Listof Number)
+         ->
+         (Listof Integer))].