diff --git a/app/CliOptions.hs b/app/CliOptions.hs
--- a/app/CliOptions.hs
+++ b/app/CliOptions.hs
@@ -29,13 +29,18 @@
 
 cliParser :: Parser CliOptions
 cliParser = CliOptions 
-  <$> flag Untyped SystemF language
+  <$> language
   <*> switch version
-  where language = long "system-f"
-          <> short 'f'
-          <> internal -- this is a secret feature
-          <> help "Use the System F interpreter"
+  where language = flag' SystemF systemF <|> flag Untyped Untyped untyped
 
         version = long "version"
           <> short 'v'
           <> help "Print the version"
+
+        systemF = long "system-f"
+          <> short 'f'
+          <> help "Use the System F interpreter"
+
+        untyped = long "untyped"
+          <> short 'l'
+          <> help "Use the Untyped Lambda Calculus interpreter"
diff --git a/app/Repl/SystemF.hs b/app/Repl/SystemF.hs
--- a/app/Repl/SystemF.hs
+++ b/app/Repl/SystemF.hs
@@ -23,7 +23,7 @@
 runSystemFRepl
   = void . runExceptT . evalStateT (evalReplOpts replOpts) $ initialState
   where replOpts = mkReplOpts banner' $ evalSystemF . pack
-        initialState = mkTypecheckState defaultUniques
+        initialState = mkTypecheckState defaultUniques defaultTyUniques
 
 banner' :: MultiLine -> Repl String
 banner' _ = unpack <$> prompt (singleton upperLambda)
@@ -34,7 +34,7 @@
 
   let res = runTypecheck (evalText input) state'
   case res of
-    Left err -> liftIO . putStrLn . pack . show $ err
+    Left err -> liftIO . putStrLn . textDisplay $ err
     Right (res', newState) -> do
       put newState
       liftIO . putStrLn . prettyPrint $ res'
diff --git a/lambda-calculator.cabal b/lambda-calculator.cabal
--- a/lambda-calculator.cabal
+++ b/lambda-calculator.cabal
@@ -1,13 +1,13 @@
 cabal-version: 1.12
 
--- This file has been generated from package.yaml by hpack version 0.34.7.
+-- This file has been generated from package.yaml by hpack version 0.35.0.
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 4320ff01290c0c866383cba3463f4090d1413eb4efc9bff24cfae0496fd819f5
+-- hash: 3256f86f253ee771f5e7374ff11bcb34286722368054e4e233095c13c9abe64b
 
 name:           lambda-calculator
-version:        3.0.0.1
+version:        3.1.0.0
 synopsis:       A lambda calculus interpreter
 description:    A simple implementation of the Untyped Lambda Calculus
 category:       LambdaCalculus,Language,Teaching
@@ -15,7 +15,7 @@
 bug-reports:    https://github.com/sgillespie/lambda-calculator/issues
 author:         Sean D Gillespie
 maintainer:     sean@mistersg.net
-copyright:      2016 Sean Gillespie
+copyright:      2016-2023 Sean Gillespie
 license:        MIT
 license-file:   LICENSE
 build-type:     Simple
@@ -34,6 +34,7 @@
       Language.Lambda.Untyped.Parser
       Language.Lambda.Untyped.State
       Language.Lambda.SystemF
+      Language.Lambda.SystemF.Eval
       Language.Lambda.SystemF.Expression
       Language.Lambda.SystemF.Parser
       Language.Lambda.SystemF.State
@@ -67,6 +68,8 @@
       MultiParamTypeClasses
       MultiWayIf
       NamedFieldPuns
+      NoImplicitPrelude
+      OverloadedStrings
       PartialTypeSignatures
       PatternGuards
       PolyKinds
@@ -78,12 +81,11 @@
       TypeFamilies
       TypeSynonymInstances
       ViewPatterns
-      NoImplicitPrelude
-      OverloadedStrings
   ghc-options: -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wpartial-fields -Wredundant-constraints
   build-depends:
       base >=4.9 && <5
     , containers
+    , microlens
     , mtl
     , parsec
     , prettyprinter
@@ -125,6 +127,8 @@
       MultiParamTypeClasses
       MultiWayIf
       NamedFieldPuns
+      NoImplicitPrelude
+      OverloadedStrings
       PartialTypeSignatures
       PatternGuards
       PolyKinds
@@ -136,14 +140,13 @@
       TypeFamilies
       TypeSynonymInstances
       ViewPatterns
-      NoImplicitPrelude
-      OverloadedStrings
   ghc-options: -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wpartial-fields -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N
   build-depends:
       base >=4.9 && <5
     , bytestring
     , containers
     , lambda-calculator
+    , microlens
     , mtl
     , optparse-applicative
     , prettyprinter
@@ -181,6 +184,8 @@
       MultiParamTypeClasses
       MultiWayIf
       NamedFieldPuns
+      NoImplicitPrelude
+      OverloadedStrings
       PartialTypeSignatures
       PatternGuards
       PolyKinds
@@ -192,11 +197,11 @@
       TypeFamilies
       TypeSynonymInstances
       ViewPatterns
-      ImplicitPrelude
   ghc-options: -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wpartial-fields -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N
   build-depends:
       base >=4.9 && <5
     , hlint
+    , microlens
     , mtl
     , prettyprinter
     , rio
@@ -206,7 +211,11 @@
   type: exitcode-stdio-1.0
   main-is: Spec.hs
   other-modules:
+      Language.Lambda.SystemF.EvalSpec
+      Language.Lambda.SystemF.Examples.BoolSpec
+      Language.Lambda.SystemF.Examples.NatSpec
       Language.Lambda.SystemF.ExpressionSpec
+      Language.Lambda.SystemF.HspecUtils
       Language.Lambda.SystemF.ParserSpec
       Language.Lambda.SystemF.TypeCheckSpec
       Language.Lambda.SystemFSpec
@@ -245,6 +254,8 @@
       MultiParamTypeClasses
       MultiWayIf
       NamedFieldPuns
+      NoImplicitPrelude
+      OverloadedStrings
       PartialTypeSignatures
       PatternGuards
       PolyKinds
@@ -263,6 +274,7 @@
     , containers
     , hspec
     , lambda-calculator
+    , microlens
     , mtl
     , prettyprinter
     , rio
diff --git a/scripts/HLint.hs b/scripts/HLint.hs
--- a/scripts/HLint.hs
+++ b/scripts/HLint.hs
@@ -1,7 +1,7 @@
 module Main (main) where
 
 import Language.Haskell.HLint (hlint)
-import System.Exit (exitFailure, exitSuccess)
+import RIO
 
 arguments :: [String]
 arguments = [ 
diff --git a/src/Language/Lambda/Shared/Errors.hs b/src/Language/Lambda/Shared/Errors.hs
--- a/src/Language/Lambda/Shared/Errors.hs
+++ b/src/Language/Lambda/Shared/Errors.hs
@@ -3,7 +3,8 @@
     isLambdaException,
     isLetError,
     isParseError,
-    isImpossibleError
+    isImpossibleError,
+    isTyMismatchError,
   ) where
 
 import RIO
@@ -27,6 +28,7 @@
   -- Examples:
   --
   --     (\x: X. x) (y:Y)
+  --     (\x: T. x) [U]
   | TyMismatchError Text
 
   -- | A catch-all error that indicates a bug in this project
@@ -38,6 +40,7 @@
 instance Display LambdaException where
   textDisplay (ParseError txt) = "Parse error " <> txt
   textDisplay (InvalidLet txt) = "Illegal nested let: " <> txt
+  textDisplay (TyMismatchError txt) = "Type error: " <> txt
   textDisplay ImpossibleError = "An impossible error occurred! Please file a bug."
 
 instance Show LambdaException where
@@ -59,3 +62,7 @@
 isImpossibleError :: LambdaException -> Bool
 isImpossibleError ImpossibleError = True
 isImpossibleError _ = False
+
+isTyMismatchError :: LambdaException -> Bool
+isTyMismatchError (TyMismatchError _) = True
+isTyMismatchError _ = False
diff --git a/src/Language/Lambda/Shared/UniqueSupply.hs b/src/Language/Lambda/Shared/UniqueSupply.hs
--- a/src/Language/Lambda/Shared/UniqueSupply.hs
+++ b/src/Language/Lambda/Shared/UniqueSupply.hs
@@ -1,9 +1,27 @@
 module Language.Lambda.Shared.UniqueSupply where
 
+import Language.Lambda.Shared.Errors (LambdaException(..))
+
+import Control.Monad.Except (MonadError(..), throwError)
 import RIO
-import RIO.Text (pack)
+import RIO.List (find)
+import RIO.Text (pack, toUpper)
 
-defaultUniques :: [Text]
+type Unique = Text
+
+defaultUniques :: [Unique]
 defaultUniques = map pack strings
   where strings = concatMap (\p -> map (:p) . reverse $ ['a'..'z']) suffix
         suffix = "" : map show [(0::Int)..]
+
+defaultTyUniques :: [Unique]
+defaultTyUniques = map toUpper defaultUniques
+
+next
+  :: (Ord name, MonadError LambdaException m)
+  => [name] -- ^ Unique supply
+  -> [name] -- ^ Free Variables
+  -> m name
+next freeVars uniques' = case find (`notElem` freeVars) uniques' of
+  Just unique -> pure unique
+  Nothing -> throwError ImpossibleError
diff --git a/src/Language/Lambda/SystemF.hs b/src/Language/Lambda/SystemF.hs
--- a/src/Language/Lambda/SystemF.hs
+++ b/src/Language/Lambda/SystemF.hs
@@ -1,26 +1,100 @@
 module Language.Lambda.SystemF (
-  Globals(),
   evalText,
+  typecheckText,
+  runEvalText,
+  runTypecheckText,
+  execEvalText,
+  execTypecheckText,
+  unsafeExecEvalText,
+  unsafeExecTypecheckText,
+  defaultUniques,
+  defaultTyUniques,
+  mkState,
 
   module Language.Lambda.SystemF.Expression,
   module Language.Lambda.SystemF.Parser,
   module Language.Lambda.SystemF.State
   ) where
 
-import Control.Monad.Except
-import RIO
-import qualified RIO.Text as Text
-import qualified Data.Map as Map
-
 import Language.Lambda.Shared.Errors
+import Language.Lambda.Shared.UniqueSupply (defaultUniques, defaultTyUniques)
+import Language.Lambda.SystemF.Eval (evalExpr)
 import Language.Lambda.SystemF.Expression
 import Language.Lambda.SystemF.Parser
 import Language.Lambda.SystemF.State
+import Language.Lambda.SystemF.TypeCheck
 
-type Globals = Map.Map String (SystemFExpr String String)
+import Control.Monad.Except
+import RIO
+import qualified RIO.Text as Text
+import qualified RIO.Map as Map
 
-evalText :: Text -> Typecheck Text (SystemFExpr Text Text)
-evalText text = case parseExpr text of
-  Left err -> throwError $ ParseError $ Text.pack $ show err
-  Right res -> return res
+evalText
+  :: Text
+  -> Typecheck Text (TypedExpr Text)
+evalText = either throwParseError processExpr . parseExpr
+    where throwParseError = throwError . ParseError . Text.pack . show
 
+typecheckText
+  :: Text
+  -> Typecheck Text (Ty Text)
+typecheckText = either throwParseError typecheck . parseExpr
+    where throwParseError = throwError . ParseError . Text.pack . show
+
+runEvalText
+  :: Text
+  -> Globals Text
+  -> Either LambdaException (TypedExpr Text, TypecheckState Text)
+runEvalText input globals' = runTypecheck (evalText input) (mkState globals')
+
+runTypecheckText
+  :: Text
+  -> Globals Text
+  -> Either LambdaException (Ty Text, TypecheckState Text)
+runTypecheckText input globals'
+  = runTypecheck (typecheckText input) (mkState globals')
+
+execEvalText
+  :: Text
+  -> Globals Text
+  -> Either LambdaException (TypedExpr Text)
+execEvalText input globals'
+  = execTypecheck (evalText input) (mkState globals')
+
+execTypecheckText
+  :: Text
+  -> Globals Text
+  -> Either LambdaException (Ty Text)
+execTypecheckText input globals'
+  = execTypecheck (typecheckText input) (mkState globals')
+
+unsafeExecEvalText
+  :: Text
+  -> Globals Text
+  -> TypedExpr Text
+unsafeExecEvalText input globals'
+  = unsafeExecTypecheck (evalText input) (mkState globals')
+
+unsafeExecTypecheckText
+  :: Text
+  -> Globals Text
+  -> Ty Text
+unsafeExecTypecheckText input globals'
+  = unsafeExecTypecheck (typecheckText input) (mkState globals')
+
+mkState :: Globals Text -> TypecheckState Text
+mkState globals' = TypecheckState globals' defaultUniques defaultTyUniques
+
+processExpr :: SystemFExpr Text -> Typecheck Text (TypedExpr Text)
+processExpr (Let n expr) = tcAndEval expr >>= addBinding n
+processExpr expr = tcAndEval expr
+
+tcAndEval :: SystemFExpr Text -> Typecheck Text (TypedExpr Text)
+tcAndEval expr = do
+  ty <- typecheck expr
+  reduced <- evalExpr expr
+
+  pure $ TypedExpr reduced ty
+
+addBinding :: Text -> TypedExpr Text -> Typecheck Text (TypedExpr Text)
+addBinding name expr = modifyGlobals (Map.insert name expr) >> pure expr
diff --git a/src/Language/Lambda/SystemF/Eval.hs b/src/Language/Lambda/SystemF/Eval.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Lambda/SystemF/Eval.hs
@@ -0,0 +1,179 @@
+module Language.Lambda.SystemF.Eval
+  ( evalExpr,
+    subGlobals,
+    betaReduce,
+    alphaConvert,
+    etaConvert,
+    freeVarsOf
+  ) where
+
+import Language.Lambda.Shared.Errors
+import Language.Lambda.Shared.UniqueSupply (next)
+import Language.Lambda.SystemF.Expression
+import Language.Lambda.SystemF.State
+
+import Control.Monad.Except (throwError)
+import Prettyprinter
+import RIO
+import qualified RIO.Map as Map
+
+-- | Evaluates an expression
+evalExpr
+  :: (Pretty name, Ord name)
+  => SystemFExpr name
+  -> Typecheck name (SystemFExpr name)
+evalExpr = evalTopLevel
+
+-- | Evaluates a top-level expression
+evalTopLevel
+  :: (Pretty name, Ord name)
+  => SystemFExpr name
+  -> Typecheck name (SystemFExpr name)
+evalTopLevel (Let n expr) = Let n <$> (subGlobals expr >>= evalInner)
+evalTopLevel expr = subGlobals expr >>= evalInner
+
+-- | Evaluates a non top-level expression. Does NOT support Lets
+evalInner
+  :: (Pretty name, Ord name)
+  => SystemFExpr name
+  -> Typecheck name (SystemFExpr name)
+evalInner (Abs n ty expr) = Abs n ty <$> evalInner expr
+evalInner (App e1 e2) = evalApp e1 e2
+evalInner (TyAbs n expr) = TyAbs n <$> evalInner expr
+evalInner (TyApp expr ty) = evalTyApp expr ty
+evalInner (Let n expr) = throwError . InvalidLet . prettyPrint $ Let n expr
+evalInner expr = pure expr
+
+subGlobals :: Ord name => SystemFExpr name -> Typecheck name (SystemFExpr name)
+subGlobals expr = getGlobals >>= subGlobals'
+  where subGlobals' globals' = case expr of
+          Var x -> pure . maybe expr (view _expr) $ globals' Map.!? x
+          VarAnn x _ -> pure . maybe expr (view _expr) $ globals' Map.!? x
+          App e1 e2 -> App <$> subGlobals e1 <*> subGlobals e2
+          Abs name ty expr'
+            | Map.member name globals' -> pure expr
+            | otherwise -> Abs name ty <$> subGlobals expr'
+          _ -> pure expr
+
+evalApp
+  :: (Pretty name, Ord name)
+  => SystemFExpr name
+  -> SystemFExpr name
+  -> Typecheck name (SystemFExpr name)
+evalApp e1 e2 = do
+  e1' <- evalInner e1
+  e2' <- evalInner e2
+
+  betaReduce e1' e2'
+
+evalTyApp
+  :: (Pretty name, Ord name)
+  => SystemFExpr name
+  -> Ty name
+  -> Typecheck name (SystemFExpr name)
+evalTyApp expr ty = case expr of
+  TyAbs name inner -> evalInner $ substituteTyInExpr ty name inner
+  Abs name (TyForAll tyName ty') inner ->
+    Abs name (substituteTy ty tyName ty') <$> evalInner inner
+  VarAnn name (TyForAll tyName ty') -> pure $ VarAnn name (substituteTy ty tyName ty')
+  _ -> TyApp <$> evalInner expr <*> pure ty
+
+betaReduce
+  :: (Ord name, Pretty name)
+  => SystemFExpr name
+  -> SystemFExpr name
+  -> Typecheck name (SystemFExpr name)
+betaReduce e1 e2 = case e1 of
+  App e1' e2' -> App <$> betaReduce e1' e2' <*> pure e2
+  Abs n _ e1' -> do
+    converted <- alphaConvert (freeVarsOf e2) e1'
+    evalInner $ substitute converted n e2
+  Let _ _ -> throwError ImpossibleError
+  _ -> pure $ App e1 e2
+
+alphaConvert
+  :: (Ord name, Pretty name)
+  => [name]
+  -> SystemFExpr name
+  -> Typecheck name (SystemFExpr name)
+alphaConvert freeVars (Abs name ty body) = do
+  uniques <- getVarUniques
+  nextName <- next freeVars uniques
+  alphaConvertAbs name ty body freeVars nextName
+alphaConvert _ expr = pure expr
+
+etaConvert :: Ord name => SystemFExpr name -> SystemFExpr name
+etaConvert (Abs name ty body) = case body of
+  App e1 (Var name')
+    | name == name' -> etaConvert e1
+    | otherwise -> Abs name ty (App (etaConvert e1) (Var name'))
+  body'@Abs{}
+    | body' == eta' -> Abs name ty body'
+    | otherwise -> etaConvert $ Abs name ty eta'
+    where eta' = etaConvert body'
+  _ -> Abs name ty $ etaConvert body
+etaConvert (App e1 e2) = App (etaConvert e1) (etaConvert e2)
+etaConvert expr = expr
+
+substitute
+  :: Eq name
+  => SystemFExpr name
+  -> name
+  -> SystemFExpr name
+  -> SystemFExpr name
+substitute expr forName inExpr
+  = case expr of
+      (Var n)
+        | n == forName -> inExpr
+        | otherwise -> expr
+      (VarAnn n _)
+        | n == forName -> inExpr
+        | otherwise -> expr
+      (Abs n ty body)
+        | n == forName -> expr
+        | otherwise -> Abs n ty $ substitute body forName inExpr
+      (App e1 e2) -> App (sub e1) (sub e2)
+      (TyAbs n body) -> TyAbs n $ substitute body forName inExpr
+      (TyApp body ty) -> TyApp (substitute body forName inExpr) ty
+      _ -> inExpr
+  where sub expr' = substitute expr' forName inExpr
+
+substituteTyInExpr
+  :: Eq name
+  => Ty name
+  -> name
+  -> SystemFExpr name
+  -> SystemFExpr name
+substituteTyInExpr ty forName inExpr
+  = case inExpr of
+      VarAnn name ty' -> VarAnn name (substituteTy ty forName ty')
+      App e1 e2 -> App (sub e1) (sub e2)
+      Abs name ty' expr -> Abs name (substituteTy ty forName ty') (sub expr)
+      TyAbs name expr -> TyAbs name (sub expr)
+      TyApp expr ty' -> TyApp (sub expr) (substituteTy ty forName ty')
+      _ -> inExpr
+  where sub = substituteTyInExpr ty forName
+
+freeVarsOf
+  :: (Ord name, Pretty name)
+  => SystemFExpr name
+  -> [name]
+freeVarsOf (Abs n _ expr) = filter (/=n) . freeVarsOf $ expr
+freeVarsOf (App e1 e2) = freeVarsOf e1 ++ freeVarsOf e2
+freeVarsOf (Var n) = [n]
+freeVarsOf (VarAnn n _) = [n]
+freeVarsOf (Let _ expr) = freeVarsOf expr
+freeVarsOf (TyAbs _ expr) = freeVarsOf expr
+freeVarsOf (TyApp expr _) = freeVarsOf expr
+
+alphaConvertAbs
+  :: (Ord name, Pretty name)
+  => name
+  -> Ty name
+  -> SystemFExpr name
+  -> [name]
+  -> name
+  -> Typecheck name (SystemFExpr name)
+alphaConvertAbs name ty body freeVars nextName
+  | name `elem` freeVars = pure $ Abs nextName ty (substitute body name (Var nextName))
+  | otherwise = Abs name ty <$> alphaConvert freeVars body
diff --git a/src/Language/Lambda/SystemF/Expression.hs b/src/Language/Lambda/SystemF/Expression.hs
--- a/src/Language/Lambda/SystemF/Expression.hs
+++ b/src/Language/Lambda/SystemF/Expression.hs
@@ -1,7 +1,11 @@
 module Language.Lambda.SystemF.Expression
   ( SystemFExpr(..),
+    TypedExpr(..),
     Ty(..),
+    _expr,
+    _ty,
     prettyPrint,
+    substituteTy,
     upperLambda
   ) where
 
@@ -10,46 +14,91 @@
 import Prettyprinter.Render.Text (renderStrict)
 import RIO
 
-data SystemFExpr name ty
+data SystemFExpr name
+  -- | A global binding: `let x = y`
+  = Let name (SystemFExpr name)
   -- | Variable: `x`
-  = Var name
+  | Var name
+  -- | Variable annotated with type: `x:T`
+  | VarAnn name (Ty name)
   -- | Function application: `x y`
-  | App (SystemFExpr name ty) (SystemFExpr name ty)
+  | App (SystemFExpr name) (SystemFExpr name)
   -- | Lambda abstraction: `\x: X. x`
-  | Abs name (Ty ty) (SystemFExpr name ty)
+  | Abs name (Ty name) (SystemFExpr name)
   -- | Type Abstraction: `\X. body`
-  | TyAbs ty (SystemFExpr name ty)                  
+  | TyAbs name (SystemFExpr name)
   -- | Type Application: `x [X]`
-  | TyApp (SystemFExpr name ty) (Ty ty)
+  | TyApp (SystemFExpr name) (Ty name)
   deriving (Eq, Show)
 
+data TypedExpr name = TypedExpr
+  { teExpr :: SystemFExpr name,
+    teTy :: Ty name
+  } deriving (Eq, Show)
+
 data Ty name
   = TyVar name                  -- ^ Type variable (T)
   | TyArrow (Ty name) (Ty name) -- ^ Type arrow    (T -> U)
   | TyForAll name (Ty name)     -- ^ Universal type (forall T. X)
-  deriving (Eq, Show)
+  deriving (Show)
 
-instance (Pretty name, Pretty ty) => Pretty (SystemFExpr name ty) where
+instance (Pretty name) => Pretty (SystemFExpr name) where
   pretty (Var name) = pretty name
+  pretty (VarAnn name ty) = prettyVarAnn name ty
   pretty (App e1 e2) = prettyApp e1 e2
   pretty (Abs name ty body) = prettyAbs name ty body
+  pretty (Let name expr) = prettyLet name expr
   pretty (TyAbs ty body) = prettyTyAbs ty body
   pretty (TyApp expr ty) = prettyTyApp expr ty
 
+instance Pretty name => Pretty (TypedExpr name) where
+  pretty expr = pretty (expr ^. _expr) <+> colon <+> pretty (expr ^. _ty)
+
 instance Pretty name => Pretty (Ty name) where
   pretty = prettyTy False
 
+instance Eq name => Eq (Ty name) where
+  (==) = isTyEquivalent
+
+_expr :: Lens' (TypedExpr name) (SystemFExpr name)
+_expr = lens teExpr (\res expr -> res { teExpr = expr })
+
+_ty :: Lens' (TypedExpr name) (Ty name)
+_ty = lens teTy (\res ty -> res { teTy = ty })
+
 prettyPrint :: Pretty pretty => pretty -> Text
 prettyPrint expr = renderStrict docStream
   where docStream = layoutPretty defaultLayoutOptions (pretty expr)
 
+substituteTy
+  :: Eq name
+  => Ty name
+  -> name
+  -> Ty name
+  -> Ty name
+substituteTy ty forName inTy
+  = case inTy of
+      TyVar n
+        | n == forName -> ty
+        | otherwise -> inTy
+      TyArrow t1 t2 -> TyArrow (sub t1) (sub t2)
+      TyForAll n ty'
+        | n == forName -> inTy
+        | otherwise -> TyForAll n (sub ty')
+  where sub = substituteTy ty forName
+
 upperLambda :: Char
 upperLambda = 'Λ'
 
+prettyVarAnn :: Pretty name => name -> Ty name -> Doc a
+prettyVarAnn var ty = pretty var <> colon <> prettyTy' ty
+  where prettyTy' (TyVar _) = prettyTy True ty
+        prettyTy' _ = parens $ prettyTy True ty
+
 prettyApp
-  :: (Pretty name, Pretty ty)
-  => SystemFExpr name ty
-  -> SystemFExpr name ty
+  :: Pretty name
+  => SystemFExpr name
+  -> SystemFExpr name
   -> Doc a
 prettyApp e1@Abs{} e2@Abs{} = parens (pretty e1) <+> parens (pretty e2)
 prettyApp e1@Abs{} e2 = parens (pretty e1) <+> pretty e2
@@ -58,10 +107,10 @@
 prettyApp e1 e2 = pretty e1 <+> pretty e2
 
 prettyAbs
-  :: (Pretty name, Pretty ty)
+  :: Pretty name
   => name
-  -> Ty ty
-  -> SystemFExpr name ty
+  -> Ty name
+  -> SystemFExpr name
   -> Doc ann
 prettyAbs name ty body
   = lambda
@@ -70,11 +119,14 @@
     <+> pretty body'
   where (names, body') = uncurryAbs name ty body
 
-prettyTyAbs :: (Pretty name, Pretty ty) => ty -> SystemFExpr name ty -> Doc ann
+prettyLet :: Pretty name => name -> SystemFExpr name -> Doc ann
+prettyLet name expr = "let" <+> pretty name <+> equals <+> pretty expr
+
+prettyTyAbs :: (Pretty name) => name -> SystemFExpr name -> Doc ann
 prettyTyAbs name body = upperLambda' <+> hsep (map pretty names) <> dot
     <+> pretty body'
   where (names, body') = uncurryTyAbs name body
-prettyTyApp :: (Pretty name, Pretty ty) => SystemFExpr name ty -> Ty ty -> Doc ann
+prettyTyApp :: (Pretty name) => SystemFExpr name -> Ty name -> Doc ann
 prettyTyApp expr ty = pretty expr <+> brackets (pretty ty)
 
 prettyTy :: Pretty name => Bool -> Ty name -> Doc ann
@@ -82,6 +134,13 @@
 prettyTy compact (TyArrow t1 t2) = prettyTyArrow compact t1 t2
 prettyTy compact (TyForAll name ty) = prettyTyForAll compact name ty
 
+isTyEquivalent :: Eq name => Ty name -> Ty name -> Bool
+isTyEquivalent t1 t2
+  | t1 `isTySame` t2 = True
+  | otherwise = case (t1, t2) of
+      (TyForAll n1 t1', TyForAll n2 t2') -> (n1, t1') `areForAllsEquivalent` (n2, t2')
+      _ -> False
+
 prettyTyArrow :: Pretty name => Bool -> Ty name -> Ty name -> Doc ann
 prettyTyArrow compact (TyArrow t1 t2) t3
   = prettyTyArrow' compact compositeTy $ prettyTy compact t3
@@ -107,18 +166,27 @@
 upperLambda' :: Doc ann
 upperLambda' = pretty upperLambda
 
+isTySame :: Eq name => Ty name -> Ty name -> Bool
+isTySame (TyVar n1) (TyVar n2) = n1 == n2
+isTySame (TyArrow t1 t2) (TyArrow t1' t2') = t1 == t1' && t2 == t2'
+isTySame (TyForAll n1 t1) (TyForAll n2 t2) = n1 == n2 && t1 == t2
+isTySame _ _ = False
+
+areForAllsEquivalent :: Eq name => (name, Ty name) -> (name, Ty name) -> Bool
+areForAllsEquivalent (n1, t1) (n2, t2) = t1 == substituteTy (TyVar n1) n2 t2
+
 prettyTyArrow' :: Bool -> Doc ann -> Doc ann -> Doc ann
 prettyTyArrow' compact doc1 doc2 = doc1 `add'` "->" `add'` doc2
   where add'
           | compact = (<>) 
           | otherwise = (<+>)
 
-uncurryAbs :: n -> Ty t -> SystemFExpr n t -> ([(n, Ty t)], SystemFExpr n t)
+uncurryAbs :: n -> Ty n -> SystemFExpr n -> ([(n, Ty n)], SystemFExpr n)
 uncurryAbs name ty = uncurry' [(name, ty)] 
   where uncurry' ns (Abs n' t' body') = uncurry' ((n', t'):ns) body'
         uncurry' ns body'             = (reverse ns, body')
 
-uncurryTyAbs :: t -> SystemFExpr n t -> ([t], SystemFExpr n t)
+uncurryTyAbs :: n -> SystemFExpr n -> ([n], SystemFExpr n)
 uncurryTyAbs ty = uncurry' [ty]
   where uncurry' ts (TyAbs t' body') = uncurry' (t':ts) body'
         uncurry' ts body'            = (reverse ts, body')
diff --git a/src/Language/Lambda/SystemF/Parser.hs b/src/Language/Lambda/SystemF/Parser.hs
--- a/src/Language/Lambda/SystemF/Parser.hs
+++ b/src/Language/Lambda/SystemF/Parser.hs
@@ -13,46 +13,61 @@
 
 import Language.Lambda.SystemF.Expression
 
-parseExpr :: Text -> Either ParseError (SystemFExpr Text Text)
-parseExpr = parse (whitespace *> expr <* eof) ""
+parseExpr :: Text -> Either ParseError (SystemFExpr Text)
+parseExpr = parse (whitespace *> topLevelExpr <* eof) ""
 
 parseType :: Text -> Either ParseError (Ty Text)
 parseType = parse (whitespace *> ty <* eof) ""
 
+-- Lets can only be at the top level
+topLevelExpr :: Parser (SystemFExpr Text)
+topLevelExpr = let' <|> expr
+
 -- Parse expressions
-expr :: Parser (SystemFExpr Text Text)
+expr :: Parser (SystemFExpr Text)
 expr = try tyapp <|> try app <|> term
 
-app :: Parser (SystemFExpr Text Text)
+app :: Parser (SystemFExpr Text)
 app = chainl1 term (return App)
 
-tyapp :: Parser (SystemFExpr Text Text)
+tyapp :: Parser (SystemFExpr Text)
 tyapp = TyApp
       <$> term
       <*> ty'
   where ty' = symbol '[' *> ty <* symbol ']'
 
-term :: Parser (SystemFExpr Text Text)
+term :: Parser (SystemFExpr Text)
 term = try abs <|> tyabs <|> var <|> parens expr
 
-var :: Parser (SystemFExpr Text Text)
-var = Var <$> exprId
+let' :: Parser (SystemFExpr Text)
+let' = Let <$> ident <*> expr
+  where ident = symbol' "let" *> exprId <* symbol '='
 
-abs :: Parser (SystemFExpr Text Text)
+var :: Parser (SystemFExpr Text)
+var = try varann <|> var'
+  where var' = Var <$> exprId
+        varann = VarAnn <$> (exprId <* symbol ':') <*> ty
+
+abs :: Parser (SystemFExpr Text)
 abs = curry'
-    <$> (symbol '\\' *> many1 args <* symbol '.') 
+    <$> (symbol '\\' *> many1 args <* symbol '.')
     <*> expr
   where args = (,) <$> (exprId <* symbol ':') <*> ty
         curry' = flip . foldr . uncurry $ Abs
 
-tyabs :: Parser (SystemFExpr Text Text)
+tyabs :: Parser (SystemFExpr Text)
 tyabs = curry' <$> args <*> expr
   where args = symbol '\\' *> many1 typeId <* symbol '.'
         curry' = flip (foldr TyAbs)
 
 -- Parse type expressions
 ty :: Parser (Ty Text)
-ty = try arrow
+ty = try forall <|> try arrow
+
+forall :: Parser (Ty Text)
+forall = curry' <$> args <*> ty
+  where args = symbol' "forall" *> many1 typeId <* symbol '.'
+        curry' = flip $ foldr TyForAll
 
 arrow :: Parser (Ty Text)
 arrow = chainr1 tyterm (symbol' "->" $> TyArrow)
diff --git a/src/Language/Lambda/SystemF/State.hs b/src/Language/Lambda/SystemF/State.hs
--- a/src/Language/Lambda/SystemF/State.hs
+++ b/src/Language/Lambda/SystemF/State.hs
@@ -2,23 +2,31 @@
   ( TypecheckState(..),
     Typecheck(),
     Context(),
+    Binding(..),
+    Globals(),
     runTypecheck,
     execTypecheck,
     unsafeRunTypecheck,
     unsafeExecTypecheck,
     mkTypecheckState,
-    context,
-    uniques,
+    _context,
+    _globals,
+    _varUniques,
+    _tyUniques,
     getContext,
-    getUniques,
-    modifyContext,
-    modifyUniques,
-    setContext,
-    setUniques
+    getGlobals,
+    getVarUniques,
+    getTyUniques,
+    modifyGlobals,
+    modifyVarUniques,
+    modifyTyUniques,
+    setGlobals,
+    setVarUniques,
+    setTyUniques
   ) where
 
 import Language.Lambda.Shared.Errors (LambdaException(..))
-import Language.Lambda.SystemF.Expression (Ty(..))
+import Language.Lambda.SystemF.Expression
 
 import Control.Monad.Except (Except(), runExcept)
 import RIO
@@ -26,16 +34,24 @@
 import qualified RIO.Map as Map
 
 data TypecheckState name = TypecheckState
-  { tsContext :: Context name,
-    tsUniques :: [name]
-  }
+  { tsGlobals :: Globals name,
+    tsVarUniques :: [name],  -- ^ A unique supply of term-level variables
+    tsTyUniques :: [name]    -- ^ A unique supply of type-level variables
+  } deriving (Eq, Show)
 
 type Typecheck name
   = StateT (TypecheckState name)
       (Except LambdaException)
 
-type Context name = Map name (Ty name)
+type Globals name = Map name (TypedExpr name)
 
+type Context name = Map name (Binding name)
+
+data Binding name
+  = BindTerm (Ty name)
+  | BindTy
+  deriving (Eq, Show)
+
 runTypecheck
   :: Typecheck name result
   -> TypecheckState name
@@ -59,31 +75,52 @@
 unsafeExecTypecheck computation state' = either impureThrow id tcResult
   where tcResult = execTypecheck computation state'
 
-mkTypecheckState :: [name] -> TypecheckState name
+mkTypecheckState :: [name] -> [name] -> TypecheckState name
 mkTypecheckState = TypecheckState Map.empty
 
-uniques :: Lens' (TypecheckState name) [name]
-uniques f state' = (\uniques' -> state' { tsUniques = uniques' })
-  <$> f (tsUniques state')
+_context :: SimpleGetter (TypecheckState name) (Context name)
+_context = to (getContext' . tsGlobals)
+  where getContext' :: Globals name -> Context name
+        getContext' = Map.map (\expr -> BindTerm (expr ^. _ty))
+        
+_globals :: Lens' (TypecheckState name) (Globals name)
+_globals f state' = (\globals' -> state' { tsGlobals = globals' })
+  <$> f (tsGlobals state')
 
-context :: Lens' (TypecheckState name) (Context name)
-context f state' = (\context' -> state' { tsContext = context' })
-  <$> f (tsContext state')
+_varUniques :: Lens' (TypecheckState name) [name]
+_varUniques f state' = (\uniques' -> state' { tsVarUniques = uniques' })
+  <$> f (tsVarUniques state')
 
-getUniques :: Typecheck name [name]
-getUniques = gets (^. uniques)
+_tyUniques :: Lens' (TypecheckState name) [name]
+_tyUniques f state' = (\uniques' -> state' { tsTyUniques = uniques' })
+  <$> f (tsTyUniques state')
 
+getVarUniques :: Typecheck name [name]
+getVarUniques = gets (^. _varUniques)
+
+getTyUniques :: Typecheck name [name]
+getTyUniques = gets (^. _tyUniques)
+
 getContext :: Typecheck name (Context name)
-getContext = gets (^. context)
+getContext = gets (^. _context)
 
-modifyContext :: (Context name -> Context name) -> Typecheck name ()
-modifyContext f = modify $ context %~ f
+getGlobals :: Typecheck name (Globals name)
+getGlobals = gets (^. _globals)
 
-modifyUniques :: ([name] -> [name]) -> Typecheck name ()
-modifyUniques f = modify $ uniques %~ f
+modifyGlobals :: (Globals name -> Globals name) -> Typecheck name ()
+modifyGlobals f = modify $ _globals %~ f
 
-setUniques :: [name] -> Typecheck name ()
-setUniques uniques' = modify (& uniques .~ uniques')
+modifyVarUniques :: ([name] -> [name]) -> Typecheck name ()
+modifyVarUniques f = modify $ _varUniques %~ f
 
-setContext :: Context name -> Typecheck name ()
-setContext context' = modify (& context .~ context')
+modifyTyUniques :: ([name] -> [name]) -> Typecheck name ()
+modifyTyUniques f = modify $ _tyUniques %~ f
+
+setVarUniques :: [name] -> Typecheck name ()
+setVarUniques uniques' = modify $ _varUniques .~ uniques'
+
+setTyUniques :: [name] -> Typecheck name ()
+setTyUniques uniques' = modify $ _tyUniques .~ uniques'
+
+setGlobals :: Globals name -> Typecheck name ()
+setGlobals globals' = modify $ _globals .~ globals'
diff --git a/src/Language/Lambda/SystemF/TypeCheck.hs b/src/Language/Lambda/SystemF/TypeCheck.hs
--- a/src/Language/Lambda/SystemF/TypeCheck.hs
+++ b/src/Language/Lambda/SystemF/TypeCheck.hs
@@ -7,116 +7,183 @@
 import Control.Monad.Except (MonadError(..))
 import Prettyprinter
 import RIO
-import qualified RIO.List as List
 import qualified RIO.Map as Map
 
 type UniqueSupply n = [n]
 type Context' n t = Map n t
 
--- TODO: name/ty different types
 typecheck
   :: (Ord name, Pretty name)
-  => SystemFExpr name name
+  => SystemFExpr name
   -> Typecheck name (Ty name)
-typecheck (Var v) = typecheckVar v
-typecheck (Abs n t body) = typecheckAbs n t body
-typecheck (App e1 e2) = typecheckApp e1 e2
-typecheck (TyAbs t body) = typecheckTyAbs t body
-typecheck (TyApp e ty) = typecheckTyApp e ty
+typecheck expr = do
+  ctx <- getContext
+  typecheckTopLevel ctx expr
 
-typecheckVar :: Ord name => name -> Typecheck name (Ty name)
-typecheckVar var = getContext >>= defaultToFreshTyVar . Map.lookup var
-  where defaultToFreshTyVar (Just v) = return v
-        defaultToFreshTyVar Nothing = TyVar <$> unique
+typecheckTopLevel
+  :: (Ord name, Pretty name)
+  => Context name
+  -> SystemFExpr name
+  -> Typecheck name (Ty name)
+typecheckTopLevel ctx (Let n expr) = typecheckLet ctx n expr
+typecheckTopLevel ctx expr = typecheckExpr ctx expr
 
+typecheckLet
+  :: (Pretty name, Ord name)
+  => Context name
+  -> name
+  -> SystemFExpr name
+  -> Typecheck name (Ty name)
+typecheckLet ctx _ = typecheckExpr ctx
+  
+typecheckExpr
+  :: (Ord name, Pretty name)
+  => Context name
+  -> SystemFExpr name
+  -> Typecheck name (Ty name)
+typecheckExpr ctx (Var v) = typecheckVar ctx v
+typecheckExpr ctx (VarAnn v ty) = typecheckVarAnn ctx v ty
+typecheckExpr ctx (Abs n t body) = typecheckAbs ctx n t body
+typecheckExpr ctx (App e1 e2) = typecheckApp ctx e1 e2
+typecheckExpr ctx (TyAbs t body) = typecheckTyAbs ctx t body
+typecheckExpr ctx (TyApp e ty) = typecheckTyApp ctx e ty
+typecheckExpr _ (Let _ _) = throwError ImpossibleError
+
+typecheckVar :: Ord name => Context name -> name -> Typecheck name (Ty name)
+typecheckVar ctx = defaultToUnique . typecheckVar' ctx
+  where defaultToUnique = maybe (TyVar <$> tyUnique) pure
+    
+typecheckVarAnn
+  :: (Ord name, Pretty name)
+  => Context name
+  -> name
+  -> Ty  name
+  -> Typecheck name (Ty name)
+typecheckVarAnn ctx var ty = maybe (pure ty) checkContextType maybeTy
+  where checkContextType ty'
+          | ty' == ty = pure ty
+          | otherwise = throwError $ tyMismatchError ty' ty
+        maybeTy = typecheckVar' ctx var
+
 typecheckAbs
   :: (Ord name, Pretty name)
-  => name
+  => Context name
+  -> name
   -> Ty name
-  -> SystemFExpr name name
+  -> SystemFExpr name
   -> Typecheck name (Ty name)
-typecheckAbs name ty body
-  = modifyContext (Map.insert name ty)
-    >> TyArrow ty <$> typecheck body
+typecheckAbs ctx name ty body = typecheckAbs' ty' (Map.insert name (BindTerm ty') ctx)
+  where typecheckAbs' (TyForAll tyName tyBody) ctx' = do
+          inner <- typecheckExpr (Map.insert tyName BindTy ctx') body
+          pure $ TyForAll tyName (TyArrow tyBody inner)
+        typecheckAbs' t ctx' = TyArrow t <$> typecheckExpr ctx' body
 
+        ty' = liftForAlls ty
+      
 typecheckApp
   :: (Ord name, Pretty name)
-  => SystemFExpr name name
-  -> SystemFExpr name name
+  => Context name
+  -> SystemFExpr name
+  -> SystemFExpr name
   -> Typecheck name (Ty name)
-typecheckApp e1 e2 = do
+typecheckApp ctx e1 e2 = do
   -- Typecheck expressions
-  t1 <- typecheck e1
-  t2 <- typecheck e2
+  t1 <- typecheckExpr ctx e1
+  t2 <- typecheckExpr ctx e2
 
-  -- Verify the type of t1 is an Arrow
   (t1AppInput, t1AppOutput) <- case t1 of
-    (TyArrow appInput appOutput) -> return (appInput, appOutput)
-    t1' -> throwError $ tyMismatchError t1' t1
+    (TyArrow appInput appOutput) -> pure (appInput, appOutput)
+    (TyForAll n1 (TyArrow appInput _))
+      -> pure (TyForAll n1 appInput, t2)
+    _ -> throwError $ TyMismatchError "Not Arrow"
 
   -- Verify the output of e1 matches the type of e2
-  if t1AppInput == t2
+  if t1AppInput `isTyEquivalent` t2
     then return t1AppOutput
     else throwError $ tyMismatchError (TyArrow t2 t1AppOutput) (TyArrow t1 t1AppOutput)
 
 typecheckTyAbs
   :: (Ord name, Pretty name)
-  => name
-  -> SystemFExpr name name
+  => Context name
+  -> name
+  -> SystemFExpr name
   -> Typecheck name (Ty name)
-typecheckTyAbs ty body
-  = modifyContext (Map.insert ty (TyVar ty))
-    >> TyForAll ty <$> typecheck body
+typecheckTyAbs ctx ty body = TyForAll ty <$> typecheckExpr ctx' body
+  where ctx' = Map.insert ty BindTy ctx
 
 typecheckTyApp
   :: (Ord name, Pretty name)
-  => SystemFExpr name name
+  => Context name
+  -> SystemFExpr name
   -> Ty name
   -> Typecheck name (Ty name)
-typecheckTyApp (TyAbs t expr) ty = typecheck $ substitute ty t expr
-typecheckTyApp expr _ = typecheck expr
+typecheckTyApp ctx expr ty = do
+  -- Clear in-scope type variables
+  let ctx' = Map.filter isTyBind ctx
+  
+  typecheckExpr ctx' expr >>= \case
+    TyForAll tyName tyBody -> pure $ substituteTy ty tyName tyBody
+    _ -> do
+      err <- tyAppMismatchError ctx expr ty
+      throwError err
 
-unique :: Typecheck name name
-unique = getUniques >>= fromJust' . List.headMaybe
-  where fromJust' (Just u) = return u
-        fromJust' Nothing = throwError ImpossibleError
+  where
+    isTyBind BindTy = False
+    isTyBind _ = True
 
-substitute
-  :: Eq n
-  => Ty n
-  -> n
-  -> SystemFExpr n n
-  -> SystemFExpr n n
-substitute ty name (App e1 e2) = App (substitute ty name e1) (substitute ty name e2)
-substitute ty name (Abs n ty' e) = Abs n (substituteTy ty name ty') (substitute ty name e)
-substitute ty name (TyAbs ty' e) = TyAbs ty' (substitute ty name e) 
-substitute ty name (TyApp e ty') = TyApp (substitute ty name e) (substituteTy ty name ty')
-substitute _ _ expr = expr
+typecheckVar' :: Ord name => Context name -> name -> Maybe (Ty name)
+typecheckVar' ctx var = Map.lookup var ctx >>= \case
+  BindTerm ty@(TyForAll tyName tyBody)
+    | Map.member tyName ctx -> Just tyBody
+    | otherwise -> Just ty
+  BindTerm ty -> Just ty
+  BindTy -> Nothing
 
-substituteTy
-  :: Eq name
-  => Ty name
-  -> name
-  -> Ty name
-  -> Ty name
-substituteTy ty name (TyArrow t1 t2) 
-  = TyArrow (substituteTy ty name t1) (substituteTy ty name t2)
-substituteTy ty name ty'@(TyVar name') 
-  | name == name' = ty
-  | otherwise     = ty'
-substituteTy _ name t2@(TyForAll name' t2') 
-  | name == name' = t2
-  | otherwise     = TyForAll name' (substituteTy t2 name t2')
+liftForAlls :: Ty name -> Ty name
+liftForAlls ty = foldr TyForAll res tyNames
+  where (tyNames, res) = liftForAlls' ty
 
+liftForAlls' :: Ty name -> ([name], Ty name)
+liftForAlls' (TyVar name) = ([], TyVar name)
+liftForAlls' (TyForAll name body) = (name:names, body')
+  where (names, body') = liftForAlls' body
+liftForAlls' (TyArrow t1 t2) = (n1 ++ n2, TyArrow t1' t2')
+  where (n1, t1') = liftForAlls' t1
+        (n2, t2') = liftForAlls' t2
 
+isTyEquivalent :: Ord name => Ty name -> Ty name -> Bool
+isTyEquivalent t1 t2
+  | t1 == t2 = True
+  | otherwise = case (t1, t2) of
+      (TyForAll n1 t1', TyForAll n2 t2') -> (n1, t1') `areForAllsEquivalent` (n2, t2')
+      _ -> False
+
+areForAllsEquivalent :: Ord name => (name, Ty name) -> (name, Ty name) -> Bool
+areForAllsEquivalent (n1, t1) (n2, t2) = t1 == substituteTy (TyVar n1) n2 t2
+
+tyUnique :: Typecheck name name
+tyUnique = getTyUniques >>= tyUnique'
+    where tyUnique' (u:us) = setTyUniques us $> u
+          tyUnique' _ = throwError ImpossibleError
+
 tyMismatchError
-  :: (Pretty t1, Pretty t2)
-  => t1
-  -> t2
-  -> LambdaException
+  :: Pretty ty => ty -> ty -> LambdaException
 tyMismatchError expected actual
   = TyMismatchError
   $ "Couldn't match expected type "
   <> prettyPrint expected
   <> " with actual type "
   <> prettyPrint actual
+
+tyAppMismatchError
+  :: (Ord name, Pretty name)
+  => Context name
+  -> SystemFExpr name
+  -> Ty name
+  -> Typecheck name LambdaException
+tyAppMismatchError ctx expr appTy = tyAppMismatchError' <$> typecheckExpr ctx expr
+  where tyAppMismatchError' actual = TyMismatchError
+          $ "Cannot apply type "
+          <> prettyPrint appTy
+          <> " to non-polymorphic type "
+          <> prettyPrint actual
diff --git a/src/Language/Lambda/Untyped.hs b/src/Language/Lambda/Untyped.hs
--- a/src/Language/Lambda/Untyped.hs
+++ b/src/Language/Lambda/Untyped.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE FlexibleInstances #-}
 module Language.Lambda.Untyped (
   evalText,
   runEvalText,
@@ -25,9 +24,8 @@
 import Language.Lambda.Untyped.State
 
 evalText :: Text -> Eval Text (LambdaExpr Text)
-evalText = either throwParseError evalExpr' . parseExpr
+evalText = either throwParseError evalExpr . parseExpr
   where throwParseError = throwError . ParseError . Text.pack . show
-        evalExpr' = evalExpr
 
 runEvalText
   :: Text
diff --git a/test/Language/Lambda/SystemF/EvalSpec.hs b/test/Language/Lambda/SystemF/EvalSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Language/Lambda/SystemF/EvalSpec.hs
@@ -0,0 +1,247 @@
+module Language.Lambda.SystemF.EvalSpec (spec) where
+
+import RIO
+import RIO.Map (fromList)
+import Test.Hspec
+
+import Language.Lambda.Shared.Errors
+import Language.Lambda.Shared.UniqueSupply (defaultUniques, defaultTyUniques)
+import Language.Lambda.SystemF.Expression
+import Language.Lambda.SystemF.Eval
+import Language.Lambda.SystemF.HspecUtils
+import Language.Lambda.SystemF.State
+
+spec :: Spec
+spec = do
+  let evalExpr' expr = execTypecheck (evalExpr expr) $
+          mkTypecheckState defaultUniques defaultTyUniques
+  
+  describe "evalExpr" $ do
+    it "Does not reduce normal form" $ do
+      "x" `shouldEvalTo` "x"
+
+    it "beta reduces" $ do
+      "(\\x:T. x) y:T" `shouldEvalTo` "y:T"
+      "(\\f:(T->T) x:T. f x) (g:T->T) (y:T)" `shouldEvalTo` "g:(T->T) y:T"
+      "\\x:T. (\\y:T. y) x" `shouldEvalTo` "\\x:T. x"
+      "(\\f:(T->T) x:T. f x) (\\f:T. x:T)" `shouldEvalTo` "\\z:T. x:T"
+
+    it "reduces let bodies" $ do
+      "let x = (\\y:Y. y) z:Y" `shouldEvalTo` "let x = z:Y"
+
+    it "nested let expressions fail" $ do
+      eval "let x = let y = z" `shouldFailWith` isLambdaException
+
+    it "reduces type abstractions to A normal form" $ do
+      "\\T. (\\y:T. y) x:T" `shouldEvalTo` "\\T. x:T"
+
+    it "reduces type applications" $ do
+      "(\\T. x:T) [X]" `shouldEvalTo` "x:X"
+      "(\\x:(forall T. T). x) [X]" `shouldEvalTo` "\\x:X. x"
+      "x:(forall T. T) [X]" `shouldEvalTo` "x:X"
+      "(\\x:(forall T. T). x) (\\X. y:X)" `shouldEvalTo` "\\X. y:X"
+
+  describe "subGlobals" $ do
+    let subGlobals' :: SystemFExpr Text -> SystemFExpr Text
+        subGlobals' expr = unsafeExecTypecheck (subGlobals expr) state
+        state = TypecheckState globals' defaultUniques defaultTyUniques
+        globals' = fromList [("w", TypedExpr (Var "x") (TyVar "X"))]
+    
+    it "subs simple variables" $ do
+      subGlobals' (Var "w")  `shouldBe` Var "x"
+      subGlobals' (VarAnn "w" (TyVar "X"))  `shouldBe` Var "x"
+      
+    it "does not sub shadowed bindings" $ do
+      let expr = Abs "w" (TyVar "W") $ Var "w"
+      subGlobals' expr `shouldBe` expr
+      
+    xit "does not capture globals" $ do
+      let expr = Abs "x" (TyVar "X") $ Var "w"
+      subGlobals' expr `shouldBe` Abs "a" (TyVar "X") (Var "x")
+
+  describe "betaReduce" $ do
+    let betaReduce' :: SystemFExpr Text -> SystemFExpr Text -> SystemFExpr Text
+        betaReduce' e1 e2 = unsafeExecTypecheck (betaReduce e1 e2) $
+          mkTypecheckState defaultUniques defaultTyUniques
+    
+    it "reduces simple applications" $ do
+      let e1 = Abs "x" (TyVar "T") (Var "x")
+          e2 = Var "y"
+
+      betaReduce' e1 e2 `shouldBe` e2
+
+    it "reduces nested abstractions" $ do
+      let e1 = Abs "x" (TyVar "T") (Abs "y" (TyVar "U") (Var "x"))
+          e2 = Var "z"
+      betaReduce' e1 e2 `shouldBe` Abs "y" (TyVar "U") (Var "z")
+
+    it "reduces inner applications" $ do
+      let e1 = Abs "f" (TyArrow (TyVar "T") (TyVar "T")) $
+            App (Var "f") (VarAnn "x" (TyVar "T"))
+          e2 = Var "g"
+      betaReduce' e1 e2 `shouldBe` App (Var "g") (VarAnn "x" (TyVar "T"))
+
+    it "does not reduce unreducible expressions" $ do
+      let e2 = Var "y"
+
+      betaReduce' (Var "x") e2
+        `shouldBe` App (Var "x") (Var "y")
+      betaReduce' (VarAnn "x" (TyVar "T")) e2
+        `shouldBe` App (VarAnn "x" (TyVar "T")) (Var "y")
+      betaReduce' (TyAbs "X" (Var "x")) e2
+        `shouldBe` App (TyAbs "X" (Var "x")) e2
+      betaReduce' (TyApp (Var "x") (TyVar "X")) e2
+        `shouldBe` App (TyApp (Var "x") (TyVar "X")) e2
+
+    it "does not reduce irreducible chained applications" $ do
+      let e1 = App (Var "x") (Var "y")
+          e2 = Var "z"
+      betaReduce' e1 e2 `shouldBe` App (App (Var "x") (Var "y")) (Var "z")
+
+    it "does not sub shadowed bindings" $ do
+      let e1 = Abs "x" (TyVar "T") (Abs "x" (TyVar "U") (Var "x"))
+          e2 = Var "z"
+      betaReduce' e1 e2 `shouldBe` Abs "x" (TyVar "U") (Var "x")
+
+    it "fails to reduce Let" $ do
+      let e1 = Let "x" (Var "x")
+          e2 = Var "z"
+      evaluate (betaReduce' e1 e2) `shouldThrow` isImpossibleError
+
+    it "avoids capture" $ do
+      let beta :: SystemFExpr Text -> SystemFExpr Text -> SystemFExpr Text
+          beta e1 e2 = unsafeExecTypecheck (betaReduce e1 e2) $
+            mkTypecheckState ["z"] defaultTyUniques
+      
+      let e1 = Abs "f" (TyArrow (TyVar "T") (TyVar "U")) $
+            Abs "x" (TyVar "U") $
+              App (Var "f") (Var "x")
+          e2 = Abs "f" (TyVar "T") $ Var "x"
+      beta e1 e2 `shouldBe` Abs "z" (TyVar "U") (Var "x")
+
+  describe "evalTyApp" $ do
+    it "reduces simple type applications" $ do
+      let expr = TyApp
+            (TyAbs "T" (VarAnn "x" (TyVar "T")))
+            (TyVar "X")
+
+      evalExpr' expr `shouldBeRight` VarAnn "x" (TyVar "X")
+
+    it "reduces type applications with abstractions" $ do
+      let expr = TyApp
+            (TyAbs "T" (Abs "x" (TyVar "T") (Var "x")))
+            (TyVar "X")
+
+      evalExpr' expr `shouldBeRight` Abs "x" (TyVar "X") (Var "x")
+
+    it "does not reduce irreducible expressions" $ do
+      let tyApp inner = TyApp (TyAbs "T" inner) (TyVar "X")
+
+      evalExpr' (tyApp (Var "x")) `shouldBeRight` Var "x"
+      evalExpr' (tyApp (VarAnn "x" (TyVar "Z"))) `shouldBeRight` VarAnn "x" (TyVar "Z")
+      evalExpr' (tyApp (Abs "x" (TyVar "Z") (Var "x")))
+        `shouldBeRight` Abs "x" (TyVar "Z") (Var "x")
+
+    it "fails on let" $ do
+      let expr = TyApp (Let "x" (VarAnn "y" (TyVar "T"))) (TyVar "X")
+      evalExpr' expr `shouldSatisfy` either isLetError (const False)
+
+    it "reduces nested expressions" $ do
+      let tyApp inner = TyApp (TyAbs "T" inner) (TyVar "X")
+      
+      let e1 = App (Var "f") (VarAnn "x" (TyVar "T"))
+      evalExpr' (tyApp e1) `shouldBeRight` App (Var "f") (VarAnn "x" $ TyVar "X")
+
+      let e2 = Abs "x" (TyVar "U") (VarAnn "t" $ TyVar "T")
+      evalExpr' (tyApp e2) `shouldBeRight` Abs "x" (TyVar "U") (VarAnn "t" $ TyVar "X")
+
+      let e3 = TyAbs "U" $ VarAnn "x" (TyVar "T")
+      evalExpr' (tyApp e3) `shouldBeRight` TyAbs "U" (VarAnn "x" $ TyVar "X")
+
+      let e4 = TyApp (VarAnn "x" (TyVar "T")) (TyVar "U")
+      evalExpr' (tyApp e4) `shouldBeRight` TyApp (VarAnn "x" $ TyVar "X") (TyVar "U")
+
+      let e5 = TyApp
+            (TyAbs "U" $ VarAnn "x" (TyVar "U"))
+            (TyVar "T")
+      evalExpr' (tyApp e5) `shouldBeRight` VarAnn "x" (TyVar "X")
+
+    it "reduces in nested types" $ do
+      let tyApp inner = TyApp (TyAbs "T" inner) (TyVar "X")
+
+      let e1 = VarAnn "f" $ TyArrow (TyVar "T") (TyVar "U")
+      evalExpr' (tyApp e1) `shouldBeRight` VarAnn "f" (TyArrow (TyVar "X") (TyVar "U"))
+
+      let e2 = VarAnn "f" $ TyForAll "T" (TyVar "T")
+      evalExpr' (tyApp e2) `shouldBeRight` e2
+
+      let e3 = VarAnn "f" $ TyForAll "U" (TyVar "T")
+      evalExpr' (tyApp e3) `shouldBeRight` VarAnn "f" (TyForAll "U" (TyVar "X"))
+                
+
+  describe "alphaConvert" $ do
+    let alphaConvert' :: [Text] -> [Text] -> SystemFExpr Text -> SystemFExpr Text
+        alphaConvert' uniques' fvs expr = unsafeExecTypecheck (alphaConvert fvs expr) $
+          mkTypecheckState uniques' defaultTyUniques
+    
+    it "alpha converts simple expressions" $ do
+      let freeVars = ["x"] :: [Text]
+          expr = Abs "x" (TyVar "T") (Var "x")
+          uniques' = ["y"]
+      alphaConvert' uniques' freeVars expr `shouldBe` Abs "y" (TyVar "T") (Var "y")
+
+    it "avoids captures" $ do
+      let freeVars = ["x"]
+          expr = Abs "x" (TyVar "T") (Var "x")
+          uniques' = ["x", "y"]
+      alphaConvert' uniques' freeVars expr `shouldBe` Abs "y" (TyVar "T") (Var "y")
+
+  describe "etaConvert" $ do
+    it "eta converts simple expressions" $ do
+      let expr :: SystemFExpr Text
+          expr = Abs "x" (TyVar "T") $ App (Var "f") (Var "x")
+      etaConvert expr `shouldBe` Var "f"
+      
+    it "eta converts nested applications" $ do
+      let expr1 :: SystemFExpr Text
+          expr1 = Abs "y" (TyVar "T")  $ App (App (Var "f") (Var "x")) (Var "y")
+      etaConvert expr1 `shouldBe` App (Var "f") (Var "x")
+
+      let expr2 :: SystemFExpr Text
+          expr2 = Abs "x" (TyArrow (TyVar "T") (TyVar "T")) $
+            Abs "y" (TyVar "T") $
+              App (App (Var "f") (Var "x")) (Var "y")
+      etaConvert expr2 `shouldBe` Var "f" 
+
+      let expr3 :: SystemFExpr Text
+          expr3 = Abs "x" (TyVar "T") $
+            Abs "y" (TyArrow (TyVar "T") (TyVar "T")) $
+              App (Var "y") (Var "x")
+      etaConvert expr3 `shouldBe` expr3
+
+      let expr4 :: SystemFExpr Text
+          expr4 = Abs "f" (TyVar "T") $
+            Abs "x" (TyVar "T") (Var "x")
+      etaConvert expr4 `shouldBe` expr4
+      
+    it "ignores non-eta convertable expressions" $ do
+      let expr :: SystemFExpr Text
+          expr = Abs "x" (TyVar "T") $ Var "x"
+      etaConvert expr `shouldBe` expr
+
+  describe "freeVarsOf" $ do
+    let freeVarsOf' :: SystemFExpr Text -> [Text]
+        freeVarsOf' = freeVarsOf
+    
+    it "Returns simple vars" $ do
+      freeVarsOf' (Var "x") `shouldBe` ["x"]
+      freeVarsOf' (VarAnn "x" (TyVar "T")) `shouldBe` ["x"]
+      
+    it "Does not return bound vars" $ 
+      freeVarsOf' (Abs "x" (TyVar "T") (Var "x")) `shouldBe` []
+      
+    it "Returns nested simple vars" $
+      freeVarsOf' (Abs "x" (TyVar "T") (Var "y")) `shouldBe` ["y"]
+                                                             
+    it "Returns applied simple vars" $
+      freeVarsOf' (App (Var "x") (Var "y")) `shouldBe` ["x", "y"]
diff --git a/test/Language/Lambda/SystemF/Examples/BoolSpec.hs b/test/Language/Lambda/SystemF/Examples/BoolSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Language/Lambda/SystemF/Examples/BoolSpec.hs
@@ -0,0 +1,30 @@
+module Language.Lambda.SystemF.Examples.BoolSpec where
+
+import RIO
+import Test.Hspec
+
+import Language.Lambda.SystemF.HspecUtils
+
+spec :: Spec
+spec = describe "Bool" $ do
+  -- Bool is the definition of Booleans. We represent bools
+  -- using Church Encodings:
+  --
+  -- true:  \T. \t:T f:T. t
+  -- false: \T. \t:T f:T. f
+  -- false: \T. \t:T f:T. f
+  describe "not" $ do
+    -- not takes a Bool and returns its opposite value
+    --
+    -- not(true)  = false
+    -- not(false) = true
+    --
+    -- not is defined by
+    -- not = \x. x (\t f. f) (\t f. t)
+    it "not true = false" $
+      "(\\x:(forall T. T -> T -> T). \\X. \\t:X f:X. (x [X]) f t) (\\U. \\t:U f:U. t)"
+        `shouldEvalTo` "\\X. \\t:X f:X. f"
+
+    it "not false = true" $
+      "(\\x:(forall T. T-> T -> T). \\X. \\t:X f:X. (x [X]) f t) (\\U. \\t:U f:U. f)"
+        `shouldEvalTo` "\\X. \\t:X f:X. t"
diff --git a/test/Language/Lambda/SystemF/Examples/NatSpec.hs b/test/Language/Lambda/SystemF/Examples/NatSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Language/Lambda/SystemF/Examples/NatSpec.hs
@@ -0,0 +1,75 @@
+module Language.Lambda.SystemF.Examples.NatSpec where
+
+import RIO
+import Test.Hspec
+
+import Language.Lambda.SystemF (evalText)
+import Language.Lambda.SystemF.HspecUtils
+
+spec :: Spec
+spec = describe "Nat" $ do
+  -- Nat is the definition of natural numbers. More precisely, Nat
+  -- is the set of nonnegative integers.  We represent nats using
+  -- Church Encodings:
+  --
+  -- 0: \f:(T->T) x:T. x
+  -- 1: \f:(T->T) x:T. f x
+  -- 2: \f:(T->T) x:T. f (f x)
+  -- ...and so on
+
+  describe "successor" $ do
+    -- successor is a function that adds 1
+    -- succ(0) = 1
+    -- succ(1) = 2
+    -- ... and so forth
+    --
+    -- successor is defined by
+    -- succ = \n:((T->T)->T->T) f:(T->T) x:T. f (n f x)
+    it "succ 0 = 1" $ do
+      "(\\n:((T->T)->T->T) f:(T->T) x:T. f (n f x)) (\\f:(T->T) x:T. x)"
+        `shouldEvalTo` "\\f:(T->T) x:T. f x"
+
+    it "succ 1 = 2" $
+      "(\\n:((T->T)->T->T) f:(T->T) x:T. f (n f x)) (\\f:(T->T) x:T. f x)"
+        `shouldEvalTo` "\\f:(T->T) x:T. f (f x)"
+
+  describe "add" $ do
+    -- add(m, n) = m + n
+    --
+    -- It is defined by applying successor m times on n:
+    -- add = \m:((T->T)->T->T) n:((T->T)->T->T) f:(T->T) x:T. m f (n f x)
+    it "add 0 2 = 2" $
+      "(\\m:((T->T)->T->T) n:((T->T)->T->T) f:(T->T) x:T. m f (n f x)) (\\f:(T->T) x:T. x) (\\f:(T->T) x:T. f (f x))"
+        `shouldEvalTo` "\\f:(T->T) x:T. f (f x)"
+
+    it "add 3 2 = 5" $
+      "(\\m:((T->T)->T->T) n:((T->T)->T->T) f:(T->T) x:T. m f (n f x)) (\\f:(T->T) x:T. f (f (f x))) (\\f:(T->T) x:T. f (f x))"
+        `shouldEvalTo` "\\f:(T->T) x:T. f (f (f (f (f x))))"
+
+    it "add 0 n = n" $
+      "(\\m:((T->T)->T->T) n:((T->T)->T->T) f:(T->T) x:T. m f (n f x)) (\\f:(T->T) x:T. x) n:((T->T)->T->T)"
+        `shouldEvalTo` "\\f:(T->T) x:T. n:((T->T)->T->T) f x"
+
+  describe "multiply" $ do
+    -- multiply(m, n) = m * n
+    --
+    -- multiply is defined by applying add m times
+    -- multiply = \m n f x. m (n f x) x)
+    --
+    -- Using eta conversion, we can omit the parameter x
+    -- multiply = \m n f. m (n f)
+    it "multiply 0 2 = 0" $
+      "(\\m:((T->T)->T->T) n:((T->T)->T->T) f:(T->T). m (n f)) (\\f:(T->T) x:T. x) (\\f:(T->T) x:T. f (f x))"
+        `shouldEvalTo` "\\f:(T->T) x:T. x"
+
+    it "multiply 2 3 = 6" $
+      "(\\m:((T->T)->T->T) n:((T->T)->T->T) f:(T->T). m (n f)) (\\f:(T->T) x:T. f (f x)) (\\f:(T->T) x:T. f (f (f x)))"
+        `shouldEvalTo` "\\f:(T->T) x:T. f (f (f (f (f (f x)))))"
+
+    it "multiply 0 n = 0" $
+      "(\\m:((T->T)->T->T) n:((T->T)->T->T) f:(T->T). m (n f)) (\\f:(T->T) x:T. x) n:((T->T)->T->T)"
+        `shouldEvalTo` "\\f:(T->T) x:T. x"
+
+    it "multiply 1 n = n" $
+      "(\\m:((T->T)->T->T) n:((T->T)->T->T) f:(T->T). m (n f)) (\\f:(T->T) x:T. f x) n:((T->T)->T->T)"
+        `shouldEvalTo` "\\f:(T->T) x:T. n:((T->T)->T->T) f x"
diff --git a/test/Language/Lambda/SystemF/ExpressionSpec.hs b/test/Language/Lambda/SystemF/ExpressionSpec.hs
--- a/test/Language/Lambda/SystemF/ExpressionSpec.hs
+++ b/test/Language/Lambda/SystemF/ExpressionSpec.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE OverloadedStrings, NoImplicitPrelude #-}
 module Language.Lambda.SystemF.ExpressionSpec where
 
 import RIO
@@ -7,81 +6,125 @@
 import Language.Lambda.SystemF.Expression
 
 spec :: Spec
-spec = describe "prettyPrint" $ do
-  let prettyPrint' :: SystemFExpr Text Text -> Text
-      prettyPrint' = prettyPrint
+spec = do
+  describe "prettyPrint" $ do
+    let prettyPrint' :: SystemFExpr Text -> Text
+        prettyPrint' = prettyPrint
 
-      prettyPrintTy :: Ty Text -> Text
-      prettyPrintTy = prettyPrint
+        prettyPrintTy :: Ty Text -> Text
+        prettyPrintTy = prettyPrint
   
-  it "prints simple variables" $
-    prettyPrint' (Var "x") `shouldBe` "x"
+    it "prints simple variables" $
+      prettyPrint' (Var "x") `shouldBe` "x"
 
-  it "prints simple applications" $
-    prettyPrint' (App (Var "a") (Var "b")) `shouldBe` "a b"
+    it "prints annotated variables" $
+      prettyPrint' (VarAnn "x" (TyVar "T")) `shouldBe` "x:T"
 
-  it "prints simple abstractions" $ 
-    prettyPrint' (Abs "x" (TyVar "T") (Var "x")) `shouldBe` "λ x:T. x"
+    it "prints simple applications" $
+      prettyPrint' (App (Var "a") (Var "b")) `shouldBe` "a b"
 
-  it "prints simple type abstractions" $
-    prettyPrint' (TyAbs "X" (Var "x")) `shouldBe` "Λ X. x"
+    it "prints simple abstractions" $ 
+      prettyPrint' (Abs "x" (TyVar "T") (Var "x")) `shouldBe` "λ x:T. x"
 
-  it "prints simple type applications" $ 
-    prettyPrint' (TyApp (Var "t") (TyVar "T")) `shouldBe` "t [T]"
+    it "prints simple type abstractions" $
+      prettyPrint' (TyAbs "X" (Var "x")) `shouldBe` "Λ X. x"
 
-  it "prints nested abstractions" $
-    prettyPrint' (Abs "f" (TyVar "F") (Abs "x" (TyVar "X") (Var "x")))
-      `shouldBe` "λ f:F x:X. x"
+    it "prints simple type applications" $ 
+      prettyPrint' (TyApp (Var "t") (TyVar "T")) `shouldBe` "t [T]"
 
-  it "prints abstractions with composite types" $ do
-    prettyPrint' (Abs "f" (TyArrow (TyVar "X") (TyVar "Y")) (Var "f"))
-      `shouldBe ` "λ f:(X->Y). f"
+    it "prints simple let expressions" $
+      prettyPrint' (Let "x" (Var "y")) `shouldBe` "let x = y"
 
-    prettyPrint' (Abs "f" (TyArrow (TyVar "X") (TyArrow (TyVar "Y") (TyVar "Z"))) (Var "f"))
-      `shouldBe ` "λ f:(X->Y->Z). f"
+    it "prints annotated variables with composite types" $
+      prettyPrint' (VarAnn "x" (TyArrow (TyVar "T") (TyVar "V"))) `shouldBe` "x:(T->V)"
 
-  it "prints nested type abstractions" $
-    prettyPrint' (TyAbs "A" (TyAbs "B" (Var "x")))
-      `shouldBe` "Λ A B. x"
+    it "prints nested abstractions" $
+      prettyPrint' (Abs "f" (TyVar "F") (Abs "x" (TyVar "X") (Var "x")))
+        `shouldBe` "λ f:F x:X. x"
 
-  it "prints nested applications" $
-    prettyPrint' (App (App (Var "f") (Var "x")) (Var "y"))
-      `shouldBe` "f x y"
+    it "prints abstractions with composite types" $ do
+      prettyPrint' (Abs "f" (TyArrow (TyVar "X") (TyVar "Y")) (Var "f"))
+        `shouldBe ` "λ f:(X->Y). f"
 
-  it "prints parenthesized applications" $ do
-    prettyPrint' (App (Var "w") (App (Var "x") (Var "y")))
-      `shouldBe` "w (x y)"
+      prettyPrint' (Abs "f" (TyArrow (TyVar "X") (TyArrow (TyVar "Y") (TyVar "Z"))) (Var "f"))
+        `shouldBe ` "λ f:(X->Y->Z). f"
 
-    prettyPrint' (App (Abs "t" (TyVar "T") (Var "t")) (Var "x"))
-      `shouldBe` "(λ t:T. t) x"
+    it "prints nested type abstractions" $
+      prettyPrint' (TyAbs "A" (TyAbs "B" (Var "x")))
+        `shouldBe` "Λ A B. x"
 
-    prettyPrint' (App (Abs "f" (TyVar "F") (Var "f")) (Abs "g" (TyVar "G") (Var "g")))
-      `shouldBe` "(λ f:F. f) (λ g:G. g)"
+    it "prints nested applications" $
+      prettyPrint' (App (App (Var "f") (Var "x")) (Var "y"))
+        `shouldBe` "f x y"
 
-  it "prints simple types" $
-    prettyPrintTy (TyVar "X") `shouldBe` "X"
+    it "prints parenthesized applications" $ do
+      prettyPrint' (App (Var "w") (App (Var "x") (Var "y")))
+        `shouldBe` "w (x y)"
 
-  it "print simple arrow types" $
-    prettyPrintTy (TyArrow (TyVar "A") (TyVar "B")) `shouldBe` "A -> B"
+      prettyPrint' (App (Abs "t" (TyVar "T") (Var "t")) (Var "x"))
+        `shouldBe` "(λ t:T. t) x"
 
-  it "prints simple forall types" $
-    prettyPrintTy (TyForAll "X" (TyVar "X")) `shouldBe` "forall X. X"
+      prettyPrint' (App (Abs "f" (TyVar "F") (Var "f")) (Abs "g" (TyVar "G") (Var "g")))
+        `shouldBe` "(λ f:F. f) (λ g:G. g)"
 
-  it "prints chained arrow types" $
-    prettyPrintTy (TyArrow (TyVar "X") (TyArrow (TyVar "Y") (TyVar "Z")))
-      `shouldBe` "X -> Y -> Z"
+    it "prints simple types" $
+      prettyPrintTy (TyVar "X") `shouldBe` "X"
 
-  it "prints nested arrow types" $
-    prettyPrintTy (TyArrow (TyArrow (TyVar "T") (TyVar "U")) (TyVar "V"))
-      `shouldBe` "(T -> U) -> V"
+    it "print simple arrow types" $
+      prettyPrintTy (TyArrow (TyVar "A") (TyVar "B")) `shouldBe` "A -> B"
 
-  it "prints complex forall types" $
-    prettyPrintTy (TyForAll "A" (TyArrow (TyVar "A") (TyVar "A")))
-      `shouldBe` "forall A. A -> A"
+    it "prints simple forall types" $
+      prettyPrintTy (TyForAll "X" (TyVar "X")) `shouldBe` "forall X. X"
 
-  it "prints nested forall types" $
-    prettyPrintTy (TyForAll "W" 
-                  (TyForAll "X" 
-                    (TyArrow (TyVar "W") (TyArrow (TyVar "X") (TyVar "Y")))))
-      `shouldBe` "forall W. forall X. W -> X -> Y"
+    it "prints chained arrow types" $
+      prettyPrintTy (TyArrow (TyVar "X") (TyArrow (TyVar "Y") (TyVar "Z")))
+        `shouldBe` "X -> Y -> Z"
 
+    it "prints nested arrow types" $
+      prettyPrintTy (TyArrow (TyArrow (TyVar "T") (TyVar "U")) (TyVar "V"))
+        `shouldBe` "(T -> U) -> V"
+
+    it "prints complex forall types" $
+      prettyPrintTy (TyForAll "A" (TyArrow (TyVar "A") (TyVar "A")))
+        `shouldBe` "forall A. A -> A"
+
+    it "prints nested forall types" $
+      prettyPrintTy (TyForAll "W" 
+                     (TyForAll "X" 
+                      (TyArrow (TyVar "W") (TyArrow (TyVar "X") (TyVar "Y")))))
+        `shouldBe` "forall W. forall X. W -> X -> Y"
+
+  describe "(==)" $ do
+    let tyvar = "X" :: Text
+    
+    it "same types return true" $ do
+      TyVar tyvar `shouldBe` TyVar tyvar
+      TyArrow (TyVar tyvar) (TyVar tyvar) `shouldBe` TyArrow (TyVar tyvar) (TyVar tyvar)
+      TyForAll tyvar (TyVar tyvar) `shouldBe` TyForAll tyvar (TyVar tyvar)
+
+    it "equivalent foralls return true" $
+      TyForAll tyvar (TyVar tyvar) `shouldBe` TyForAll "Y" (TyVar "Y")
+
+    it "unequal types return false" $ do
+      TyVar tyvar `shouldNotBe` TyVar "Y"
+      TyArrow (TyVar tyvar) (TyVar tyvar) `shouldNotBe` TyArrow (TyVar "Y") (TyVar "Y")
+      TyForAll tyvar (TyVar tyvar) `shouldNotBe` TyForAll tyvar (TyVar "Y")
+      TyVar tyvar `shouldNotBe` TyForAll tyvar (TyVar tyvar)
+
+  describe "substituteTy" $ do
+    let sub :: Ty Text -> Text -> Ty Text -> Ty Text
+        sub = substituteTy
+    
+    it "substititues simple types" $ do
+      sub (TyVar "X") "Y" (TyVar "Y") `shouldBe` TyVar "X"
+      sub (TyVar "X") "Y" (TyVar "Z") `shouldBe` TyVar "Z"
+      sub (TyArrow (TyVar "Z") (TyVar "X")) "Y" (TyVar "Y")
+        `shouldBe` TyArrow (TyVar "Z") (TyVar "X")
+      sub (TyForAll "X" (TyVar "Z")) "Y" (TyVar "Y")
+        `shouldBe` TyForAll "X" (TyVar "Z")
+      sub (TyVar "X") "Y" (TyForAll "Z" (TyVar "Y"))
+        `shouldBe` TyForAll "Z" (TyVar "X")
+
+    it "does not capture foralls" $ do
+      sub (TyVar "X") "Y" (TyForAll "Y" (TyVar "Y"))
+        `shouldBe` TyForAll "Y" (TyVar "Y")
diff --git a/test/Language/Lambda/SystemF/HspecUtils.hs b/test/Language/Lambda/SystemF/HspecUtils.hs
new file mode 100644
--- /dev/null
+++ b/test/Language/Lambda/SystemF/HspecUtils.hs
@@ -0,0 +1,65 @@
+module Language.Lambda.SystemF.HspecUtils where
+
+import Language.Lambda.Shared.Errors
+import Language.Lambda.SystemF
+
+import RIO
+import Test.Hspec
+import qualified RIO.Map as Map
+
+shouldEvalTo :: Text -> Text -> Expectation
+shouldEvalTo input expected = eval input `shouldBe` eval expected
+
+shouldTypecheckTo :: Text -> Text -> Expectation
+shouldTypecheckTo = shouldTypecheckToWithGlobals []
+
+shouldTypecheckToWithGlobals :: [(Text, TypedExpr Text)] -> Text -> Text -> Expectation
+shouldTypecheckToWithGlobals globals expr ty = typecheck' globals expr `shouldHaveType` ty
+
+shouldBeRight
+  :: (Show l, Show r, Eq l, Eq r)
+  => Either l r
+  -> r
+  -> Expectation
+shouldBeRight res = (res `shouldBe`) . Right
+
+shouldBeLeft
+  :: (Show l, Show r, Eq l, Eq r)
+  => Either l r
+  -> l
+  -> Expectation
+shouldBeLeft res = (res `shouldBe`) . Left
+
+shouldHaveType
+  :: Either LambdaException (Ty Text)
+  -> Text
+  -> Expectation
+shouldHaveType res tyRepr = case parseType tyRepr of
+    Left err -> expectationFailure $
+      "Could not parse type " <> show tyRepr <> ": " <> show err
+    Right ty -> res `shouldBe` Right ty
+
+shouldFailWith
+  :: Show a
+  => Either LambdaException a
+  -> Selector LambdaException
+  -> Expectation
+shouldFailWith res selector = case res of
+  Left err -> err `shouldSatisfy` selector
+  Right res' -> expectationFailure $
+        "did not get expected failure: " <> show res'
+
+eval :: Text -> Either LambdaException (TypedExpr Text)
+eval input = execTypecheck (evalText input) initialState
+  where initialState = mkTypecheckState defaultUniques defaultTyUniques
+
+typecheck' :: [(Text, TypedExpr Text)] -> Text -> Either LambdaException (Ty Text)
+typecheck' globals input = execTypecheck (typecheckText input) initialState
+  where initialState = TypecheckState (Map.fromList globals) defaultUniques defaultTyUniques
+
+runTypecheck'
+  :: [(Text, TypedExpr Text)]
+  -> Text
+  -> Either LambdaException (Ty Text, TypecheckState Text)
+runTypecheck' globals input = runTypecheck (typecheckText input) initialState
+  where initialState = TypecheckState (Map.fromList globals) defaultUniques defaultTyUniques
diff --git a/test/Language/Lambda/SystemF/ParserSpec.hs b/test/Language/Lambda/SystemF/ParserSpec.hs
--- a/test/Language/Lambda/SystemF/ParserSpec.hs
+++ b/test/Language/Lambda/SystemF/ParserSpec.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE NoImplicitPrelude, OverloadedStrings #-}
 module Language.Lambda.SystemF.ParserSpec (spec) where
 
 import Data.Either
@@ -7,6 +6,7 @@
 import Test.Hspec
 
 import Language.Lambda.SystemF.Expression
+import Language.Lambda.SystemF.HspecUtils
 import Language.Lambda.SystemF.Parser
 
 spec :: Spec
@@ -15,6 +15,9 @@
     it "parses simple variables" $
       parseExpr "x" `shouldBe` Right (Var "x")
 
+    it "parses annotated variables" $
+      parseExpr "x:T" `shouldBe` Right (VarAnn "x" (TyVar "T"))
+
     it "parses parenthesized variables" $
       parseExpr "(x)" `shouldBe` Right (Var "x")
 
@@ -27,6 +30,11 @@
     it "parses simple type applications" $ 
       parseExpr "x [T]" `shouldBe` Right (TyApp (Var "x") (TyVar "T"))
 
+    it "parses simple lets" $ do
+      parseExpr "let x = t" `shouldBeRight` Let "x" (Var "t")
+      parseExpr "let f = \\x: T. x" `shouldBeRight`
+        Let "f" (Abs "x" (TyVar "T") (Var "x"))
+
     it "parses nested abstractions" $
       parseExpr "\\a:A b:B. b" 
         `shouldBe` Right (Abs "a" (TyVar "A") (Abs "b" (TyVar "B") (Var "b")))
@@ -56,6 +64,9 @@
     it "does not parse trailing errors" $
       parseExpr "x +" `shouldSatisfy` isLeft
 
+    it "does not parse misplaced lets" $
+      parseExpr "\\x: T. let y = x" `shouldSatisfy` isLeft
+
     it "ignores whitespace" $ do
       let exprs = [
             " x ",
@@ -84,3 +95,8 @@
 
       parseType "(W -> V) -> U"
         `shouldBe` Right (TyArrow (TyArrow (TyVar "W") (TyVar "V")) (TyVar "U"))
+
+    it "parses forall types" $ do
+      parseType "forall T. T" `shouldBeRight` TyForAll "T" (TyVar "T")
+      parseType "forall T U. T->U"
+        `shouldBeRight` TyForAll "T" (TyForAll "U" (TyArrow (TyVar "T") (TyVar "U")))
diff --git a/test/Language/Lambda/SystemF/TypeCheckSpec.hs b/test/Language/Lambda/SystemF/TypeCheckSpec.hs
--- a/test/Language/Lambda/SystemF/TypeCheckSpec.hs
+++ b/test/Language/Lambda/SystemF/TypeCheckSpec.hs
@@ -1,71 +1,92 @@
 module Language.Lambda.SystemF.TypeCheckSpec (spec) where
 
-import Data.Either
-import Data.Map
-import Prettyprinter
-import Test.Hspec
-
 import Language.Lambda.Shared.Errors
 import Language.Lambda.SystemF.Expression
 import Language.Lambda.SystemF.State
-import Language.Lambda.SystemF.TypeCheck
+import Language.Lambda.SystemF.HspecUtils
 
-tc uniqs ctx expr = execTypecheck (typecheck expr) (TypecheckState (fromList ctx) uniqs)
+import Control.Monad.Except
+import Data.Map
+import Lens.Micro
+import RIO
+import Test.Hspec
 
 spec :: Spec
 spec = describe "typecheck" $ do
-  it "typechecks simple variables in context" $
-    tc [] [("x", TyVar "X")] (Var "x") `shouldBe` Right (TyVar "X")
+  let someGlobal = ("x", TypedExpr (Var "y") (TyVar "X"))
+  
+  it "typechecks simple variables" $ do
+    typecheck' [someGlobal] "x" `shouldHaveType` "X"
+    typecheck' [] "x" `shouldHaveType` "Z"
 
-  it "typechecks simple variables not in context" $ 
-    tc ["A"] [] (Var "x") `shouldBe` Right (TyVar "A")
+  it "typechecks annotated variables" $ do
+    typecheck' [someGlobal] "x:X" `shouldHaveType` "X"
+    typecheck' [someGlobal] "x:X" `shouldHaveType` "X"
 
-  it "typechecks simple abstractions" $
-    tc [] [] (Abs "x" (TyVar "A") (Var "x")) 
-      `shouldBe` Right (TyArrow (TyVar "A") (TyVar "A"))
+    typecheck' [someGlobal] "x:Y" `shouldFailWith` isTyMismatchError
 
-  it "typechecks simple applications" $ do
-    let ctx = [
-          ("f", TyArrow (TyVar "T") (TyVar "U")),
-          ("a", TyVar "T")
-          ]
+  it "typechecks abstractions" $
+    typecheck' [] "\\x:A. x" `shouldHaveType` "A -> A"
 
-    tc [] ctx (App (Var "f") (Var "a")) `shouldBe` Right (TyVar "U")
+  it "typechecks applications" $ do
+    let globals'
+          = [ ("f", TypedExpr (Var "f") $ TyArrow (TyVar "T") (TyVar "U")),
+              ("a", TypedExpr (Var "a") $ TyVar "T"),
+              ("b", TypedExpr (Var "b") (TyVar "B"))
+            ]
 
-  it "apply variable to variable fails" $ do
-    let ctx = [
-          ("a", TyVar "A"),
-          ("b", TyVar "B")
-          ]
+    typecheck' globals' "f a" `shouldHaveType` "U"
+    typecheck' [] "(\\t: T. t) x:T" `shouldHaveType` "T"
 
-    tc ["C"] ctx (App (Var "a") (Var "b")) 
-      `shouldSatisfy` isLeft
+    -- Polymorphic application
+    typecheck' [] "\\x:(forall T. T). x"
+      `shouldHaveType` "forall T. T -> T"
+    typecheck' [] "\\x:(forall T. T->U). x"
+      `shouldHaveType` "forall T. (T -> U) -> (T -> U)"
+    typecheck' [] "\\x:(U->(forall T. T)). x"
+      `shouldHaveType` "forall T. (U -> T) -> (U -> T)"
+    typecheck' [] "\\x:(forall T. T). x:T"
+      `shouldHaveType` "forall T. T -> T"
+    typecheck' [] "(\\z:(forall X. X). z) (\\X. a:X)"
+      `shouldHaveType` "forall X. X"
+    typecheck' [] "(\\x:(forall T. T). x) (\\X. y:X)"
+      `shouldHaveType` "forall X. X"
 
-  it "apply arrow to variable of wrong type fails" $ do
-    let ctx = [
-          ("f", TyArrow (TyVar "F") (TyVar "G")),
-          ("b", TyVar "B")
-          ]
+    typecheck' globals' "a b" `shouldFailWith` isTyMismatchError
+    typecheck' globals' "f b" `shouldFailWith` isTyMismatchError
 
-    tc [] ctx (App (Var "f") (Var "b")) `shouldSatisfy` isLeft
+  it "typechecks let expressions" $ do
+    typecheck' [] "let x = y" `shouldHaveType` "Z"
+    typecheck' [] "\\x:T. let y = z" `shouldFailWith` isLambdaException
 
-  it "typechecks simple type abstractions" $
-    tc ["A"] [] (TyAbs "X" (Var "x")) `shouldBe` Right (TyForAll "X" (TyVar "A"))
+  it "typechecks type abstractions" $ do
+    typecheck' [] "\\X. (\\x:X. x)" `shouldHaveType` "forall X. X->X"
+    typecheck' [] "\\X. x" `shouldHaveType` "forall X. Z"
 
-  it "typechecks type abstractions with simple abstraction" $
-    tc [] [] (TyAbs "X" (Abs "x" (TyVar "X") (Var "x"))) 
-      `shouldBe` Right (TyForAll "X" (TyArrow (TyVar "X") (TyVar "X")))
+  it "typechecks type applications" $ do
+    let globals'
+          = [ ("y", TypedExpr (Var "y") (TyVar "Y")),
+              ("x", TypedExpr (Var "x") $ TyVar "A")]
 
-  it "typechecks type abstractions with application" $
-    tc [] [("y", TyVar "Y")] 
-      (App (TyApp (TyAbs "X" (Abs "x" (TyVar "X") (Var "x"))) (TyVar "Y")) 
-           (Var "y"))
-      `shouldBe` Right (TyVar "Y")
+    typecheck' globals' "((\\X.\\x:X.x) [Y]) y" `shouldHaveType` "Y"
+    typecheck' globals' "(\\X. x) [T]" `shouldHaveType` "A"
+    typecheck' globals' "(\\X. z: X) [T]" `shouldHaveType` "T"
+    typecheck' globals' "(\\X. (\\x:X. x)) [Y]" `shouldHaveType` "Y -> Y"
+    typecheck' globals' "(z:forall X. X) [Y]" `shouldHaveType` "Y"
+    typecheck' globals' "\\x:(forall X. X). x [Y]" `shouldHaveType` "forall X. X -> Y"
+    
+  
+    typecheck' [] "x:T [U]" `shouldFailWith` isTyMismatchError
+    typecheck' globals' "x [U]" `shouldFailWith` isTyMismatchError
 
-  it "typechecks simple type applications" $
-    tc [] [("x", TyVar "A")] (TyApp (TyAbs "X" (Var "x")) (TyVar "X"))
-      `shouldBe` Right (TyVar "A")
+  it "doesn't modify context" $ do
+    let exprs
+          = [ "\\x:A. x",
+              "\\X. x" ]
 
-  it "typechecks type applications with simple abstraction" $
-    tc [] [] (TyApp (TyAbs "X" (Abs "x" (TyVar "X") (Var "x"))) (TyVar "Y"))
-      `shouldBe` Right (TyArrow (TyVar "Y") (TyVar "Y"))
+    forM_ exprs $ \expr -> do
+      let ctx = do
+            (_, state) <- runTypecheck' [] expr
+            pure $ state ^. _context
+      
+      ctx `shouldBeRight` empty
diff --git a/test/Language/Lambda/SystemFSpec.hs b/test/Language/Lambda/SystemFSpec.hs
--- a/test/Language/Lambda/SystemFSpec.hs
+++ b/test/Language/Lambda/SystemFSpec.hs
@@ -1,9 +1,116 @@
 module Language.Lambda.SystemFSpec where
 
-import Test.Hspec
-
+import Language.Lambda.Shared.Errors (LambdaException(..), isLambdaException)
 import Language.Lambda.SystemF
+import Language.Lambda.SystemF.HspecUtils
 
+import Lens.Micro
+import RIO
+import RIO.Map (empty, fromList)
+import Test.Hspec
+
 spec :: Spec
-spec = describe "evalString" $ 
-  return ()
+spec = do
+  describe "evalText" $ do
+    let eval' :: Text -> Either LambdaException (SystemFExpr Text)
+        eval' = over _Right (^. _expr) . eval
+
+    it "evaluates simple text" $ do
+      eval' "x" `shouldBeRight` Var "x"
+      eval' "\\x:T. x" `shouldBeRight` Abs "x" (TyVar "T") (Var "x")
+      eval' "\\X. x" `shouldBeRight` TyAbs "X" (Var "x")
+
+    it "reduces simple applications" $
+      eval' "(\\x:T. x) y:T" `shouldBeRight` VarAnn "y" (TyVar "T")
+
+    it "reduces applications with nested redexes" $
+      eval' "(\\f:T->T x:T. f x) (\\y:T. y)"
+        `shouldBeRight` Abs "x" (TyVar "T") (Var "x")
+
+    it "lets update state" $ do
+      let act = evalText "let x = a: A" >> evalText "x"
+
+      unsafeExecTypecheck act (mkTypecheckState [] [])
+        `shouldBe` TypedExpr (VarAnn "a" (TyVar "A")) (TyVar "A")
+
+  describe "runEvalText" $ do
+    let runEvalText' input = extract $ runEvalText input empty
+        extract = _Right %~ (^. _expr) . fst
+    
+    it "evaluates simple text" $ do
+      runEvalText' "x" `shouldBeRight` Var "x"
+      runEvalText' "\\x:T. x" `shouldBeRight` Abs "x" (TyVar "T") (Var "x")
+      runEvalText' "\\X. x" `shouldBeRight` TyAbs "X" (Var "x")
+
+  describe "execEvalText" $ do
+    let execEvalText' input = extract $ execEvalText input empty
+        extract = over _Right (^. _expr)
+    
+    it "evaluates simple text" $ do
+      execEvalText' "x" `shouldBeRight` Var "x"
+      execEvalText' "\\x:T. x" `shouldBeRight` Abs "x" (TyVar "T") (Var "x")
+      execEvalText' "\\X. x" `shouldBeRight` TyAbs "X" (Var "x")
+
+  describe "unsafeExecEvalText" $ do
+    let unsafeExecEvalText' input = extract $ unsafeExecEvalText input empty
+        extract = (^. _expr)
+
+    it "evaluates simple text" $ do
+      unsafeExecEvalText' "x" `shouldBe` Var "x"
+      unsafeExecEvalText' "\\x:T. x" `shouldBe` Abs "x" (TyVar "T") (Var "x")
+      unsafeExecEvalText' "\\X. x" `shouldBe` TyAbs "X" (Var "x")
+
+    it "throws errors" $ do
+      evaluate (unsafeExecEvalText' "\\x. x") `shouldThrow` isLambdaException
+
+  describe "typecheckText" $ do
+    let tc :: Text -> Either LambdaException (Ty Text)
+        tc input = execTypecheck (typecheckText input) initialState
+
+        initialState = mkTypecheckState defaultUniques defaultTyUniques
+
+    it "typechecks simple text" $ do
+      tc "x" `shouldHaveType` "Z"
+      tc "\\x:T. x" `shouldHaveType` "T -> T"
+      tc "\\X. x" `shouldHaveType` "forall X. Z"
+      tc "(\\x:T. x) y:T" `shouldHaveType` "T"
+      tc "(\\f:(T->T) x:T. f x) (\\y:T. y)" `shouldHaveType` "T -> T"
+
+  describe "runTypecheckText" $ do
+    let tc :: Text -> Either LambdaException (Ty Text)
+        tc input = fst <$> runTypecheckText input globals'
+
+        globals' = fromList [("x", TypedExpr (Var "x") (TyVar "A"))]
+
+    it "typechecks simple text" $ do
+      tc "x" `shouldHaveType` "A"
+      tc "\\x:T. x" `shouldHaveType` "T -> T"
+      tc "\\X. x" `shouldHaveType` "forall X. A"
+      tc "(\\x:T. x) y:T" `shouldHaveType` "T"
+      tc "(\\f:(T->T) x:T. f x) (\\y:T. y)" `shouldHaveType` "T -> T"
+
+  describe "execTypecheckText" $ do
+    let tc :: Text -> Either LambdaException (Ty Text)
+        tc input = execTypecheckText input globals'
+
+        globals' = fromList [("x", TypedExpr (Var "x") (TyVar "A"))]
+
+    it "typechecks simple text" $ do
+      tc "x" `shouldHaveType` "A"
+      tc "\\x:T. x" `shouldHaveType` "T -> T"
+      tc "\\X. x" `shouldHaveType` "forall X. A"
+      tc "(\\x:T. x) y:T" `shouldHaveType` "T"
+      tc "(\\f:(T->T) x:T. f x) (\\y:T. y)" `shouldHaveType` "T -> T"
+
+  describe "unsafeExecTypecheckText" $ do
+    let tc :: Text -> Ty Text
+        tc input = unsafeExecTypecheckText input globals'
+
+        globals' = fromList [("x", TypedExpr (Var "x") (TyVar "A"))]
+
+    it "typechecks simple text" $ do
+      Right (tc "x") `shouldHaveType` "A"
+      Right (tc "\\x:T. x") `shouldHaveType` "T -> T"
+      Right (tc "\\X. x") `shouldHaveType` "forall X. A"
+      Right (tc "(\\x:T. x) y:T") `shouldHaveType` "T"
+      Right (tc "(\\f:(T->T) x:T. f x) (\\y:T. y)") `shouldHaveType` "T -> T"
diff --git a/test/Language/Lambda/Untyped/EvalSpec.hs b/test/Language/Lambda/Untyped/EvalSpec.hs
--- a/test/Language/Lambda/Untyped/EvalSpec.hs
+++ b/test/Language/Lambda/Untyped/EvalSpec.hs
@@ -7,8 +7,6 @@
 
 import Language.Lambda.Shared.Errors
 import Language.Lambda.Untyped
-import Language.Lambda.Untyped.Eval
-import Language.Lambda.Untyped.State
 
 spec :: Spec
 spec = do
@@ -97,6 +95,14 @@
       let e1 = Abs "x" (Abs "x" (Var "x"))
           e2 = Var "z"
       betaReduce' e1 e2 `shouldBe` Abs "x" (Var "x")
+
+    it "avoids captures" $ do
+      let beta :: LambdaExpr Text -> LambdaExpr Text -> LambdaExpr Text
+          beta e1 e2 = unsafeExecEval (betaReduce e1 e2) (mkEvalState ["z"])
+      
+      let e1 = Abs "f" $ Abs "x" $ App (Var "f") (Var "x")
+          e2 = Abs "f" $ Var "x"
+      beta e1 e2 `shouldBe` Abs "z" (Var "x")
 
   describe "alphaConvert" $ do
     let alphaConvert' :: [Text] -> [Text] -> LambdaExpr Text -> LambdaExpr Text
diff --git a/test/Language/Lambda/Untyped/Examples/BoolSpec.hs b/test/Language/Lambda/Untyped/Examples/BoolSpec.hs
--- a/test/Language/Lambda/Untyped/Examples/BoolSpec.hs
+++ b/test/Language/Lambda/Untyped/Examples/BoolSpec.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE NoImplicitPrelude, OverloadedStrings #-}
 module Language.Lambda.Untyped.Examples.BoolSpec where
 
 import RIO
diff --git a/test/Language/Lambda/Untyped/Examples/NatSpec.hs b/test/Language/Lambda/Untyped/Examples/NatSpec.hs
--- a/test/Language/Lambda/Untyped/Examples/NatSpec.hs
+++ b/test/Language/Lambda/Untyped/Examples/NatSpec.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE NoImplicitPrelude, OverloadedStrings #-}
 module Language.Lambda.Untyped.Examples.NatSpec where
 
 import RIO
diff --git a/test/Language/Lambda/Untyped/HspecUtils.hs b/test/Language/Lambda/Untyped/HspecUtils.hs
--- a/test/Language/Lambda/Untyped/HspecUtils.hs
+++ b/test/Language/Lambda/Untyped/HspecUtils.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE NoImplicitPrelude #-}
 module Language.Lambda.Untyped.HspecUtils where
 
 import RIO