diff --git a/app/CliOptions.hs b/app/CliOptions.hs
new file mode 100644
--- /dev/null
+++ b/app/CliOptions.hs
@@ -0,0 +1,41 @@
+module CliOptions
+  ( CliOptions(..),
+    Language(..),
+    parseCliOptions
+  ) where
+
+import RIO
+
+import Options.Applicative hiding (command, ParseError())
+
+data CliOptions = CliOptions {
+  language :: Language,
+  version :: Bool
+}
+
+-- | Supported Languages:
+-- 
+--    * Untyped Lambda Calculus
+--    * System F
+data Language 
+  = Untyped
+  | SystemF
+
+parseCliOptions :: IO CliOptions
+parseCliOptions = execParser opts
+  where opts = info
+          (helper <*> cliParser)
+          (briefDesc <> progDesc "A Lambda Calculus Interpreter")
+
+cliParser :: Parser CliOptions
+cliParser = CliOptions 
+  <$> flag Untyped SystemF language
+  <*> switch version
+  where language = long "system-f"
+          <> short 'f'
+          <> internal -- this is a secret feature
+          <> help "Use the System F interpreter"
+
+        version = long "version"
+          <> short 'v'
+          <> help "Print the version"
diff --git a/app/Main.hs b/app/Main.hs
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -1,107 +1,22 @@
 module Main where
 
-import Data.Version
-
-import Data.Semigroup
-import Options.Applicative hiding (ParseError)
-import System.Console.Shell
-import System.Console.Shell.ShellMonad
-import System.Console.Shell.Backend.Readline (readlineBackend)
-
+import CliOptions (CliOptions(..), parseCliOptions)
+import Repl (runRepl)
 import qualified Paths_lambda_calculator as P
 
-import Language.Lambda
-import Language.Lambda.Util.PrettyPrint
-import Language.SystemF
+import Data.Version
+import RIO
 
 main :: IO ()
-main = execParser opts >>= runShell'
-  where opts = info (helper <*> cliParser)
-                    (briefDesc <> progDesc "A Lambda Calculus Interpreter")
-
--- Option Parsing
-data CliOptions = CliOptions {
-  language :: Eval Language,
-  version :: Bool
-  }
-
--- Supported Languages:
--- 
---  * Untyped Lambda Calculus
---  * System F
-data Language 
-  = Untyped
-  | SystemF
-
--- The result of an evaluation
-type Result a = Either a -- An error
-                       a -- The result
-
--- Represent a language together with its evaluation function
-data Eval a = Eval a (String -> Result String)
-
-untyped :: Eval Language
-untyped = Eval Untyped eval
-  where eval = fromEvalString Language.Lambda.evalString
-
-systemf :: Eval Language
-systemf = Eval SystemF eval
-  where eval = fromEvalString Language.SystemF.evalString
-
--- Take a typed evaluation function and return a function that returns a result
--- 
--- For example:
---   (String -> Either ParseError (LambdaExpr String)) -> (String -> Result String)
---   (String -> Either ParseError (SystemFExpr String String)) -> (String -> Result String)
-fromEvalString :: (Show s, PrettyPrint p)
-               => (String -> Either s p)
-               -> (String -> Result String)
-fromEvalString f = either (Left . show) (Right . prettyPrint) . f
-
-cliParser :: Parser CliOptions
-cliParser = CliOptions 
-  <$> flag untyped systemf (long "system-f" <> 
-                            short 'f' <> 
-                            internal <>    -- this is a secret feature
-                            help "Use the System F interpreter")
-
-  <*> switch (long "version" <> 
-              short 'v' <> 
-              help "Print the version")
-
--- Interactive Shell
-runShell' :: CliOptions -> IO ()
-runShell' CliOptions{version=True} = putStrLn version'
-runShell' CliOptions{language=Eval lang eval} 
-  = runShell (mkShellDesc lang eval) readlineBackend ()
-
-mkShellDesc :: Language 
-            -> (String -> Result String)
-            -> ShellDescription ()
-mkShellDesc language f = shellDesc' $ mkShellDescription commands (eval f)
-  where shellDesc' d = d {
-          greetingText = Just shellGreeting,
-          prompt = shellPrompt language
-          }
-
-shellGreeting :: String
-shellGreeting = "Lambda Calculator (" ++ version' ++ ")\nType :h for help\n"
-  
-shellPrompt :: Language -> s -> IO String
-shellPrompt language _ = return $ prefix language : " > "
-  where prefix Untyped = lambda
-        prefix SystemF = upperLambda
-
-commands :: [ShellCommand s]
-commands = [
-  exitCommand "q",
-  helpCommand "h"
-  ]
-
-eval :: (String -> Result String) -> String -> Sh s' ()
-eval f = either shellPutErrLn shellPutStrLn . f
+main = runSimpleApp $ do
+  CliOptions{..} <- liftIO parseCliOptions
 
--- Get the current version
-version' :: String
-version' = showVersion P.version
- 
+  if version
+    then
+      logInfo $ "Lambda Calculator (" <> version' <> ")"
+    else
+      liftIO $ runRepl language
+    
+-- | Get the current version
+version' :: Utf8Builder
+version' = fromString $ showVersion P.version
diff --git a/app/Repl.hs b/app/Repl.hs
new file mode 100644
--- /dev/null
+++ b/app/Repl.hs
@@ -0,0 +1,11 @@
+module Repl (runRepl) where
+
+import CliOptions (Language(..))
+import Repl.SystemF (runSystemFRepl)
+import Repl.Untyped (runUntypedRepl)
+
+import RIO
+
+runRepl :: Language -> IO ()
+runRepl SystemF = runSystemFRepl
+runRepl Untyped = runUntypedRepl
diff --git a/app/Repl/Shared.hs b/app/Repl/Shared.hs
new file mode 100644
--- /dev/null
+++ b/app/Repl/Shared.hs
@@ -0,0 +1,59 @@
+module Repl.Shared where
+
+import CliOptions (Language(..))
+import Paths_lambda_calculator (version)
+import Language.Lambda.Shared.Errors (LambdaException())
+import Language.Lambda.Shared.UniqueSupply (defaultUniques)
+import Language.Lambda.SystemF
+
+import Data.Text (singleton)
+import Data.Text.IO (putStrLn)
+import Data.Version (showVersion)
+import RIO
+import RIO.State
+import RIO.Text (pack, unpack)
+import System.Console.Repline
+import Control.Monad.Except
+import qualified Data.Map as M
+
+mkReplOpts banner command = ReplOpts
+  { banner = banner,
+    command = command,
+    options = commands,
+    prefix = Just ':',
+    multilineCommand = Nothing,
+    tabComplete = Custom completer,
+    initialiser = initializer,
+    finaliser = return Exit
+  }
+
+prompt :: Applicative ap => Text -> HaskelineT ap Text
+prompt prefix = pure $ prefix <> " > "
+
+commands :: (MonadIO m, MonadThrow m) => [(String, String -> HaskelineT m ())]
+commands
+  = [ ("h", help'),
+      ("help", help'),
+      ("q", quit'),
+      ("quit", quit')
+    ]
+  where help' = const helpCommand
+        quit' = const abort
+
+completer :: Monad m => CompletionFunc m
+completer (left, _) = pure (left, []) -- No tab completion
+
+initializer :: MonadIO io => HaskelineT io ()
+initializer = liftIO $ putStrLn greeting
+  where greeting = "Lambda Calculator ("
+          <> version'
+          <> ")\nType :h for help\n"
+
+helpCommand :: MonadIO io => HaskelineT io ()
+helpCommand = liftIO $ putStrLn banner
+  where banner = " Commands available: \n\n"
+          <> "    :help, :h\tShow this help\n"
+          <> "    :quit, :q\tQuit\n"
+
+version' :: Text
+version' = fromString $ showVersion version
diff --git a/app/Repl/SystemF.hs b/app/Repl/SystemF.hs
new file mode 100644
--- /dev/null
+++ b/app/Repl/SystemF.hs
@@ -0,0 +1,40 @@
+module Repl.SystemF (runSystemFRepl) where
+
+import Language.Lambda.Shared.Errors (LambdaException())
+import Language.Lambda.Shared.UniqueSupply (defaultUniques)
+import Language.Lambda.SystemF
+import Repl.Shared
+
+import Data.Text (singleton)
+import Data.Text.IO (putStrLn)
+import RIO
+import RIO.State
+import RIO.Text (pack, unpack)
+import System.Console.Repline
+import Control.Monad.Except (ExceptT(..), runExceptT)
+
+type EvalT name m
+  = StateT (TypecheckState name)
+      (ExceptT LambdaException m)
+
+type Repl a = HaskelineT (EvalT Text IO) a
+
+runSystemFRepl :: IO ()
+runSystemFRepl
+  = void . runExceptT . evalStateT (evalReplOpts replOpts) $ initialState
+  where replOpts = mkReplOpts banner' $ evalSystemF . pack
+        initialState = mkTypecheckState defaultUniques
+
+banner' :: MultiLine -> Repl String
+banner' _ = unpack <$> prompt (singleton upperLambda)
+
+evalSystemF :: Text -> Repl ()
+evalSystemF input = do
+  state' <- get
+
+  let res = runTypecheck (evalText input) state'
+  case res of
+    Left err -> liftIO . putStrLn . pack . show $ err
+    Right (res', newState) -> do
+      put newState
+      liftIO . putStrLn . prettyPrint $ res'
diff --git a/app/Repl/Untyped.hs b/app/Repl/Untyped.hs
new file mode 100644
--- /dev/null
+++ b/app/Repl/Untyped.hs
@@ -0,0 +1,50 @@
+module Repl.Untyped (runUntypedRepl) where
+
+import Language.Lambda.Shared.Errors (LambdaException())
+import Language.Lambda.Shared.UniqueSupply (defaultUniques)
+import Language.Lambda.Untyped
+import Repl.Shared
+
+import Data.Text (singleton)
+import Data.Text.IO (putStrLn)
+import RIO
+import RIO.State
+import RIO.Text (pack, unpack)
+import System.Console.Repline
+import Control.Monad.Except
+
+type EvalT name m
+  = StateT (EvalState name)
+      (ExceptT LambdaException m)
+
+type Repl a = HaskelineT (EvalT Text IO) a
+
+runUntypedRepl :: IO ()
+runUntypedRepl
+  = void . runExceptT . evalStateT (evalReplOpts replOpts) $ initialState
+  where replOpts = ReplOpts
+          { banner = const $ unpack <$> prompt',
+            command = evalLambda . pack,
+            options = commands,
+            prefix = Just ':',
+            multilineCommand = Nothing,
+            tabComplete = Custom completer,
+            initialiser = initializer,
+            finaliser = return Exit
+          }
+
+        initialState = mkEvalState defaultUniques
+
+prompt' :: Repl Text
+prompt' = prompt $ singleton lambda
+
+evalLambda :: Text -> Repl ()
+evalLambda input = do
+  state' <- get
+  
+  let res = runEval (evalText input) state'
+  case res of
+    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,84 +1,269 @@
-name:                lambda-calculator
-version:             2.0.0
-synopsis:            A lambda calculus interpreter
-description:         Please see README.md
-homepage:            https://github.com/sgillespie/lambda-calculus#readme
-license:             MIT
-license-file:        LICENSE
-author:              Sean D Gillespie
-maintainer:          sean@mistersg.net
-copyright:           2016 Sean Gillespie
-category:            LambdaCalculus,Language,Teaching
-build-type:          Simple
--- extra-source-files:
-cabal-version:       >=1.10
-
-library
-  hs-source-dirs:      src
-  exposed-modules:     Language.Lambda,
-                       Language.Lambda.Expression,
-                       Language.Lambda.Eval,
-                       Language.Lambda.Parser,
-
-                       Language.Lambda.Util.PrettyPrint,
+cabal-version: 1.12
 
-                       Language.SystemF,
-                       Language.SystemF.Expression,
-                       Language.SystemF.Parser,
-                       Language.SystemF.TypeCheck
-  build-depends:       base >= 4.9 && < 5,
-                       containers,
-                       parsec
-  default-language:    Haskell2010
+-- This file has been generated from package.yaml by hpack version 0.34.7.
+--
+-- see: https://github.com/sol/hpack
+--
+-- hash: 089fe9b55bbab6cbfceb1623b5f1eb4f8c706b39fa51ad2d87957cefea80301c
 
-executable lambda-calculator
-  hs-source-dirs:      app
-  main-is:             Main.hs
-  other-modules:       Paths_lambda_calculator
-  ghc-options:         -threaded -rtsopts -with-rtsopts=-N
-  build-depends:       base >= 4.9,
-                       lambda-calculator,
-                       optparse-applicative >= 0.13,
-                       Shellac,
-                       Shellac-readline
-  default-language:    Haskell2010
+name:           lambda-calculator
+version:        3.0.0
+synopsis:       A lambda calculus interpreter
+description:    Please see README.md
+category:       LambdaCalculus,Language,Teaching
+homepage:       https://github.com/sgillespie/lambda-calculus#readme
+bug-reports:    https://github.com/sgillespie/lambda-calculus/issues
+author:         Sean D Gillespie
+maintainer:     sean@mistersg.net
+copyright:      2016 Sean Gillespie
+license:        MIT
+license-file:   LICENSE
+build-type:     Simple
 
-test-suite lambda-calculus-test
-  type:                exitcode-stdio-1.0
-  hs-source-dirs:      test
-  main-is:             Spec.hs
-  other-modules:       Language.LambdaSpec,
-                       Language.Lambda.Examples.BoolSpec,
-                       Language.Lambda.Examples.NatSpec,
-                       Language.Lambda.Examples.PairSpec,
-                       Language.Lambda.ExpressionSpec,
-                       Language.Lambda.EvalSpec,
-                       Language.Lambda.HspecUtils,
-                       Language.Lambda.ParserSpec,
+source-repository head
+  type: git
+  location: https://github.com/sgillespie/lambda-calculus
 
-                       Language.Lambda.Util.PrettyPrintSpec,
+library
+  exposed-modules:
+      Language.Lambda.Shared.Errors
+      Language.Lambda.Shared.UniqueSupply
+      Language.Lambda.Untyped
+      Language.Lambda.Untyped.Expression
+      Language.Lambda.Untyped.Eval
+      Language.Lambda.Untyped.Parser
+      Language.Lambda.Untyped.State
+      Language.Lambda.SystemF
+      Language.Lambda.SystemF.Expression
+      Language.Lambda.SystemF.Parser
+      Language.Lambda.SystemF.State
+      Language.Lambda.SystemF.TypeCheck
+  other-modules:
+      Language.Lambda
+      Paths_lambda_calculator
+  hs-source-dirs:
+      src
+  default-extensions:
+      BangPatterns
+      ConstraintKinds
+      DataKinds
+      DefaultSignatures
+      DeriveDataTypeable
+      DeriveFoldable
+      DeriveFunctor
+      DeriveGeneric
+      DeriveTraversable
+      DoAndIfThenElse
+      EmptyDataDecls
+      ExistentialQuantification
+      FlexibleContexts
+      FlexibleInstances
+      FunctionalDependencies
+      GADTs
+      GeneralizedNewtypeDeriving
+      InstanceSigs
+      KindSignatures
+      LambdaCase
+      MultiParamTypeClasses
+      MultiWayIf
+      NamedFieldPuns
+      PartialTypeSignatures
+      PatternGuards
+      PolyKinds
+      RankNTypes
+      RecordWildCards
+      ScopedTypeVariables
+      StandaloneDeriving
+      TupleSections
+      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
+    , mtl
+    , parsec
+    , prettyprinter
+    , rio
+  default-language: Haskell2010
 
-                       Language.SystemFSpec,
-                       Language.SystemF.ExpressionSpec,
-                       Language.SystemF.ParserSpec,
-                       Language.SystemF.TypeCheckSpec
-  build-depends:       base < 5,
-                       lambda-calculator,
-                       containers,
-                       hspec,
-                       HUnit
-  ghc-options:         -threaded -rtsopts -with-rtsopts=-N
-  default-language:    Haskell2010
+executable lambda-calculator
+  main-is: Main.hs
+  other-modules:
+      CliOptions
+      Repl
+      Repl.Shared
+      Repl.SystemF
+      Repl.Untyped
+      Paths_lambda_calculator
+  hs-source-dirs:
+      app
+  default-extensions:
+      BangPatterns
+      ConstraintKinds
+      DataKinds
+      DefaultSignatures
+      DeriveDataTypeable
+      DeriveFoldable
+      DeriveFunctor
+      DeriveGeneric
+      DeriveTraversable
+      DoAndIfThenElse
+      EmptyDataDecls
+      ExistentialQuantification
+      FlexibleContexts
+      FlexibleInstances
+      FunctionalDependencies
+      GADTs
+      GeneralizedNewtypeDeriving
+      InstanceSigs
+      KindSignatures
+      LambdaCase
+      MultiParamTypeClasses
+      MultiWayIf
+      NamedFieldPuns
+      PartialTypeSignatures
+      PatternGuards
+      PolyKinds
+      RankNTypes
+      RecordWildCards
+      ScopedTypeVariables
+      StandaloneDeriving
+      TupleSections
+      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
+    , mtl
+    , optparse-applicative
+    , prettyprinter
+    , repline
+    , rio
+    , text
+  default-language: Haskell2010
 
 test-suite lambda-calculus-lint
-  type:                exitcode-stdio-1.0
-  hs-source-dirs:      test
-  main-is:             HLint.hs
-  build-depends:       base <= 5,
-                       hlint
-  ghc-options:         -threaded -rtsopts -with-rtsopts=-N
-  default-language:    Haskell2010
+  type: exitcode-stdio-1.0
+  main-is: HLint.hs
+  hs-source-dirs:
+      scripts
+  default-extensions:
+      BangPatterns
+      ConstraintKinds
+      DataKinds
+      DefaultSignatures
+      DeriveDataTypeable
+      DeriveFoldable
+      DeriveFunctor
+      DeriveGeneric
+      DeriveTraversable
+      DoAndIfThenElse
+      EmptyDataDecls
+      ExistentialQuantification
+      FlexibleContexts
+      FlexibleInstances
+      FunctionalDependencies
+      GADTs
+      GeneralizedNewtypeDeriving
+      InstanceSigs
+      KindSignatures
+      LambdaCase
+      MultiParamTypeClasses
+      MultiWayIf
+      NamedFieldPuns
+      PartialTypeSignatures
+      PatternGuards
+      PolyKinds
+      RankNTypes
+      RecordWildCards
+      ScopedTypeVariables
+      StandaloneDeriving
+      TupleSections
+      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
+    , mtl
+    , prettyprinter
+    , rio
+  default-language: Haskell2010
 
-source-repository head
-  type:     git
-  location: https://github.com/sgillespie/lambda-calculus
+test-suite lambda-calculus-test
+  type: exitcode-stdio-1.0
+  main-is: Spec.hs
+  other-modules:
+      Language.Lambda.SystemF.ExpressionSpec
+      Language.Lambda.SystemF.ParserSpec
+      Language.Lambda.SystemF.TypeCheckSpec
+      Language.Lambda.SystemFSpec
+      Language.Lambda.Untyped.EvalSpec
+      Language.Lambda.Untyped.Examples.BoolSpec
+      Language.Lambda.Untyped.Examples.NatSpec
+      Language.Lambda.Untyped.Examples.PairSpec
+      Language.Lambda.Untyped.ExpressionSpec
+      Language.Lambda.Untyped.HspecUtils
+      Language.Lambda.Untyped.ParserSpec
+      Language.Lambda.UntypedSpec
+      Paths_lambda_calculator
+  hs-source-dirs:
+      test
+  default-extensions:
+      BangPatterns
+      ConstraintKinds
+      DataKinds
+      DefaultSignatures
+      DeriveDataTypeable
+      DeriveFoldable
+      DeriveFunctor
+      DeriveGeneric
+      DeriveTraversable
+      DoAndIfThenElse
+      EmptyDataDecls
+      ExistentialQuantification
+      FlexibleContexts
+      FlexibleInstances
+      FunctionalDependencies
+      GADTs
+      GeneralizedNewtypeDeriving
+      InstanceSigs
+      KindSignatures
+      LambdaCase
+      MultiParamTypeClasses
+      MultiWayIf
+      NamedFieldPuns
+      PartialTypeSignatures
+      PatternGuards
+      PolyKinds
+      RankNTypes
+      RecordWildCards
+      ScopedTypeVariables
+      StandaloneDeriving
+      TupleSections
+      TypeFamilies
+      TypeSynonymInstances
+      ViewPatterns
+  ghc-options: -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wpartial-fields -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N
+  build-depends:
+      HUnit
+    , base >=4.9 && <5
+    , containers
+    , hspec
+    , lambda-calculator
+    , mtl
+    , prettyprinter
+    , rio
+  default-language: Haskell2010
diff --git a/scripts/HLint.hs b/scripts/HLint.hs
new file mode 100644
--- /dev/null
+++ b/scripts/HLint.hs
@@ -0,0 +1,16 @@
+module Main (main) where
+
+import Language.Haskell.HLint (hlint)
+import System.Exit (exitFailure, exitSuccess)
+
+arguments :: [String]
+arguments = [ 
+  "app",
+  "src",
+  "test"
+  ]
+
+main :: IO ()
+main = hlint arguments >>= main'
+  where main' [] = exitSuccess
+        main' _  = exitFailure
diff --git a/src/Language/Lambda.hs b/src/Language/Lambda.hs
--- a/src/Language/Lambda.hs
+++ b/src/Language/Lambda.hs
@@ -1,26 +1,5 @@
-{-# LANGUAGE FlexibleInstances #-}
-module Language.Lambda (
-  LambdaExpr(..),
-  ParseError(..),
-  PrettyPrint(..),
-  evalExpr,
-  evalString,
-  parseExpr,
-  uniques,
+module Language.Lambda
+  ( module Language.Lambda.Shared.Errors
   ) where
 
-import Control.Monad
-import Text.Parsec
-
-import Language.Lambda.Eval
-import Language.Lambda.Expression
-import Language.Lambda.Parser
-import Language.Lambda.Util.PrettyPrint
-
-evalString :: String -> Either ParseError (LambdaExpr String)
-evalString = fmap (evalExpr uniques) . parseExpr
-
-uniques :: [String]
-uniques = concatMap (\p -> map (:p) . reverse $ ['a'..'z']) suffix
-  where suffix = "" : map show [(0::Int)..]
-
+import Language.Lambda.Shared.Errors
diff --git a/src/Language/Lambda/Eval.hs b/src/Language/Lambda/Eval.hs
deleted file mode 100644
--- a/src/Language/Lambda/Eval.hs
+++ /dev/null
@@ -1,56 +0,0 @@
-module Language.Lambda.Eval where
-
-import Data.List
-import Data.Maybe
-
-import Language.Lambda.Expression
-
-evalExpr :: Eq n => [n] -> LambdaExpr n -> LambdaExpr n
-evalExpr uniqs (Abs name expr) = Abs name . evalExpr uniqs $ expr
-evalExpr _     expr@(Var _)    = expr
-evalExpr uniqs (App e1   e2)   = betaReduce uniqs (evalExpr uniqs e1)
-                                                  (evalExpr uniqs e2)
-
-betaReduce :: Eq n => [n] -> LambdaExpr n -> LambdaExpr n -> LambdaExpr n
-betaReduce uniqs (App e1 e1') e2 = App (betaReduce uniqs e1 e1') e2
-betaReduce _     expr@(Var _) e2 = App expr e2
-betaReduce uniqs (Abs n  e1)  e2 = evalExpr uniqs . sub n e1' $ e2
-  where fvs = freeVarsOf e2
-        e1' = alphaConvert uniqs fvs e1
-
-alphaConvert :: Eq n => [n] -> [n] -> LambdaExpr n -> LambdaExpr n
-alphaConvert uniqs freeVars (Abs name body)
-  | name `elem` freeVars = Abs uniq . sub name body . Var $ uniq
-  | otherwise            = Abs name . alphaConvert uniqs freeVars $ body
-  where uniq = fromMaybe name (find (`notElem` freeVars) uniqs)
-alphaConvert _ _ e = e
-
-etaConvert :: Eq n => LambdaExpr n -> LambdaExpr n
-etaConvert (Abs n (App e1 (Var n')))
-  | n == n'   = etaConvert e1
-  | otherwise = Abs n (App (etaConvert e1) (Var n'))
-etaConvert (Abs n e@(Abs _ _)) 
-  -- If `etaConvert e == e` then etaConverting it will create an infinite loop
-  | e == e'   = Abs n e'
-  | otherwise = etaConvert (Abs n e')
-  where e' = etaConvert e
-etaConvert (Abs n expr) = Abs n (etaConvert expr)
-etaConvert (App e1 e2)  = App (etaConvert e1) (etaConvert e2)
-etaConvert expr@(Var _) = expr
-
-sub :: Eq n => n -> LambdaExpr n -> LambdaExpr n -> LambdaExpr n
-sub name b@(Var name') expr
-  | name == name' = expr
-  | otherwise     = b
-
-sub name b@(Abs name' expr') expr
-  | name == name' = b
-  | otherwise     = Abs name' (sub name expr' expr)
-
-sub name (App e1 e2) expr = App (sub name e1 expr)
-                                (sub name e2 expr)
-
-freeVarsOf :: Eq n => LambdaExpr n -> [n]
-freeVarsOf (Abs n expr) = filter (/=n) . freeVarsOf $ expr
-freeVarsOf (App e1 e2)  = freeVarsOf e1 ++ freeVarsOf e2
-freeVarsOf (Var n)      = [n]
diff --git a/src/Language/Lambda/Expression.hs b/src/Language/Lambda/Expression.hs
deleted file mode 100644
--- a/src/Language/Lambda/Expression.hs
+++ /dev/null
@@ -1,51 +0,0 @@
-{-# LANGUAGE FlexibleInstances #-}
-module Language.Lambda.Expression where
-
-import Prelude hiding (abs, uncurry)
-
-import Language.Lambda.Util.PrettyPrint
-
-data LambdaExpr name
-  = Var name
-  | App (LambdaExpr name) (LambdaExpr name)
-  | Abs name (LambdaExpr name)
-  deriving (Eq, Show)
-
--- Pretty printing
-instance PrettyPrint a => PrettyPrint (LambdaExpr a) where
-  prettyPrint = prettyPrint . pprExpr empty
-
--- Pretty print a lambda expression
-pprExpr :: PrettyPrint n => PDoc String -> LambdaExpr n -> PDoc String
-pprExpr pdoc (Var n)      = prettyPrint n `add` pdoc
-pprExpr pdoc (Abs n body) = pprAbs pdoc n body
-pprExpr pdoc (App e1 e2)  = pprApp pdoc e1 e2
-
--- Pretty print an abstraction 
-pprAbs :: PrettyPrint n => PDoc String -> n -> LambdaExpr n -> PDoc String
-pprAbs pdoc n body
-  = between vars' [lambda] ". " (pprExpr pdoc body')
-  where (vars, body') = uncurry n body
-        vars' = intercalate (map prettyPrint vars) " " empty
-
--- Pretty print an application
-pprApp :: PrettyPrint n
-        => PDoc String
-        -> LambdaExpr n
-        -> LambdaExpr n
-        -> PDoc String
-pprApp pdoc e1@(Abs _ _) e2@(Abs _ _) = betweenParens (pprExpr pdoc e1) pdoc
-  `mappend` addSpace (betweenParens (pprExpr pdoc e2) pdoc)
-pprApp pdoc e1 e2@(App _ _) = pprExpr pdoc e1
-  `mappend` addSpace (betweenParens (pprExpr pdoc e2) pdoc)
-pprApp pdoc e1 e2@(Abs _ _) = pprExpr pdoc e1
-  `mappend` addSpace (betweenParens (pprExpr pdoc e2) pdoc)
-pprApp pdoc e1@(Abs _ _) e2 = betweenParens (pprExpr pdoc e1) pdoc
-  `mappend` addSpace (pprExpr pdoc e2)
-pprApp pdoc e1 e2
-  = pprExpr pdoc e1 `mappend` addSpace (pprExpr pdoc e2)
-
-uncurry :: n -> LambdaExpr n -> ([n], LambdaExpr n)
-uncurry n = uncurry' [n]
-  where uncurry' ns (Abs n' body') = uncurry' (n':ns) body'
-        uncurry' ns body'          = (reverse ns, body')
diff --git a/src/Language/Lambda/Parser.hs b/src/Language/Lambda/Parser.hs
deleted file mode 100644
--- a/src/Language/Lambda/Parser.hs
+++ /dev/null
@@ -1,46 +0,0 @@
-module Language.Lambda.Parser (parseExpr) where
-
-import Control.Monad
-import Prelude hiding (abs, curry, id)
-
-import Text.Parsec
-import Text.Parsec.String
-
-import Language.Lambda.Expression
-
-parseExpr :: String -> Either ParseError (LambdaExpr String)
-parseExpr = parse (whitespace *> expr <* eof) ""
-
-expr :: Parser (LambdaExpr String)
-expr = try app <|> term
-
-term :: Parser (LambdaExpr String)
-term = abs <|> var <|> parens
-
-var :: Parser (LambdaExpr String)
-var = Var <$> identifier
-
-abs :: Parser (LambdaExpr String)
-abs = curry <$> idents <*> expr
-  where idents = symbol '\\' *> many1 identifier <* symbol '.'
-        curry = flip (foldr Abs)
-
-app :: Parser (LambdaExpr String)
-app = chainl1 term (return App)
-
-parens :: Parser (LambdaExpr String)
-parens = symbol '(' *> expr <* symbol ')'
-
-lexeme :: Parser a -> Parser a
-lexeme p =  p <* whitespace
-
-whitespace :: Parser ()
-whitespace = void . many . oneOf $ " \t"
-
-identifier :: Parser String
-identifier = lexeme ((:) <$> first <*> many rest)
-  where first = letter <|> char '_'
-        rest  = first <|> digit
-
-symbol :: Char -> Parser ()
-symbol = void . lexeme . char
diff --git a/src/Language/Lambda/Shared/Errors.hs b/src/Language/Lambda/Shared/Errors.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Lambda/Shared/Errors.hs
@@ -0,0 +1,61 @@
+module Language.Lambda.Shared.Errors
+  ( LambdaException(..),
+    isLambdaException,
+    isLetError,
+    isParseError,
+    isImpossibleError
+  ) where
+
+import RIO
+
+data LambdaException
+  -- | An expression that cannot be parsed
+  -- Examples:
+  --
+  --     \x y
+  --     = y
+  = ParseError Text
+
+  -- | A let binding nested in another expression
+  -- Examples:
+  --
+  --     \x. let y = z
+  --     x (let y = z)
+  | InvalidLet Text -- ^ A let binding nested in another expression
+
+  -- | The expected type does not match the actual type
+  -- Examples:
+  --
+  --     (\x: X. x) (y:Y)
+  | TyMismatchError Text
+
+  -- | A catch-all error that indicates a bug in this project
+  | ImpossibleError
+  deriving (Eq, Typeable)
+
+instance Exception LambdaException
+
+instance Display LambdaException where
+  textDisplay (ParseError txt) = "Parse error " <> txt
+  textDisplay (InvalidLet txt) = "Illegal nested let: " <> txt
+  textDisplay ImpossibleError = "An impossible error occurred! Please file a bug."
+
+instance Show LambdaException where
+  show = show . textDisplay
+
+-- | Returns true if the passed in value is a LamdbaExpression. Can be used, for example,
+-- as a `shouldThrow` matcher
+isLambdaException :: LambdaException -> Bool
+isLambdaException _ = True
+
+isLetError :: LambdaException -> Bool
+isLetError (InvalidLet _) = True
+isLetError _ = False
+
+isParseError :: LambdaException -> Bool
+isParseError (ParseError _) = True
+isParseError _ = False
+
+isImpossibleError :: LambdaException -> Bool
+isImpossibleError ImpossibleError = True
+isImpossibleError _ = False
diff --git a/src/Language/Lambda/Shared/UniqueSupply.hs b/src/Language/Lambda/Shared/UniqueSupply.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Lambda/Shared/UniqueSupply.hs
@@ -0,0 +1,9 @@
+module Language.Lambda.Shared.UniqueSupply where
+
+import RIO
+import RIO.Text (pack)
+
+defaultUniques :: [Text]
+defaultUniques = map pack strings
+  where strings = concatMap (\p -> map (:p) . reverse $ ['a'..'z']) suffix
+        suffix = "" : map show [(0::Int)..]
diff --git a/src/Language/Lambda/SystemF.hs b/src/Language/Lambda/SystemF.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Lambda/SystemF.hs
@@ -0,0 +1,26 @@
+module Language.Lambda.SystemF (
+  Globals(),
+  evalText,
+
+  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.SystemF.Expression
+import Language.Lambda.SystemF.Parser
+import Language.Lambda.SystemF.State
+
+type Globals = Map.Map String (SystemFExpr String String)
+
+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
+
diff --git a/src/Language/Lambda/SystemF/Expression.hs b/src/Language/Lambda/SystemF/Expression.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Lambda/SystemF/Expression.hs
@@ -0,0 +1,124 @@
+module Language.Lambda.SystemF.Expression
+  ( SystemFExpr(..),
+    Ty(..),
+    prettyPrint,
+    upperLambda
+  ) where
+
+import Data.Monoid
+import Prettyprinter
+import Prettyprinter.Render.Text (renderStrict)
+import RIO
+
+data SystemFExpr name ty
+  -- | Variable: `x`
+  = Var name
+  -- | Function application: `x y`
+  | App (SystemFExpr name ty) (SystemFExpr name ty)
+  -- | Lambda abstraction: `\x: X. x`
+  | Abs name (Ty ty) (SystemFExpr name ty)
+  -- | Type Abstraction: `\X. body`
+  | TyAbs ty (SystemFExpr name ty)                  
+  -- | Type Application: `x [X]`
+  | TyApp (SystemFExpr name ty) (Ty ty)
+  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)
+
+instance (Pretty name, Pretty ty) => Pretty (SystemFExpr name ty) where
+  pretty (Var name) = pretty name
+  pretty (App e1 e2) = prettyApp e1 e2
+  pretty (Abs name ty body) = prettyAbs name ty body
+  pretty (TyAbs ty body) = prettyTyAbs ty body
+  pretty (TyApp expr ty) = prettyTyApp expr ty
+
+instance Pretty name => Pretty (Ty name) where
+  pretty = prettyTy False
+
+prettyPrint :: Pretty pretty => pretty -> Text
+prettyPrint expr = renderStrict docStream
+  where docStream = layoutPretty defaultLayoutOptions (pretty expr)
+
+upperLambda :: Char
+upperLambda = 'Λ'
+
+prettyApp
+  :: (Pretty name, Pretty ty)
+  => SystemFExpr name ty
+  -> SystemFExpr name ty
+  -> Doc a
+prettyApp e1@Abs{} e2@Abs{} = parens (pretty e1) <+> parens (pretty e2)
+prettyApp e1@Abs{} e2 = parens (pretty e1) <+> pretty e2
+prettyApp e1 e2@Abs{} = pretty e1 <+> parens (pretty e2)
+prettyApp e1 e2@App{} = pretty e1 <+> parens (pretty e2)
+prettyApp e1 e2 = pretty e1 <+> pretty e2
+
+prettyAbs
+  :: (Pretty name, Pretty ty)
+  => name
+  -> Ty ty
+  -> SystemFExpr name ty
+  -> Doc ann
+prettyAbs name ty body
+  = lambda
+    <+> hsep (map (uncurry prettyArg) names)
+    <> dot
+    <+> pretty body'
+  where (names, body') = uncurryAbs name ty body
+
+prettyTyAbs :: (Pretty name, Pretty ty) => ty -> SystemFExpr name ty -> 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 expr ty = pretty expr <+> brackets (pretty ty)
+
+prettyTy :: Pretty name => Bool -> Ty name -> Doc ann
+prettyTy _ (TyVar name) = pretty name
+prettyTy compact (TyArrow t1 t2) = prettyTyArrow compact t1 t2
+prettyTy compact (TyForAll name ty) = prettyTyForAll compact name ty
+
+prettyTyArrow :: Pretty name => Bool -> Ty name -> Ty name -> Doc ann
+prettyTyArrow compact (TyArrow t1 t2) t3
+  = prettyTyArrow' compact compositeTy $ prettyTy compact t3
+  where compositeTy = parens $ prettyTyArrow compact t1 t2
+
+prettyTyArrow compact t1 t2
+  = prettyTyArrow' compact (prettyTy compact t1) (prettyTy compact t2)
+
+prettyTyForAll :: Pretty name => Bool -> name -> Ty name -> Doc ann
+prettyTyForAll compact name ty
+  = "forall"
+  <+> pretty name <> dot
+  <+> prettyTy compact ty
+
+lambda :: Doc ann
+lambda = pretty 'λ'
+
+prettyArg :: (Pretty name, Pretty ty) => name -> Ty ty -> Doc ann
+prettyArg name (TyArrow t1 t2)
+  = pretty name <> colon <> parens (prettyTyArrow True t1 t2)
+prettyArg name ty = pretty name <> colon <> pretty ty
+
+upperLambda' :: Doc ann
+upperLambda' = pretty upperLambda
+
+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 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 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
new file mode 100644
--- /dev/null
+++ b/src/Language/Lambda/SystemF/Parser.hs
@@ -0,0 +1,88 @@
+module Language.Lambda.SystemF.Parser (
+  parseExpr,
+  parseType
+  ) where
+
+import Control.Monad
+import Data.Functor
+import RIO hiding ((<|>), abs, many, try)
+import qualified RIO.Text as Text
+
+import Text.Parsec
+import Text.Parsec.Text
+
+import Language.Lambda.SystemF.Expression
+
+parseExpr :: Text -> Either ParseError (SystemFExpr Text Text)
+parseExpr = parse (whitespace *> expr <* eof) ""
+
+parseType :: Text -> Either ParseError (Ty Text)
+parseType = parse (whitespace *> ty <* eof) ""
+
+-- Parse expressions
+expr :: Parser (SystemFExpr Text Text)
+expr = try tyapp <|> try app <|> term
+
+app :: Parser (SystemFExpr Text Text)
+app = chainl1 term (return App)
+
+tyapp :: Parser (SystemFExpr Text Text)
+tyapp = TyApp
+      <$> term
+      <*> ty'
+  where ty' = symbol '[' *> ty <* symbol ']'
+
+term :: Parser (SystemFExpr Text Text)
+term = try abs <|> tyabs <|> var <|> parens expr
+
+var :: Parser (SystemFExpr Text Text)
+var = Var <$> exprId
+
+abs :: Parser (SystemFExpr Text Text)
+abs = curry'
+    <$> (symbol '\\' *> many1 args <* symbol '.') 
+    <*> expr
+  where args = (,) <$> (exprId <* symbol ':') <*> ty
+        curry' = flip . foldr . uncurry $ Abs
+
+tyabs :: Parser (SystemFExpr Text 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
+
+arrow :: Parser (Ty Text)
+arrow = chainr1 tyterm (symbol' "->" $> TyArrow)
+
+tyterm :: Parser (Ty Text)
+tyterm = tyvar <|> parens ty
+
+tyvar :: Parser (Ty Text)
+tyvar = TyVar <$> typeId
+
+parens :: Parser a -> Parser a
+parens p = symbol '(' *> p <* symbol ')'
+
+identifier :: Parser Char -> Parser Text
+identifier firstChar = lexeme $ Text.cons <$> first' <*> (Text.pack <$> many rest)
+  where first' = firstChar <|> char '_'
+        rest = first' <|> digit
+
+typeId, exprId :: Parser Text
+typeId = identifier upper
+exprId = identifier lower
+
+whitespace :: Parser ()
+whitespace = void . many . oneOf $ " \t"
+
+symbol :: Char -> Parser ()
+symbol = void . lexeme . char
+
+symbol' :: Text -> Parser ()
+symbol' = void . lexeme . string . Text.unpack
+
+lexeme :: Parser a -> Parser a
+lexeme p = p <* whitespace
diff --git a/src/Language/Lambda/SystemF/State.hs b/src/Language/Lambda/SystemF/State.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Lambda/SystemF/State.hs
@@ -0,0 +1,89 @@
+module Language.Lambda.SystemF.State
+  ( TypecheckState(..),
+    Typecheck(),
+    Context(),
+    runTypecheck,
+    execTypecheck,
+    unsafeRunTypecheck,
+    unsafeExecTypecheck,
+    mkTypecheckState,
+    context,
+    uniques,
+    getContext,
+    getUniques,
+    modifyContext,
+    modifyUniques,
+    setContext,
+    setUniques
+  ) where
+
+import Language.Lambda.Shared.Errors (LambdaException(..))
+import Language.Lambda.SystemF.Expression (Ty(..))
+
+import Control.Monad.Except (Except(), runExcept)
+import RIO
+import RIO.State
+import qualified RIO.Map as Map
+
+data TypecheckState name = TypecheckState
+  { tsContext :: Context name,
+    tsUniques :: [name]
+  }
+
+type Typecheck name
+  = StateT (TypecheckState name)
+      (Except LambdaException)
+
+type Context name = Map name (Ty name)
+
+runTypecheck
+  :: Typecheck name result
+  -> TypecheckState name
+  -> Either LambdaException (result, TypecheckState name)
+runTypecheck computation = runExcept . runStateT computation
+
+execTypecheck
+  :: Typecheck name result
+  -> TypecheckState name
+  -> Either LambdaException result
+execTypecheck computation = runExcept . evalStateT computation
+
+unsafeRunTypecheck
+  :: Typecheck name result
+  -> TypecheckState name
+  -> (result, TypecheckState name)
+unsafeRunTypecheck computation state' = either impureThrow id tcResult
+  where tcResult = runTypecheck computation state'
+
+unsafeExecTypecheck :: Typecheck name result -> TypecheckState name -> result
+unsafeExecTypecheck computation state' = either impureThrow id tcResult
+  where tcResult = execTypecheck computation state'
+
+mkTypecheckState :: [name] -> TypecheckState name
+mkTypecheckState = TypecheckState Map.empty
+
+uniques :: Lens' (TypecheckState name) [name]
+uniques f state' = (\uniques' -> state' { tsUniques = uniques' })
+  <$> f (tsUniques state')
+
+context :: Lens' (TypecheckState name) (Context name)
+context f state' = (\context' -> state' { tsContext = context' })
+  <$> f (tsContext state')
+
+getUniques :: Typecheck name [name]
+getUniques = gets (^. uniques)
+
+getContext :: Typecheck name (Context name)
+getContext = gets (^. context)
+
+modifyContext :: (Context name -> Context name) -> Typecheck name ()
+modifyContext f = modify $ context %~ f
+
+modifyUniques :: ([name] -> [name]) -> Typecheck name ()
+modifyUniques f = modify $ uniques %~ f
+
+setUniques :: [name] -> Typecheck name ()
+setUniques uniques' = modify (& uniques .~ uniques')
+
+setContext :: Context name -> Typecheck name ()
+setContext context' = modify (& context .~ context')
diff --git a/src/Language/Lambda/SystemF/TypeCheck.hs b/src/Language/Lambda/SystemF/TypeCheck.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Lambda/SystemF/TypeCheck.hs
@@ -0,0 +1,122 @@
+module Language.Lambda.SystemF.TypeCheck where
+
+import Language.Lambda.Shared.Errors (LambdaException(..))
+import Language.Lambda.SystemF.Expression
+import Language.Lambda.SystemF.State
+
+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
+  -> 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
+
+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
+
+typecheckAbs
+  :: (Ord name, Pretty name)
+  => name
+  -> Ty name
+  -> SystemFExpr name name
+  -> Typecheck name (Ty name)
+typecheckAbs name ty body
+  = modifyContext (Map.insert name ty)
+    >> TyArrow ty <$> typecheck body
+
+typecheckApp
+  :: (Ord name, Pretty name)
+  => SystemFExpr name name
+  -> SystemFExpr name name
+  -> Typecheck name (Ty name)
+typecheckApp e1 e2 = do
+  -- Typecheck expressions
+  t1 <- typecheck e1
+  t2 <- typecheck 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
+
+  -- Verify the output of e1 matches the type of e2
+  if t1AppInput == t2
+    then return t1AppOutput
+    else throwError $ tyMismatchError (TyArrow t2 t1AppOutput) (TyArrow t1 t1AppOutput)
+
+typecheckTyAbs
+  :: (Ord name, Pretty name)
+  => name
+  -> SystemFExpr name name
+  -> Typecheck name (Ty name)
+typecheckTyAbs ty body
+  = modifyContext (Map.insert ty (TyVar ty))
+    >> TyForAll ty <$> typecheck body
+
+typecheckTyApp
+  :: (Ord name, Pretty name)
+  => SystemFExpr name name
+  -> Ty name
+  -> Typecheck name (Ty name)
+typecheckTyApp (TyAbs t expr) ty = typecheck $ substitute ty t expr
+typecheckTyApp expr _ = typecheck expr
+
+unique :: Typecheck name name
+unique = getUniques >>= fromJust' . List.headMaybe
+  where fromJust' (Just u) = return u
+        fromJust' Nothing = throwError ImpossibleError
+
+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
+
+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')
+
+
+tyMismatchError
+  :: (Pretty t1, Pretty t2)
+  => t1
+  -> t2
+  -> LambdaException
+tyMismatchError expected actual
+  = TyMismatchError
+  $ "Couldn't match expected type "
+  <> prettyPrint expected
+  <> " with actual type "
+  <> prettyPrint actual
diff --git a/src/Language/Lambda/Untyped.hs b/src/Language/Lambda/Untyped.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Lambda/Untyped.hs
@@ -0,0 +1,52 @@
+{-# LANGUAGE FlexibleInstances #-}
+module Language.Lambda.Untyped (
+  evalText,
+  runEvalText,
+  execEvalText,
+  unsafeExecEvalText,
+  defaultUniques,
+
+  module Language.Lambda.Untyped.Expression,
+  module Language.Lambda.Untyped.Eval,
+  module Language.Lambda.Untyped.Parser,
+  module Language.Lambda.Untyped.State
+  ) where
+
+import Control.Monad.Except
+import Data.Either
+import RIO
+import qualified RIO.Text as Text
+
+import Language.Lambda.Shared.Errors
+import Language.Lambda.Shared.UniqueSupply (defaultUniques)
+import Language.Lambda.Untyped.Eval
+import Language.Lambda.Untyped.Expression
+import Language.Lambda.Untyped.Parser
+import Language.Lambda.Untyped.State
+
+evalText :: Text -> Eval Text (LambdaExpr Text)
+evalText = either throwParseError evalExpr' . parseExpr
+  where throwParseError = throwError . ParseError . Text.pack . show
+        evalExpr' = evalExpr
+
+runEvalText
+  :: Text
+  -> Globals Text
+  -> Either LambdaException (LambdaExpr Text, EvalState Text)
+runEvalText input globals' = runEval (evalText input) (mkState globals')
+
+execEvalText
+  :: Text
+  -> Globals Text
+  -> Either LambdaException (LambdaExpr Text)
+execEvalText input globals' = execEval (evalText input) (mkState globals')
+
+unsafeExecEvalText
+  :: Text
+  -> Globals Text
+  -> LambdaExpr Text
+unsafeExecEvalText input globals'
+  = unsafeExecEval (evalText input) (mkState globals')
+
+mkState :: Globals Text -> EvalState Text
+mkState = flip EvalState defaultUniques
diff --git a/src/Language/Lambda/Untyped/Eval.hs b/src/Language/Lambda/Untyped/Eval.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Lambda/Untyped/Eval.hs
@@ -0,0 +1,121 @@
+module Language.Lambda.Untyped.Eval
+  ( EvalState(..),
+    evalExpr,
+    subGlobals,
+    betaReduce,
+    alphaConvert,
+    etaConvert,
+    freeVarsOf
+  ) where
+
+import Control.Monad.Except
+import Prettyprinter
+import RIO
+import RIO.List (find)
+import qualified RIO.Map as Map
+
+import Language.Lambda.Shared.Errors
+import Language.Lambda.Untyped.Expression
+import Language.Lambda.Untyped.State
+
+-- | Evaluate an expression
+evalExpr :: (Pretty name, Ord name) => LambdaExpr name -> Eval name (LambdaExpr name)
+evalExpr (Let name expr) = do
+  globals' <- getGlobals
+  result <- evalExpr' $ subGlobals globals' expr
+
+  setGlobals $ Map.insert name result globals'
+
+  return $ Let name result
+
+evalExpr expr = do
+  globals' <- getGlobals
+  evalExpr' $ subGlobals globals' expr
+
+-- | Evaluate an expression; does not support `let`
+evalExpr' :: (Eq name, Pretty name) => LambdaExpr name -> Eval name (LambdaExpr name)
+evalExpr' expr@(Var _) = return expr
+evalExpr' (Abs name expr) = Abs name <$> evalExpr' expr
+evalExpr' (App e1 e2) = do
+  e1' <- evalExpr' e1
+  e2' <- evalExpr' e2
+  betaReduce e1' e2'
+evalExpr' expr@(Let _ _) = throwError . InvalidLet . prettyPrint $ expr
+
+-- | Look up free vars that have global bindings and substitute them
+subGlobals
+  :: Ord name
+  => Map name (LambdaExpr name)
+  -> LambdaExpr name
+  -> LambdaExpr name
+subGlobals globals' expr@(Var x) = Map.findWithDefault expr x globals'
+subGlobals globals' (App e1 e2) = App (subGlobals globals' e1) (subGlobals globals' e2)
+subGlobals globals' (Abs name expr) = Abs name expr'
+  where expr'
+          | Map.member name globals' = expr
+          | otherwise = subGlobals globals' expr
+subGlobals _ expr = expr
+
+-- | Function application
+betaReduce
+  :: (Eq name, Pretty name)
+  => LambdaExpr name
+  -> LambdaExpr name
+  -> Eval name (LambdaExpr name)
+betaReduce expr@(Var _) e2 = return $ App expr e2
+betaReduce (App e1 e1') e2 = do
+  reduced <- betaReduce e1 e1'
+  return $ App reduced e2
+betaReduce (Abs n e1) e2 = do
+  e1' <- alphaConvert (freeVarsOf e2) e1
+  evalExpr' $ substitute e1' n e2
+betaReduce _ _ = throwError ImpossibleError
+
+-- | Rename abstraction parameters to avoid name captures
+alphaConvert :: Eq name => [name] -> LambdaExpr name -> Eval name (LambdaExpr name)
+alphaConvert freeVars (Abs name body) = do
+  uniques' <- getUniques
+  let nextVar = fromMaybe name $ find (`notElem` freeVars) uniques'
+
+  if name `elem` freeVars
+    then return $ Abs nextVar (substitute body name (Var nextVar))
+    else Abs name <$> alphaConvert freeVars body
+
+alphaConvert _ expr = return expr
+
+-- | Eliminite superfluous abstractions
+etaConvert :: Eq n => LambdaExpr n -> LambdaExpr n
+etaConvert (Abs n (App e1 (Var n')))
+  | n == n'   = etaConvert e1
+  | otherwise = Abs n (App (etaConvert e1) (Var n'))
+etaConvert (Abs n e@(Abs _ _)) 
+  -- If `etaConvert e == e` then etaConverting it will create an infinite loop
+  | e == e'   = Abs n e'
+  | otherwise = etaConvert (Abs n e')
+  where e' = etaConvert e
+etaConvert (Abs n expr) = Abs n (etaConvert expr)
+etaConvert (App e1 e2)  = App (etaConvert e1) (etaConvert e2)
+etaConvert expr = expr
+
+-- | Substitute an expression for a variable name in another expression
+substitute :: Eq name => LambdaExpr name -> name -> LambdaExpr name -> LambdaExpr name
+substitute subExpr@(Var name) subName inExpr
+  | name == subName = inExpr
+  | otherwise = subExpr
+
+substitute subExpr@(Abs name expr) subName inExpr
+  | name == subName = subExpr
+  | otherwise = Abs name (substitute expr subName inExpr)
+
+substitute (App e1 e2) subName inExpr
+  = App (sub e1) (sub e2)
+  where sub expr = substitute expr subName inExpr
+
+substitute _ _ expr = expr
+
+-- | Find the free variables in an expression
+freeVarsOf :: Eq n => LambdaExpr n -> [n]
+freeVarsOf (Abs n expr) = filter (/=n) . freeVarsOf $ expr
+freeVarsOf (App e1 e2)  = freeVarsOf e1 ++ freeVarsOf e2
+freeVarsOf (Var n)      = [n]
+freeVarsOf _ = []
diff --git a/src/Language/Lambda/Untyped/Expression.hs b/src/Language/Lambda/Untyped/Expression.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Lambda/Untyped/Expression.hs
@@ -0,0 +1,57 @@
+module Language.Lambda.Untyped.Expression
+  ( LambdaExpr(..),
+    lambda,
+    prettyPrint
+  ) where
+
+import RIO
+import Prettyprinter
+import Prettyprinter.Render.Text (renderStrict)
+
+data LambdaExpr name
+  = Var name                                -- ^ Variables
+  | App (LambdaExpr name) (LambdaExpr name) -- ^ Application
+  | Abs name (LambdaExpr name)              -- ^ Abstractions
+  | Let name (LambdaExpr name)              -- ^ Let bindings
+  deriving (Eq, Show)
+
+instance Pretty name => Pretty (LambdaExpr name) where
+  pretty (Var name) = pretty name
+  pretty (Abs name body) = prettyAbs name body
+  pretty (App e1 e2) = prettyApp e1 e2
+  pretty (Let name body) = prettyLet name body
+
+prettyPrint :: Pretty name => LambdaExpr name -> Text
+prettyPrint expr = renderStrict docStream
+  where docStream = layoutPretty defaultLayoutOptions (pretty expr)
+
+lambda :: Char
+lambda = 'λ'
+
+prettyAbs :: Pretty name => name -> LambdaExpr name -> Doc a
+prettyAbs name body
+  = lambda' <> hsep (map pretty names) <> dot
+    <+> pretty body'
+  where (names, body') = uncurryAbs name body
+
+prettyApp :: Pretty name => LambdaExpr name -> LambdaExpr name -> Doc a
+prettyApp e1@(Abs _ _) e2@(Abs _ _) = parens (pretty e1) <+> parens (pretty e2)
+prettyApp e1@(Abs _ _) e2 = parens (pretty e1) <+> pretty e2
+prettyApp e1 e2@(Abs _ _) = pretty e1 <+> parens (pretty e2)
+prettyApp e1 e2@(App _ _) = pretty e1 <+> parens (pretty e2)
+prettyApp e1 e2 = pretty e1 <+> pretty e2
+
+prettyLet :: Pretty name => name -> LambdaExpr name -> Doc a
+prettyLet name body
+  = pretty ("let"::Text)
+    <+> pretty name
+    <+> "="
+    <+> pretty body
+
+lambda' :: Doc ann
+lambda' = pretty lambda
+
+uncurryAbs :: n -> LambdaExpr n -> ([n], LambdaExpr n)
+uncurryAbs n = uncurry' [n]
+  where uncurry' ns (Abs n' body') = uncurry' (n':ns) body'
+        uncurry' ns body'          = (reverse ns, body')
diff --git a/src/Language/Lambda/Untyped/Parser.hs b/src/Language/Lambda/Untyped/Parser.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Lambda/Untyped/Parser.hs
@@ -0,0 +1,57 @@
+module Language.Lambda.Untyped.Parser
+  ( parseExpr,
+    module Text.Parsec
+  ) where
+
+import Control.Monad
+import RIO hiding ((<|>), abs, curry, many, try)
+import qualified RIO.Text as Text
+
+import Text.Parsec
+import Text.Parsec.Text
+
+import Language.Lambda.Untyped.Expression
+
+parseExpr :: Text -> Either ParseError (LambdaExpr Text)
+parseExpr = parse (whitespace *> expr <* eof) ""
+
+expr :: Parser (LambdaExpr Text)
+expr = try app <|> term
+
+term :: Parser (LambdaExpr Text)
+term = let' <|> abs <|> var <|> parens
+
+var :: Parser (LambdaExpr Text)
+var = Var <$> identifier
+
+abs :: Parser (LambdaExpr Text)
+abs = curry <$> idents <*> expr
+  where idents = symbol '\\' *> many1 identifier <* symbol '.'
+        curry = flip (foldr Abs)
+
+app :: Parser (LambdaExpr Text)
+app = chainl1 term (return App)
+
+let' :: Parser (LambdaExpr Text)
+let' = Let <$> ident <*> expr
+  where ident = keyword "let" *> identifier <* symbol '='
+
+parens :: Parser (LambdaExpr Text)
+parens = symbol '(' *> expr <* symbol ')'
+
+lexeme :: Parser a -> Parser a
+lexeme p =  p <* whitespace
+
+whitespace :: Parser ()
+whitespace = void . many . oneOf $ " \t"
+
+identifier :: Parser Text
+identifier = lexeme $ Text.cons <$> first' <*> (Text.pack <$> many rest)
+  where first' = letter <|> char '_'
+        rest  = first' <|> digit
+
+symbol :: Char -> Parser ()
+symbol = void . lexeme . char
+
+keyword :: Text -> Parser ()
+keyword = void . lexeme . string . Text.unpack
diff --git a/src/Language/Lambda/Untyped/State.hs b/src/Language/Lambda/Untyped/State.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Lambda/Untyped/State.hs
@@ -0,0 +1,88 @@
+module Language.Lambda.Untyped.State
+  ( EvalState(..),
+    Eval(),
+    Globals(),
+    runEval,
+    execEval,
+    unsafeExecEval,
+    unsafeRunEval,
+    globals,
+    uniques,
+    mkEvalState,
+    getGlobals,
+    getUniques,
+    setGlobals,
+    setUniques
+  ) where
+
+import Language.Lambda.Shared.Errors
+import Language.Lambda.Untyped.Expression 
+
+import Control.Monad.Except
+import RIO
+import RIO.State
+import qualified RIO.Map as Map
+
+-- | The evaluation state
+data EvalState name = EvalState
+  { esGlobals :: Globals name,
+    esUniques :: [name] -- ^ Unused unique names
+  }
+
+-- | A stateful computation
+type Eval name
+  = StateT (EvalState name)
+      (Except LambdaException)
+
+-- | A mapping of global variables to expressions
+type Globals name = Map name (LambdaExpr name)
+
+-- | Run an evalualation
+runEval :: Eval name result -> EvalState name -> Either LambdaException (result, EvalState name)
+runEval computation = runExcept . runStateT computation
+
+-- | Run an evalualation, throwing away the final state
+execEval :: Eval name result -> EvalState name -> Either LambdaException result
+execEval computation = runExcept . evalStateT computation
+
+-- | Run an evaluation. If the result is an error, throws it
+unsafeRunEval :: Eval name result -> EvalState name -> (result, EvalState name)
+unsafeRunEval computation state'
+  = case runEval computation state' of
+      Left err -> error $ show err
+      Right res -> res
+  
+-- | Run an evaluation, throwing away the final state. If the result is an error, throws it
+unsafeExecEval:: Eval name result -> EvalState name -> result
+unsafeExecEval computation state'
+  = case execEval computation state' of
+      Left err -> impureThrow err
+      Right res -> res
+
+-- | Create an EvalState
+mkEvalState :: [name] -> EvalState name
+mkEvalState = EvalState Map.empty
+
+globals :: Lens' (EvalState name) (Globals name)
+globals f state'
+  = (\globals' -> state' { esGlobals = globals' })
+  <$> f (esGlobals state')
+
+uniques :: Lens' (EvalState name) [name]
+uniques f state'
+  = (\uniques' -> state' { esUniques = uniques' })
+  <$> f (esUniques state')
+
+-- | Access globals from the state monad
+getGlobals :: Eval name (Globals name)
+getGlobals = gets (^. globals)
+
+-- | Access unique supply from state monad
+getUniques :: Eval name [name]
+getUniques = gets (^. uniques)
+
+setGlobals :: Globals name -> Eval name ()
+setGlobals globals' = modify (& globals .~ globals')
+
+setUniques :: [name] -> Eval name ()
+setUniques uniques' = modify (& uniques .~ uniques')
diff --git a/src/Language/Lambda/Util/PrettyPrint.hs b/src/Language/Lambda/Util/PrettyPrint.hs
deleted file mode 100644
--- a/src/Language/Lambda/Util/PrettyPrint.hs
+++ /dev/null
@@ -1,53 +0,0 @@
-{-# LANGUAGE FlexibleInstances #-}
-module Language.Lambda.Util.PrettyPrint where
-
-import qualified Data.List as L
-
-class PrettyPrint a where
-  prettyPrint :: a -> String
-
-instance PrettyPrint String where
-  prettyPrint = id
-  
-newtype PDoc s = PDoc [s]
-  deriving (Eq, Show)
-
-instance PrettyPrint s => PrettyPrint (PDoc s) where
-  prettyPrint (PDoc ls) = concatMap prettyPrint ls
-
-instance Monoid (PDoc s) where
-  mempty = empty
-  (PDoc p1) `mappend` (PDoc p2) = PDoc $ p1 ++ p2
-
-instance Functor PDoc where
-  fmap f (PDoc ls) = PDoc (fmap f ls)
-
-empty :: PDoc s
-empty = PDoc []
-
-add :: s -> PDoc s -> PDoc s
-add s (PDoc ps) = PDoc (s:ps)
-
-append :: [s] -> PDoc s -> PDoc s
-append =  mappend . PDoc
-
-between :: PDoc s -> s -> s -> PDoc s -> PDoc s
-between (PDoc str) start end pdoc = PDoc ((start:str) ++ [end]) `mappend` pdoc
-
-betweenParens :: PDoc String -> PDoc String -> PDoc String
-betweenParens doc = between doc "(" ")"
-
-intercalate :: [[s]] -> [s] -> PDoc [s] -> PDoc [s]
-intercalate ss sep = add $ L.intercalate sep ss
-
-addSpace :: PDoc String -> PDoc String
-addSpace = add [space]
-  
-space :: Char
-space = ' '
-
-lambda :: Char
-lambda = 'λ'
-
-upperLambda :: Char
-upperLambda = 'Λ'
diff --git a/src/Language/SystemF.hs b/src/Language/SystemF.hs
deleted file mode 100644
--- a/src/Language/SystemF.hs
+++ /dev/null
@@ -1,16 +0,0 @@
-module Language.SystemF (
-  PrettyPrint(..),
-  SystemFExpr(..),
-  evalString,
-  parseExpr
-  ) where
-
-import Text.Parsec
-
-import Language.Lambda.Util.PrettyPrint
-import Language.SystemF.Expression
-import Language.SystemF.Parser
-
-evalString :: String -> Either ParseError (SystemFExpr String String)
-evalString = parseExpr
-
diff --git a/src/Language/SystemF/Expression.hs b/src/Language/SystemF/Expression.hs
deleted file mode 100644
--- a/src/Language/SystemF/Expression.hs
+++ /dev/null
@@ -1,145 +0,0 @@
-module Language.SystemF.Expression where
-
-import Data.Monoid
-
-import Language.Lambda.Util.PrettyPrint
-
-data SystemFExpr name ty
-  = Var name                                        -- Variable
-  | App (SystemFExpr name ty) (SystemFExpr name ty) -- Application
-  | Abs name (Ty ty) (SystemFExpr name ty)          -- Abstraction
-  | TyAbs ty (SystemFExpr name ty)                  -- Type Abstraction
-                                                    -- \X. body
-
-  | TyApp (SystemFExpr name ty) (Ty ty)             -- Type Application
-                                                    -- x [X]
-  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)
-
--- Pretty printing
-instance (PrettyPrint n, PrettyPrint t) => PrettyPrint (SystemFExpr n t) where
-  prettyPrint = prettyPrint . pprExpr empty
-
-instance PrettyPrint n => PrettyPrint (Ty n) where
-  prettyPrint = prettyPrint . pprTy empty True
-
--- Same as prettyPrint, but we assume the same type for names and types. Useful
--- for testing.
-prettyPrint' :: PrettyPrint n => SystemFExpr n n -> String
-prettyPrint' = prettyPrint
-
--- Pretty print a system f expression
-pprExpr :: (PrettyPrint n, PrettyPrint t) 
-        => PDoc String 
-        -> SystemFExpr n t
-        -> PDoc String
-pprExpr pdoc (Var n)        = prettyPrint n `add` pdoc
-pprExpr pdoc (App e1 e2)    = pprApp pdoc e1 e2
-pprExpr pdoc (Abs n t body) = pprAbs pdoc n t body
-pprExpr pdoc (TyAbs t body) = pprTAbs pdoc t body
-pprExpr pdoc (TyApp e ty)   = pprTApp pdoc e ty
-
--- Pretty print an application
-pprApp :: (PrettyPrint n, PrettyPrint t)
-       => PDoc String
-       -> SystemFExpr n t
-       -> SystemFExpr n t
-       -> PDoc String
-pprApp pdoc e1@Abs{} e2@Abs{} = betweenParens (pprExpr pdoc e1) pdoc
-  `mappend` addSpace (betweenParens (pprExpr pdoc e2) pdoc)
-pprApp pdoc e1 e2@App{} = pprExpr pdoc e1
-  `mappend` addSpace (betweenParens (pprExpr pdoc e2) pdoc)
-pprApp pdoc e1 e2@Abs{} = pprExpr pdoc e1
-  `mappend` addSpace (betweenParens (pprExpr pdoc e2) pdoc)
-pprApp pdoc e1@Abs{} e2 = betweenParens (pprExpr pdoc e1) pdoc
-  `mappend` addSpace (pprExpr pdoc e2)
-pprApp pdoc e1 e2
-  = pprExpr pdoc e1 `mappend` addSpace (pprExpr pdoc e2)
-
-pprTApp :: (PrettyPrint n, PrettyPrint t)
-        => PDoc String
-        -> SystemFExpr n t
-        -> Ty t
-        -> PDoc String
-pprTApp pdoc expr ty = expr' `mappend` addSpace (between ty' "[" "]" empty)
-  where expr' = pprExpr pdoc expr
-        ty' = add (prettyPrint ty) empty
-
--- Pretty print an abstraction
-pprAbs :: (PrettyPrint n, PrettyPrint t)
-       => PDoc String
-       -> n
-       -> Ty t
-       -> SystemFExpr n t
-       -> PDoc String
-pprAbs pdoc name ty body = between vars' lambda' ". " (pprExpr pdoc body')
-  where (vars, body') = uncurryAbs name ty body
-        vars' = intercalate (map (uncurry pprArg) vars) " " empty
-        lambda' = [lambda, space]
-
-        pprArg n t = prettyPrint n ++ (':':pprArg' t)
-        pprArg' t@(TyVar _)     = prettyPrint t
-        pprArg' t@(TyArrow _ _) = prettyPrint $ betweenParens (pprTy empty False t) empty
-
--- Pretty print types
-pprTy :: PrettyPrint n
-      => PDoc String
-      -> Bool -- Add a space between arrows?
-      -> Ty n
-      -> PDoc String
-pprTy pdoc space (TyVar n) = prettyPrint n `add` pdoc
-pprTy pdoc space (TyArrow a b) = pprTyArrow pdoc space a b
-pprTy pdoc _     (TyForAll n t) =  pprTyForAll pdoc n t
-
-pprTyArrow :: PrettyPrint n
-           => PDoc String
-           -> Bool -- Add a space between arrows?
-           -> Ty n
-           -> Ty n
-           -> PDoc String
-pprTyArrow pdoc space a@(TyVar _) b = pprTyArrow' space (pprTy pdoc space a) 
-                                                        (pprTy pdoc space b)
-pprTyArrow pdoc space (TyArrow a1 a2) b = pprTyArrow' space a' (pprTy pdoc space b)
-  where a' = betweenParens (pprTyArrow pdoc space a1 a2) empty
-
-pprTyArrow' :: Bool -- Add a space between arrows?
-            -> PDoc String
-            -> PDoc String
-            -> PDoc String
-pprTyArrow' space a b = a <> arrow <> b
-  where arrow | space     = " -> " `add` empty
-              | otherwise = "->" `add` empty
-
-pprTyForAll :: PrettyPrint n
-            => PDoc String
-            -> n
-            -> Ty n
-            -> PDoc String
-pprTyForAll pdoc n t = prefix <> prettyPrint t `add` pdoc
-  where prefix = between (prettyPrint n `add` empty) "forall " ". " empty
-
--- Pretty print a type abstraction
-pprTAbs :: (PrettyPrint n, PrettyPrint t)
-        => PDoc String
-        -> t
-        -> SystemFExpr n t
-        -> PDoc String
-pprTAbs pdoc ty body = between vars' lambda' ". " (pprExpr pdoc body')
-  where (vars, body') = uncurryTAbs ty body
-        vars' = intercalate (map prettyPrint vars) " " empty
-        lambda' = [upperLambda, space]
-
-uncurryAbs :: n -> Ty t -> SystemFExpr n t -> ([(n, Ty t)], SystemFExpr n t)
-uncurryAbs name ty = uncurry' [(name, ty)] 
-  where uncurry' ns (Abs n' t' body') = uncurry' ((n', t'):ns) body'
-        uncurry' ns body'             = (reverse ns, body')
-
-uncurryTAbs :: t -> SystemFExpr n t -> ([t], SystemFExpr n t)
-uncurryTAbs ty = uncurry' [ty]
-  where uncurry' ts (TyAbs t' body') = uncurry' (t':ts) body'
-        uncurry' ts body'            = (reverse ts, body')
diff --git a/src/Language/SystemF/Parser.hs b/src/Language/SystemF/Parser.hs
deleted file mode 100644
--- a/src/Language/SystemF/Parser.hs
+++ /dev/null
@@ -1,86 +0,0 @@
-module Language.SystemF.Parser (
-  parseExpr,
-  parseType
-  ) where
-
-import Control.Monad
-import Prelude hiding (abs)
-
-import Text.Parsec
-import Text.Parsec.String
-
-import Language.SystemF.Expression
-
-parseExpr :: String -> Either ParseError (SystemFExpr String String)
-parseExpr = parse (whitespace *> expr <* eof) ""
-
-parseType :: String -> Either ParseError (Ty String)
-parseType = parse (whitespace *> ty <* eof) ""
-
--- Parse expressions
-expr :: Parser (SystemFExpr String String)
-expr = try tyapp <|> try app <|> term
-
-app :: Parser (SystemFExpr String String)
-app = chainl1 term (return App)
-
-tyapp :: Parser (SystemFExpr String String)
-tyapp = TyApp
-      <$> term
-      <*> ty'
-  where ty' = symbol '[' *> ty <* symbol ']'
-
-term :: Parser (SystemFExpr String String)
-term = try abs <|> tyabs <|> var <|> parens expr
-
-var :: Parser (SystemFExpr String String)
-var = Var <$> exprId
-
-abs :: Parser (SystemFExpr String String)
-abs = curry 
-    <$> (symbol '\\' *> many1 args <* symbol '.') 
-    <*> expr
-  where args = (,) <$> (exprId <* symbol ':') <*> ty
-        curry = flip . foldr . uncurry $ Abs
-
-tyabs :: Parser (SystemFExpr String String)
-tyabs = curry <$> args <*> expr
-  where args = symbol '\\' *> many1 typeId <* symbol '.'
-        curry = flip (foldr TyAbs)
-
--- Parse type expressions
-ty :: Parser (Ty String)
-ty = try arrow
-
-arrow :: Parser (Ty String)
-arrow = chainr1 tyterm (symbol' "->" *> return TyArrow)
-
-tyterm :: Parser (Ty String)
-tyterm = tyvar <|> parens ty
-
-tyvar :: Parser (Ty String)
-tyvar = TyVar <$> typeId
-
-parens :: Parser a -> Parser a
-parens p = symbol '(' *> p <* symbol ')'
-
-identifier :: Parser Char -> Parser String
-identifier firstChar = lexeme ((:) <$> first <*> many rest)
-  where first = firstChar <|> char '_'
-        rest = first <|> digit
-
-typeId, exprId :: Parser String
-typeId = identifier upper
-exprId = identifier lower
-
-whitespace :: Parser ()
-whitespace = void . many . oneOf $ " \t"
-
-symbol :: Char -> Parser ()
-symbol = void . lexeme . char
-
-symbol' :: String -> Parser ()
-symbol' = void . lexeme . string
-
-lexeme :: Parser a -> Parser a
-lexeme p = p <* whitespace
diff --git a/src/Language/SystemF/TypeCheck.hs b/src/Language/SystemF/TypeCheck.hs
deleted file mode 100644
--- a/src/Language/SystemF/TypeCheck.hs
+++ /dev/null
@@ -1,119 +0,0 @@
-module Language.SystemF.TypeCheck where
-
-import Data.Map
-import Prelude hiding (lookup)
-
-import Language.Lambda.Util.PrettyPrint
-import Language.SystemF.Expression
-
-type UniqueSupply n = [n]
-type Context n t = Map n t
-
-typecheck :: (Ord n, Eq n, PrettyPrint n)
-          => UniqueSupply n 
-          -> Context n (Ty n)
-          -> SystemFExpr n n 
-          -> Either String (Ty n)
-typecheck uniqs ctx (Var v)        = tcVar uniqs ctx v
-typecheck uniqs ctx (Abs n t body) = tcAbs uniqs ctx n t body
-typecheck uniqs ctx (App e1 e2)    = tcApp uniqs ctx e1 e2
-typecheck uniqs ctx (TyAbs t body) = tcTyAbs uniqs ctx t body
-typecheck uniqs ctx (TyApp e ty)   = tcTyApp uniqs ctx e ty
-
-tcVar :: (Ord n, Eq n, PrettyPrint n)
-      => UniqueSupply n
-      -> Context n (Ty n)
-      -> n
-      -> Either String (Ty n)
-tcVar uniqs ctx var = maybe (TyVar <$> unique uniqs) return (lookup var ctx)
-
-tcAbs :: (Ord n, Eq n, PrettyPrint n)
-      => UniqueSupply n
-      -> Context n (Ty n)
-      -> n
-      -> Ty n
-      -> SystemFExpr n n
-      -> Either String (Ty n)
-tcAbs uniqs ctx name ty body = TyArrow ty <$> typecheck uniqs ctx' body
-  where ctx' = insert name ty ctx
-
-tcApp :: (Ord n, Eq n, PrettyPrint n)
-      => UniqueSupply n
-      -> Context n (Ty n)
-      -> SystemFExpr n n
-      -> SystemFExpr n n
-      -> Either String (Ty n)
-tcApp uniqs ctx e1 e2 = do
-    t1 <- typecheck uniqs ctx e1
-    t2 <- typecheck uniqs ctx e2
-
-    -- Unwrap t1; Should be (t2 -> *)
-    (t2', t3) <- either genMismatchVar return (arrow t1)
-
-    if t2' == t2
-      then return t3
-      else Left $ tyMismatchMsg (TyArrow t2 t3) (TyArrow t1 t3)
-
-  where genMismatchVar expected = tyMismatchMsg expected <$> unique uniqs >>= Left
-        arrow (TyArrow t1 t2) = return (t1, t2)
-        arrow t               = Left t
-
-tcTyAbs :: (Ord n, Eq n, PrettyPrint n)
-        => UniqueSupply n
-        -> Context n (Ty n)
-        -> n
-        -> SystemFExpr n n
-        -> Either String (Ty n)
-tcTyAbs uniqs ctx ty body = TyForAll ty <$> typecheck uniqs ctx' body
-  where ctx' = insert ty (TyVar ty) ctx
-
-tcTyApp :: (Ord n, Eq n, PrettyPrint n)
-        => UniqueSupply n
-        -> Context n (Ty n)
-        -> SystemFExpr n n
-        -> Ty n
-        -> Either String (Ty n)
-tcTyApp uniqs ctx (TyAbs t expr) ty = typecheck uniqs ctx expr'
-  where expr' = sub t ty expr
-tcTyApp uniqs ctx expr ty = typecheck uniqs ctx expr
-
--- Utilities
-unique :: UniqueSupply t
-       -> Either String t
-unique (u:_) = return u
-unique _     = fail "Unique supply ran out"
-
-sub :: Eq n
-    => n
-    -> Ty n
-    -> SystemFExpr n n
-    -> SystemFExpr n n
-sub name ty (App e1 e2)   = App (sub name ty e1) (sub name ty e2)
-sub name ty (Abs n ty' e) = Abs n (subTy name ty ty') (sub name ty e)
-sub name ty (TyAbs ty' e) = TyAbs ty' (sub name ty e) 
-sub name ty (TyApp e ty') = TyApp (sub name ty e) (subTy name ty ty')
-sub name ty expr = expr
-
-subTy :: Eq n
-      => n
-      -> Ty n
-      -> Ty n
-      -> Ty n
-subTy name ty (TyArrow t1 t2) 
-  = TyArrow (subTy name ty t1) (subTy name ty t2)
-subTy name ty ty'@(TyVar name') 
-  | name == name' = ty
-  | otherwise     = ty'
-subTy name t1 t2@(TyForAll name' t2') 
-  | name == name' = t2
-  | otherwise     = TyForAll name' (subTy name t2 t2')
-
-
-tyMismatchMsg :: (PrettyPrint t, PrettyPrint t')
-              => t
-              -> t'
-              -> String
-tyMismatchMsg expected actual = "Couldn't match expected type " ++
-                                prettyPrint expected ++
-                                " with actual type " ++
-                                prettyPrint actual
diff --git a/test/HLint.hs b/test/HLint.hs
deleted file mode 100644
--- a/test/HLint.hs
+++ /dev/null
@@ -1,16 +0,0 @@
-module Main (main) where
-
-import Language.Haskell.HLint (hlint)
-import System.Exit (exitFailure, exitSuccess)
-
-arguments :: [String]
-arguments = [ 
-  "app",
-  "src",
-  "test"
-  ]
-
-main :: IO ()
-main = hlint arguments >>= main'
-  where main' [] = exitSuccess
-        main' _  = exitFailure
diff --git a/test/Language/Lambda/EvalSpec.hs b/test/Language/Lambda/EvalSpec.hs
deleted file mode 100644
--- a/test/Language/Lambda/EvalSpec.hs
+++ /dev/null
@@ -1,110 +0,0 @@
-module Language.Lambda.EvalSpec where
-
-import Test.Hspec
-
-import Language.Lambda
-import Language.Lambda.Eval
-import Language.Lambda.Expression
-
-spec :: Spec
-spec = do
-  describe "evalExpr" $ do
-    let evalExpr' = evalExpr uniques
-    
-    it "beta reduces" $ do
-      let expr = App (Abs "x" (Var "x")) (Var "z")
-      evalExpr' expr `shouldBe` Var "z"
-
-    it "reduces multiple applications" $ do
-      let expr = App (App (Abs "f" (Abs "x" (App (Var "f") (Var "x")))) (Var "g")) (Var "y")
-      evalExpr' expr `shouldBe` App (Var "g") (Var "y")
-
-    it "reduces inner redexes" $ do
-      let expr = Abs "x" (App (Abs "y" (Var "y")) (Var "x"))
-      evalExpr' expr `shouldBe` Abs "x" (Var "x")
-
-    it "reduces with name captures" $ do
-      let expr = App (Abs "f" (Abs "x" (App (Var "f") (Var "x"))))
-                     (Abs "f" (Var "x"))
-      evalExpr' expr `shouldBe` Abs "z" (Var "x")
-
-  describe "betaReduce" $ do
-    let betaReduce' = betaReduce []
-    
-    it "reduces simple applications" $ do
-      let e1 = Abs "x" (Var "x")
-          e2 = Var "y"
-      betaReduce' e1 e2 `shouldBe` Var "y"
-
-    it "reduces nested abstractions" $ do
-      let e1 = Abs "x" (Abs "y" (Var "x"))
-          e2 = Var "z"
-      betaReduce' e1 e2 `shouldBe` Abs "y" (Var "z")
-
-    it "reduces inner applications" $ do
-      let e1 = Abs "f" (App (Var "f") (Var "x"))
-          e2 = Var "g"
-      betaReduce' e1 e2 `shouldBe` App (Var "g") (Var "x")
-
-    it "does not reduce unreducible expression" $ do
-      let e1 = Var "x"
-          e2 = Var "y"
-      betaReduce' e1 e2 `shouldBe` App (Var "x") (Var "y")
-
-    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" (Abs "x" (Var "x"))
-          e2 = Var "z"
-      betaReduce' e1 e2 `shouldBe` Abs "x" (Var "x")
-
-  describe "alphaConvert" $ do
-    it "alpha converts simple expressions" $ do
-      let freeVars = ["x"]
-          expr = Abs "x" (Var "x")
-          uniques = ["y"]
-      alphaConvert uniques freeVars expr `shouldBe` Abs "y" (Var "y")
-  
-    it "avoids captures" $ do
-      let freeVars = ["x"]
-          expr = Abs "x" (Var "x")
-          uniques = ["x", "y"]
-      alphaConvert uniques freeVars expr `shouldBe` Abs "y" (Var "y")
-
-  describe "etaConvert" $ do
-    it "eta converts simple expressions" $ do
-      let expr = Abs "x" $ App (Var "f") (Var "x")
-      etaConvert expr `shouldBe` Var "f" 
-
-    it "eta converts nested applications" $ do
-      let expr = Abs "y" $ App (App (Var "f") (Var "x")) (Var "y")
-      etaConvert expr `shouldBe` App (Var "f") (Var "x")
-
-      let expr' = Abs "x" $ Abs "y" (App (App (Var "f") (Var "x")) (Var "y"))
-      etaConvert expr' `shouldBe` Var "f" 
-
-      let expr'' = Abs "x" (Abs "y" (App (Var "y") (Var "x")))
-      etaConvert expr'' `shouldBe` expr''
-
-      let expr''' = Abs "f" (Abs "x" (Var "x"))
-      etaConvert expr''' `shouldBe` expr'''
-
-    it "ignores non-eta convertable expressions" $ do
-      let expr = Abs "x" $ Var "x"
-      etaConvert expr `shouldBe` expr
-
-  describe "freeVarsOf" $ do
-    it "Returns simple vars" $
-      freeVarsOf (Var "x") `shouldBe` ["x"]
-  
-    it "Does not return bound vars" $
-      freeVarsOf (Abs "x" (Var "x")) `shouldBe` []
-
-    it "Returns nested simple vars" $
-      freeVarsOf (Abs "x" (Var "y")) `shouldBe` ["y"]
-
-    it "Returns applied simple vars" $
-      freeVarsOf (App (Var "x") (Var "y")) `shouldBe` ["x", "y"]
diff --git a/test/Language/Lambda/Examples/BoolSpec.hs b/test/Language/Lambda/Examples/BoolSpec.hs
deleted file mode 100644
--- a/test/Language/Lambda/Examples/BoolSpec.hs
+++ /dev/null
@@ -1,108 +0,0 @@
-module Language.Lambda.Examples.BoolSpec where
-
-import Test.Hspec
-
-import Language.Lambda.HspecUtils
-
-spec :: Spec
-spec = describe "Bool" $ do
-  -- Bool is the definition of Booleans. We represent bools
-  -- using Church Encodings:
-  --
-  -- true:  \t f. t
-  -- false: \t f. f
-  describe "and" $ do
-    -- The function and takes two Bools and returns true
-    -- iff both arguments are true
-    -- 
-    -- and(true,  true)  = true
-    -- and(false, true)  = false
-    -- and(true,  false) = false
-    -- and(false, false) = false
-    --
-    -- and is defined by
-    -- and = \x y. x y x
-    it "true and true = true" $
-      "(\\x y. x y x) (\\t f. t) (\\t f. t)" `shouldEvalTo` "\\t f. t"
-
-    it "true and false = false" $
-      "(\\x y. x y x) (\\t f. t) (\\t f. f)" `shouldEvalTo` "\\t f. f"
-      
-    it "false and true = false" $
-      "(\\x y. x y x) (\\t f. f) (\\t f. t)" `shouldEvalTo` "\\t f. f"
-
-    it "false and false = false" $
-      "(\\x y. x y x) (\\t f. f) (\\t f. f)" `shouldEvalTo` "\\t f. f"
-
-    it "false and p = false" $
-      "(\\x y. x y x) (\\t f. f) p" `shouldEvalTo` "\\t f. f"
-
-    it "true and p = false" $
-      "(\\x y. x y x) (\\t f. t) p" `shouldEvalTo` "p"
-
-  describe "or" $ do
-    -- or takes two Bools and returns true iff either argument is true
-    -- 
-    -- or(true,  true)  = true
-    -- or(true,  false) = true
-    -- or(false, true)  = true
-    -- or(false, false) = false
-    --
-    -- or is defined by
-    -- or = \x y. x x y
-    it "true or true = true" $
-      "(\\x y. x x y) (\\t f. t) (\\t f. t)" `shouldEvalTo` "\\t f. t"
-    
-    it "true or false = true" $
-      "(\\x y. x x y) (\\t f. t) (\\t f. f)" `shouldEvalTo` "\\t f. t"
-      
-    it "false or true = true" $
-      "(\\x y. x x y) (\\t f. f) (\\t f. t)" `shouldEvalTo` "\\t f. t"
-
-    it "false or false = false" $
-      "(\\x y. x x y) (\\t f. f) (\\t f. f)" `shouldEvalTo` "\\t f. f"
-
-    it "true or p = true" $
-      "(\\x y. x x y) (\\t f. t) p" `shouldEvalTo` "\\t f. t"
-
-    it "false or p = p" $
-      "(\\x y. x x y) (\\t f. f) p" `shouldEvalTo` "p"
-      
-
-  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. x (\\t f. f) (\\t f. t)) \\t f. t" `shouldEvalTo` "\\t f. f"
-
-    it "not false = true" $
-      "(\\x. x (\\t f. f) (\\t f. t)) \\t f. f" `shouldEvalTo` "\\t f. t"
-      
-  describe "if" $ do
-    -- if takes a Bool and two values. If returns the first value
-    -- if the Bool is true, and the second otherwise. In other words,
-    -- if p x y = if p then x else y
-    --
-    -- if(true,  x, y) = x
-    -- if(false, x, y) = y
-    -- 
-    -- if is defined by
-    -- if = \p x y. p x y
-    it "if true 0 1 = 0" $
-      "(\\p x y. p x y) (\\t f. t) (\\f x. x) (\\f x. f x)"
-        `shouldEvalTo` "\\f x. x"
-
-    it "if false 0 1 = 1" $
-      "(\\p x y. p x y) (\\t f. f) (\\f x. x) (\\f x. f x)"
-        `shouldEvalTo` "\\f x. f x"
-
-    it "it true p q = p" $
-      "(\\p x y. p x y) (\\t f. t) p q" `shouldEvalTo` "p"
-
-    it "it false p q = q" $
-      "(\\p x y. p x y) (\\t f. f) p q" `shouldEvalTo` "q"
diff --git a/test/Language/Lambda/Examples/NatSpec.hs b/test/Language/Lambda/Examples/NatSpec.hs
deleted file mode 100644
--- a/test/Language/Lambda/Examples/NatSpec.hs
+++ /dev/null
@@ -1,102 +0,0 @@
-module Language.Lambda.Examples.NatSpec where
-
-import Test.Hspec
-
-import Language.Lambda.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 x. x
-  -- 1: \f x. f x
-  -- 2: \f x. 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 f x. f (n f x)
-    it "succ 0 = 1" $
-      "(\\n f x. f (n f x)) (\\f x. x)" `shouldEvalTo` "\\f x. f x"
-
-    it "succ 1 = 2" $
-      "(\\n f x. f (n f x)) (\\f x. f x)" `shouldEvalTo` "\\f x. f (f x)"
-
-  describe "add" $ do
-    -- add(m, n) = m + n
-    --
-    -- It is defined by applying successor m times on n:
-    -- add = \m n f x. m f (n f x)
-    it "add 0 2 = 2" $
-      "(\\m n f x. m f (n f x)) (\\f x. x) (\\f x. f (f x))"
-        `shouldEvalTo` "\\f x. f (f x)"
-
-    it "add 3 2 = 5" $
-      "(\\m n f x. m f (n f x)) (\\f x. f (f (f x))) (\\f x. f (f x))"
-        `shouldEvalTo` "\\f x. f (f (f (f (f x))))"
-
-    -- Here, we use `\f x. n f x` instead of `n`. This is because
-    -- I haven't implemented eta conversion
-    it "add 0 n = n" $
-      "(\\m n f x. m f (n f x)) (\\f x. x) n"
-        `shouldEvalTo` "\\f x. n 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 n f. m (n f)) (\\f x. x) (\\f x. f (f x))"
-        `shouldEvalTo` "\\f x. x"
-
-    it "multiply 2 3 = 6" $
-      "(\\m n f. m (n f)) (\\f x. f (f x)) (\\f x. f (f (f x)))"
-        `shouldEvalTo` "\\f x. f (f (f (f (f (f x)))))"
-
-    it "multiply 0 n = 0" $
-      "(\\m n f. m (n f)) (\\f x. x) n"
-        `shouldEvalTo` "\\f x. x"
-
-    it "multiply 1 n = n" $
-      "(\\m n f. m (n f)) (\\f x. f x) n"
-        `shouldEvalTo` "\\f x. n f x"
-
-  describe "power" $ do
-    -- The function power raises m to the power of n.
-    -- power(m, n) = m^n
-    --
-    -- power is defined by applying multiply n times
-    -- power = \m n f x. (n m) f x
-    --
-    -- Using eta conversion again, we can omit the parameter f
-    -- power = \m n = n m
-
-    -- NOTE: Here we use the first form to get more predictable
-    -- variable names. Otherwise, alpha conversion will choose a random
-    -- unique variable.
-    it "power 0 1 = 0" $
-      "(\\m n f x. (n m) f x) (\\f x. x) (\\f x. f x)"
-        `shouldEvalTo` "\\f x. x"
-
-    it "power 2 3 = 8" $
-      "(\\m n f x. (n m) f x) (\\f x. f (f x)) (\\f x. f (f (f x)))"
-        `shouldEvalTo` "\\f x. f (f (f (f (f (f (f (f x)))))))"
-
-    it "power n 0 = 1" $
-      "(\\m n f x. (n m) f x) n (\\f x. x)"
-        `shouldEvalTo` "\\f x. f x"
-
-    it "power n 1 = n" $
-      "(\\m n f x. (n m) f x) n (\\f x. f x)"
-        `shouldEvalTo` "\\f x. n f x"
diff --git a/test/Language/Lambda/Examples/PairSpec.hs b/test/Language/Lambda/Examples/PairSpec.hs
deleted file mode 100644
--- a/test/Language/Lambda/Examples/PairSpec.hs
+++ /dev/null
@@ -1,38 +0,0 @@
-module Language.Lambda.Examples.PairSpec where
-
-import Language.Lambda.HspecUtils
-
-import Test.Hspec
-
-spec :: Spec
-spec = describe "Pair" $ do
-  -- Pair is the definition of tuples with two items. Pairs,
-  -- again are represented using Church Encodings:
-  --
-  -- pair = \x y f. f x y
-  describe "first" $ do
-    -- The function first returns the first item in a pair
-    -- first(x, y) = x
-    --
-    -- first is defined by
-    -- first = \p. p (\t f. t)
-    it "first 0 1 = 0" $
-      "(\\p. p (\\t f. t)) ((\\x y f. f x y) (\\f x. x) (\\f x. f x))"
-        `shouldEvalTo` "\\f x. x"
-
-    it "first x y = x" $
-      "(\\p. p (\\t f. t)) ((\\x y f. f x y) x y)" `shouldEvalTo` "x"
-
-  describe "second" $ do
-    -- The function second returns the second item in a pair
-    -- second(x, y) = y
-    --
-    -- second is defined by
-    -- second = \p. p (\t f. f)
-    it "second 0 1 = 1" $
-      "(\\p. p (\\t f. f)) ((\\x y f. f x y) (\\f x. x) (\\f x. f x))"
-        `shouldEvalTo` "\\f x. f x"
-
-    it "second x y = y" $ do
-      "(\\p. p (\\t f. f)) ((\\x y f. f x y) x y)" `shouldEvalTo` "y"
-      "(\\p. p (\\x y z. x)) ((\\x y z f. f x y z) x y z)" `shouldEvalTo` "x"
diff --git a/test/Language/Lambda/ExpressionSpec.hs b/test/Language/Lambda/ExpressionSpec.hs
deleted file mode 100644
--- a/test/Language/Lambda/ExpressionSpec.hs
+++ /dev/null
@@ -1,39 +0,0 @@
-module Language.Lambda.ExpressionSpec where
-
-import Test.Hspec
-
-import Language.Lambda.Expression
-import Language.Lambda.Util.PrettyPrint
-
-spec :: Spec
-spec = describe "prettyPrint" $ do
-    it "prints simple variables" $ 
-      prettyPrint (Var "x") `shouldBe` "x"
-
-    it "prints simple abstractions" $
-      prettyPrint (Abs "x" (Var "x")) `shouldBe` "λx. x"
-
-    it "prints simple applications" $
-      prettyPrint (App (Var "a") (Var "b"))
-        `shouldBe` "a b"
-
-    it "prints nested abstractions" $
-      prettyPrint (Abs "f" (Abs "x" (Var "x")))
-        `shouldBe` "λf x. x"
-
-    it "prints nested applications" $
-      prettyPrint (App (App (Var "f") (Var "x")) (Var "y"))
-        `shouldBe` "f x y"
-
-    it "prints parenthesized applications" $ do
-      prettyPrint (App (Var "f") (App (Var "x") (Var "y")))
-        `shouldBe` "f (x y)"
-
-      prettyPrint (App (Abs "x" (Var "x")) (Var "y"))
-        `shouldBe` "(λx. x) y"
-
-      prettyPrint (App (Var "x") (Abs "f" (Var "f")))
-        `shouldBe` "x (λf. f)"
-      
-      prettyPrint (App (Abs "f" (Var "f")) (Abs "g" (Var "g")))
-        `shouldBe` "(λf. f) (λg. g)"
diff --git a/test/Language/Lambda/HspecUtils.hs b/test/Language/Lambda/HspecUtils.hs
deleted file mode 100644
--- a/test/Language/Lambda/HspecUtils.hs
+++ /dev/null
@@ -1,11 +0,0 @@
-module Language.Lambda.HspecUtils where
-
-import Test.Hspec
-
-import Language.Lambda
-
-shouldEvalTo :: String -> String -> Expectation
-shouldEvalTo s1 = shouldBe (eval s1) . eval
-
-eval :: String -> Either ParseError (LambdaExpr String)
-eval = evalString
diff --git a/test/Language/Lambda/ParserSpec.hs b/test/Language/Lambda/ParserSpec.hs
deleted file mode 100644
--- a/test/Language/Lambda/ParserSpec.hs
+++ /dev/null
@@ -1,53 +0,0 @@
-module Language.Lambda.ParserSpec (spec) where
-
-import Data.Either
-
-import Test.Hspec
-
-import Language.Lambda.Expression
-import Language.Lambda.Parser
-
-spec :: Spec
-spec = describe "parseExpr" $ do
-  it "parses simple variables" $
-    parseExpr "x" `shouldBe` Right (Var "x")
-
-  it "parses parenthesized variables" $
-    parseExpr "(x)" `shouldBe` Right (Var "x")
-
-  it "parses simple abstractions" $
-    parseExpr "\\x. x" `shouldBe` Right (Abs "x" (Var "x"))
-
-  it "parses nested abstractions" $
-    parseExpr "\\f a. a" `shouldBe` Right (Abs "f" (Abs "a" (Var "a")))
-
-  it "parses simple applications" $
-    parseExpr "f x" `shouldBe` Right (App (Var "f") (Var "x"))
-
-  it "parses chained applications" $
-    parseExpr "f x y" `shouldBe` Right (App (App (Var "f") (Var "x")) (Var "y"))
-
-  it "parses complex expressions" $ do
-    let exprs = [
-          "\\f x. f x",
-          "(\\p x y. y) (\\p x y. x)",
-          "f (\\x. x)",
-          "(\\x . f x) g y",
-          "(\\f . (\\ x y. f x y) f x y) w x y"
-          ]
-    
-    mapM_ (flip shouldSatisfy isRight . parseExpr) exprs
-
-  it "does not parse trailing errors" $
-    parseExpr "x +" `shouldSatisfy` isLeft
-
-  it "ignores whitespace" $ do
-    let exprs = [
-          " x ",
-          " \\ x . x ",
-          " ( x ) "
-          ]
-    
-    mapM_ (flip shouldSatisfy isRight . parseExpr) exprs
-            
-
diff --git a/test/Language/Lambda/SystemF/ExpressionSpec.hs b/test/Language/Lambda/SystemF/ExpressionSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Language/Lambda/SystemF/ExpressionSpec.hs
@@ -0,0 +1,87 @@
+{-# LANGUAGE OverloadedStrings, NoImplicitPrelude #-}
+module Language.Lambda.SystemF.ExpressionSpec where
+
+import RIO
+import Test.Hspec
+
+import Language.Lambda.SystemF.Expression
+
+spec :: Spec
+spec = describe "prettyPrint" $ do
+  let prettyPrint' :: SystemFExpr Text Text -> Text
+      prettyPrint' = prettyPrint
+
+      prettyPrintTy :: Ty Text -> Text
+      prettyPrintTy = prettyPrint
+  
+  it "prints simple variables" $
+    prettyPrint' (Var "x") `shouldBe` "x"
+
+  it "prints simple applications" $
+    prettyPrint' (App (Var "a") (Var "b")) `shouldBe` "a b"
+
+  it "prints simple abstractions" $ 
+    prettyPrint' (Abs "x" (TyVar "T") (Var "x")) `shouldBe` "λ x:T. x"
+
+  it "prints simple type abstractions" $
+    prettyPrint' (TyAbs "X" (Var "x")) `shouldBe` "Λ X. x"
+
+  it "prints simple type applications" $ 
+    prettyPrint' (TyApp (Var "t") (TyVar "T")) `shouldBe` "t [T]"
+
+  it "prints nested abstractions" $
+    prettyPrint' (Abs "f" (TyVar "F") (Abs "x" (TyVar "X") (Var "x")))
+      `shouldBe` "λ f:F x:X. x"
+
+  it "prints abstractions with composite types" $ do
+    prettyPrint' (Abs "f" (TyArrow (TyVar "X") (TyVar "Y")) (Var "f"))
+      `shouldBe ` "λ f:(X->Y). f"
+
+    prettyPrint' (Abs "f" (TyArrow (TyVar "X") (TyArrow (TyVar "Y") (TyVar "Z"))) (Var "f"))
+      `shouldBe ` "λ f:(X->Y->Z). f"
+
+  it "prints nested type abstractions" $
+    prettyPrint' (TyAbs "A" (TyAbs "B" (Var "x")))
+      `shouldBe` "Λ A B. x"
+
+  it "prints nested applications" $
+    prettyPrint' (App (App (Var "f") (Var "x")) (Var "y"))
+      `shouldBe` "f x y"
+
+  it "prints parenthesized applications" $ do
+    prettyPrint' (App (Var "w") (App (Var "x") (Var "y")))
+      `shouldBe` "w (x y)"
+
+    prettyPrint' (App (Abs "t" (TyVar "T") (Var "t")) (Var "x"))
+      `shouldBe` "(λ t:T. t) x"
+
+    prettyPrint' (App (Abs "f" (TyVar "F") (Var "f")) (Abs "g" (TyVar "G") (Var "g")))
+      `shouldBe` "(λ f:F. f) (λ g:G. g)"
+
+  it "prints simple types" $
+    prettyPrintTy (TyVar "X") `shouldBe` "X"
+
+  it "print simple arrow types" $
+    prettyPrintTy (TyArrow (TyVar "A") (TyVar "B")) `shouldBe` "A -> B"
+
+  it "prints simple forall types" $
+    prettyPrintTy (TyForAll "X" (TyVar "X")) `shouldBe` "forall X. X"
+
+  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"
+
diff --git a/test/Language/Lambda/SystemF/ParserSpec.hs b/test/Language/Lambda/SystemF/ParserSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Language/Lambda/SystemF/ParserSpec.hs
@@ -0,0 +1,86 @@
+{-# LANGUAGE NoImplicitPrelude, OverloadedStrings #-}
+module Language.Lambda.SystemF.ParserSpec (spec) where
+
+import Data.Either
+
+import RIO
+import Test.Hspec
+
+import Language.Lambda.SystemF.Expression
+import Language.Lambda.SystemF.Parser
+
+spec :: Spec
+spec = do
+  describe "parseExpr" $ do
+    it "parses simple variables" $
+      parseExpr "x" `shouldBe` Right (Var "x")
+
+    it "parses parenthesized variables" $
+      parseExpr "(x)" `shouldBe` Right (Var "x")
+
+    it "parses simple abstractions" $
+      parseExpr "\\x:T. x" `shouldBe` Right (Abs "x" (TyVar "T") (Var "x"))
+
+    it "parses simple type abstractions" $
+      parseExpr "\\X. x" `shouldBe` Right (TyAbs "X" (Var "x"))
+
+    it "parses simple type applications" $ 
+      parseExpr "x [T]" `shouldBe` Right (TyApp (Var "x") (TyVar "T"))
+
+    it "parses nested abstractions" $
+      parseExpr "\\a:A b:B. b" 
+        `shouldBe` Right (Abs "a" (TyVar "A") (Abs "b" (TyVar "B") (Var "b")))
+
+    it "parses abstractions with arrow types" $
+      parseExpr "\\f:(T->U). f"
+        `shouldBe` Right (Abs "f" (TyArrow (TyVar "T") (TyVar "U")) (Var "f"))
+
+    it "parses simple applications" $
+      parseExpr "f x" `shouldBe` Right (App (Var "f") (Var "x"))
+
+    it "parses chained applications" $
+      parseExpr "a b c" `shouldBe` Right (App (App (Var "a") (Var "b")) (Var "c"))
+
+    it "parses complex expressions"  $ do
+      let exprs = [
+            "\\f:(A->B) x:B. f x",
+            "(\\p:(X->Y->Z) x:X y:Y. y) (\\p:(A->B->C) x:B y:C. x)",
+            "f (\\x:T. x)",
+            "(\\ x:X . f x) g y",
+            "(\\f:(X->Y) . (\\ x:X y:Y. f x y) f x y) w x y",
+            "(\\x:T. x) [U]"
+            ]
+
+      mapM_ (flip shouldSatisfy isRight . parseExpr) exprs
+
+    it "does not parse trailing errors" $
+      parseExpr "x +" `shouldSatisfy` isLeft
+
+    it "ignores whitespace" $ do
+      let exprs = [
+            " x ",
+            " \\ x : X. x ",
+            " ( x ) "
+            ]
+
+      mapM_ (flip shouldSatisfy isRight . parseExpr) exprs
+  
+  describe "parseType" $ do
+    it "parses simple variables" $
+      parseType "X" `shouldBe` Right (TyVar "X")
+
+    it "parses parenthesized variables" $
+      parseType "(T)" `shouldBe` Right (TyVar "T")
+
+    it "parses simple arrow types" $
+      parseType "A -> B" `shouldBe` Right (TyArrow (TyVar "A") (TyVar "B")) 
+
+    it "parses parenthesized arrow types" $
+      parseType "((X)->(Y))" `shouldBe` Right (TyArrow (TyVar "X") (TyVar "Y"))
+
+    it "parses nested arrow types" $ do
+      parseType "T -> U -> V" 
+        `shouldBe` Right (TyArrow (TyVar "T") (TyArrow (TyVar "U") (TyVar "V")))
+
+      parseType "(W -> V) -> U"
+        `shouldBe` Right (TyArrow (TyArrow (TyVar "W") (TyVar "V")) (TyVar "U"))
diff --git a/test/Language/Lambda/SystemF/TypeCheckSpec.hs b/test/Language/Lambda/SystemF/TypeCheckSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Language/Lambda/SystemF/TypeCheckSpec.hs
@@ -0,0 +1,71 @@
+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
+
+tc uniqs ctx expr = execTypecheck (typecheck expr) (TypecheckState (fromList ctx) uniqs)
+
+spec :: Spec
+spec = describe "typecheck" $ do
+  it "typechecks simple variables in context" $
+    tc [] [("x", TyVar "X")] (Var "x") `shouldBe` Right (TyVar "X")
+
+  it "typechecks simple variables not in context" $ 
+    tc ["A"] [] (Var "x") `shouldBe` Right (TyVar "A")
+
+  it "typechecks simple abstractions" $
+    tc [] [] (Abs "x" (TyVar "A") (Var "x")) 
+      `shouldBe` Right (TyArrow (TyVar "A") (TyVar "A"))
+
+  it "typechecks simple applications" $ do
+    let ctx = [
+          ("f", TyArrow (TyVar "T") (TyVar "U")),
+          ("a", TyVar "T")
+          ]
+
+    tc [] ctx (App (Var "f") (Var "a")) `shouldBe` Right (TyVar "U")
+
+  it "apply variable to variable fails" $ do
+    let ctx = [
+          ("a", TyVar "A"),
+          ("b", TyVar "B")
+          ]
+
+    tc ["C"] ctx (App (Var "a") (Var "b")) 
+      `shouldSatisfy` isLeft
+
+  it "apply arrow to variable of wrong type fails" $ do
+    let ctx = [
+          ("f", TyArrow (TyVar "F") (TyVar "G")),
+          ("b", TyVar "B")
+          ]
+
+    tc [] ctx (App (Var "f") (Var "b")) `shouldSatisfy` isLeft
+
+  it "typechecks simple type abstractions" $
+    tc ["A"] [] (TyAbs "X" (Var "x")) `shouldBe` Right (TyForAll "X" (TyVar "A"))
+
+  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 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")
+
+  it "typechecks simple type applications" $
+    tc [] [("x", TyVar "A")] (TyApp (TyAbs "X" (Var "x")) (TyVar "X"))
+      `shouldBe` Right (TyVar "A")
+
+  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"))
diff --git a/test/Language/Lambda/SystemFSpec.hs b/test/Language/Lambda/SystemFSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Language/Lambda/SystemFSpec.hs
@@ -0,0 +1,9 @@
+module Language.Lambda.SystemFSpec where
+
+import Test.Hspec
+
+import Language.Lambda.SystemF
+
+spec :: Spec
+spec = describe "evalString" $ 
+  return ()
diff --git a/test/Language/Lambda/Untyped/EvalSpec.hs b/test/Language/Lambda/Untyped/EvalSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Language/Lambda/Untyped/EvalSpec.hs
@@ -0,0 +1,160 @@
+{-# LANGUAGE NoImplicitPrelude, OverloadedStrings #-}
+module Language.Lambda.Untyped.EvalSpec where
+
+import Data.Map (fromList)
+import RIO
+import Test.Hspec
+
+import Language.Lambda.Shared.Errors
+import Language.Lambda.Untyped
+import Language.Lambda.Untyped.Eval
+import Language.Lambda.Untyped.State
+
+spec :: Spec
+spec = do
+  describe "evalExpr" $ do
+    let evalExpr' expr = execEval (evalExpr expr) (mkEvalState defaultUniques)
+
+    it "beta reduces" $ do
+      let expr = App (Abs "x" (Var "x")) (Var "z")
+      evalExpr' expr `shouldBe` Right (Var "z")
+
+    it "reduces multiple applications" $ do
+      let expr = App (App (Abs "f" (Abs "x" (App (Var "f") (Var "x")))) (Var "g")) (Var "y")
+      evalExpr' expr `shouldBe` Right (App (Var "g") (Var "y"))
+
+    it "reduces inner redexes" $ do
+      let expr = Abs "x" (App (Abs "y" (Var "y")) (Var "x"))
+      evalExpr' expr `shouldBe` Right (Abs "x" (Var "x"))
+
+    it "reduces with name captures" $ do
+      let expr = App (Abs "f" (Abs "x" (App (Var "f") (Var "x"))))
+                     (Abs "f" (Var "x"))
+      evalExpr' expr `shouldBe` Right (Abs "z" (Var "x"))
+
+    it "reduces let bodies" $ do
+      let expr = Let "x" $ App (Abs "y" (Var "y")) (Var "z")
+      evalExpr' expr `shouldBe` Right (Let "x" (Var "z"))
+
+    it "let expressions update state" $ do
+      let res = flip unsafeExecEval (mkEvalState defaultUniques) $ do
+            _ <- evalExpr $ Let "w" (Var "x")
+            evalExpr $ Var "w"
+
+      res `shouldBe` Var "x"
+
+    it "nested let expressions fail" $ do
+      let res = flip unsafeExecEval (mkEvalState defaultUniques) $ do
+            evalExpr $ Let "x" (Let "y" (Var "z"))
+      evaluate res `shouldThrow` isLetError
+
+  describe "subGlobals" $ do
+    let globals' :: Map String (LambdaExpr String)
+        globals' = fromList [("w", Var "x")] 
+        subGlobals' = subGlobals globals'
+    
+    it "subs simple variables" $
+      subGlobals' (Var "w") `shouldBe` Var "x"
+
+    it "does not sub shadowed bindings" $ do
+      let expr = Abs "w" (Var "w")
+      subGlobals' expr `shouldBe` expr
+
+    xit "does not capture globals" $ do
+      let expr = Abs "x" (Var "w")
+      subGlobals' expr `shouldBe` Abs "a" (Var "x")
+
+  describe "betaReduce" $ do
+    let betaReduce' :: LambdaExpr Text -> LambdaExpr Text -> LambdaExpr Text
+        betaReduce' e1 e2 = unsafeExecEval (betaReduce e1 e2) (mkEvalState [])
+    
+    it "reduces simple applications" $ do
+      let e1 = Abs "x" (Var "x")
+          e2 = Var "y"
+      betaReduce' e1 e2 `shouldBe` Var "y"
+
+    it "reduces nested abstractions" $ do
+      let e1 = Abs "x" (Abs "y" (Var "x"))
+          e2 = Var "z"
+      betaReduce' e1 e2 `shouldBe` Abs "y" (Var "z")
+
+    it "reduces inner applications" $ do
+      let e1 = Abs "f" (App (Var "f") (Var "x"))
+          e2 = Var "g"
+      betaReduce' e1 e2 `shouldBe` App (Var "g") (Var "x")
+
+    it "does not reduce unreducible expression" $ do
+      let e1 = Var "x"
+          e2 = Var "y"
+      betaReduce' e1 e2 `shouldBe` App (Var "x") (Var "y")
+
+    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" (Abs "x" (Var "x"))
+          e2 = Var "z"
+      betaReduce' e1 e2 `shouldBe` Abs "x" (Var "x")
+
+  describe "alphaConvert" $ do
+    let alphaConvert' :: [Text] -> [Text] -> LambdaExpr Text -> LambdaExpr Text
+        alphaConvert' uniques' fvs expr
+          = unsafeExecEval (alphaConvert fvs expr) (mkEvalState uniques')
+    
+    it "alpha converts simple expressions" $ do
+      let freeVars = ["x"] :: [Text]
+          expr = Abs "x" (Var "x")
+          uniques' = ["y"]
+      alphaConvert' uniques' freeVars expr `shouldBe` Abs "y" (Var "y")
+  
+    it "avoids captures" $ do
+      let freeVars = ["x"]
+          expr = Abs "x" (Var "x")
+          uniques' = ["x", "y"]
+      alphaConvert' uniques' freeVars expr `shouldBe` Abs "y" (Var "y")
+
+  describe "etaConvert" $ do
+    it "eta converts simple expressions" $ do
+      let expr :: LambdaExpr Text
+          expr = Abs "x" $ App (Var "f") (Var "x") :: LambdaExpr Text
+      etaConvert expr `shouldBe` Var "f" 
+
+    it "eta converts nested applications" $ do
+      let expr :: LambdaExpr Text
+          expr = Abs "y" $ App (App (Var "f") (Var "x")) (Var "y")
+      etaConvert expr `shouldBe` App (Var "f") (Var "x")
+
+      let expr' :: LambdaExpr Text
+          expr' = Abs "x" $ Abs "y" (App (App (Var "f") (Var "x")) (Var "y"))
+      etaConvert expr' `shouldBe` Var "f" 
+
+      let expr'' :: LambdaExpr Text
+          expr'' = Abs "x" (Abs "y" (App (Var "y") (Var "x")))
+      etaConvert expr'' `shouldBe` expr''
+
+      let expr''' :: LambdaExpr Text
+          expr''' = Abs "f" (Abs "x" (Var "x"))
+      etaConvert expr''' `shouldBe` expr'''
+
+    it "ignores non-eta convertable expressions" $ do
+      let expr :: LambdaExpr Text
+          expr = Abs "x" $ Var "x"
+      etaConvert expr `shouldBe` expr
+
+  describe "freeVarsOf" $ do
+    let freeVarsOf' :: LambdaExpr Text -> [Text]
+        freeVarsOf' = freeVarsOf
+    
+    it "Returns simple vars" $
+      freeVarsOf' (Var "x") `shouldBe` ["x"]
+  
+    it "Does not return bound vars" $
+      freeVarsOf' (Abs "x" (Var "x")) `shouldBe` []
+
+    it "Returns nested simple vars" $
+      freeVarsOf' (Abs "x" (Var "y")) `shouldBe` ["y"]
+
+    it "Returns applied simple vars" $
+      freeVarsOf' (App (Var "x") (Var "y")) `shouldBe` ["x", "y"]
diff --git a/test/Language/Lambda/Untyped/Examples/BoolSpec.hs b/test/Language/Lambda/Untyped/Examples/BoolSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Language/Lambda/Untyped/Examples/BoolSpec.hs
@@ -0,0 +1,110 @@
+{-# LANGUAGE NoImplicitPrelude, OverloadedStrings #-}
+module Language.Lambda.Untyped.Examples.BoolSpec where
+
+import RIO
+import Test.Hspec
+
+import Language.Lambda.Untyped.HspecUtils
+
+spec :: Spec
+spec = describe "Bool" $ do
+  -- Bool is the definition of Booleans. We represent bools
+  -- using Church Encodings:
+  --
+  -- true:  \t f. t
+  -- false: \t f. f
+  describe "and" $ do
+    -- The function and takes two Bools and returns true
+    -- iff both arguments are true
+    -- 
+    -- and(true,  true)  = true
+    -- and(false, true)  = false
+    -- and(true,  false) = false
+    -- and(false, false) = false
+    --
+    -- and is defined by
+    -- and = \x y. x y x
+    it "true and true = true" $
+      "(\\x y. x y x) (\\t f. t) (\\t f. t)" `shouldEvalTo` "\\t f. t"
+
+    it "true and false = false" $
+      "(\\x y. x y x) (\\t f. t) (\\t f. f)" `shouldEvalTo` "\\t f. f"
+      
+    it "false and true = false" $
+      "(\\x y. x y x) (\\t f. f) (\\t f. t)" `shouldEvalTo` "\\t f. f"
+
+    it "false and false = false" $
+      "(\\x y. x y x) (\\t f. f) (\\t f. f)" `shouldEvalTo` "\\t f. f"
+
+    it "false and p = false" $
+      "(\\x y. x y x) (\\t f. f) p" `shouldEvalTo` "\\t f. f"
+
+    it "true and p = false" $
+      "(\\x y. x y x) (\\t f. t) p" `shouldEvalTo` "p"
+
+  describe "or" $ do
+    -- or takes two Bools and returns true iff either argument is true
+    -- 
+    -- or(true,  true)  = true
+    -- or(true,  false) = true
+    -- or(false, true)  = true
+    -- or(false, false) = false
+    --
+    -- or is defined by
+    -- or = \x y. x x y
+    it "true or true = true" $
+      "(\\x y. x x y) (\\t f. t) (\\t f. t)" `shouldEvalTo` "\\t f. t"
+    
+    it "true or false = true" $
+      "(\\x y. x x y) (\\t f. t) (\\t f. f)" `shouldEvalTo` "\\t f. t"
+      
+    it "false or true = true" $
+      "(\\x y. x x y) (\\t f. f) (\\t f. t)" `shouldEvalTo` "\\t f. t"
+
+    it "false or false = false" $
+      "(\\x y. x x y) (\\t f. f) (\\t f. f)" `shouldEvalTo` "\\t f. f"
+
+    it "true or p = true" $
+      "(\\x y. x x y) (\\t f. t) p" `shouldEvalTo` "\\t f. t"
+
+    it "false or p = p" $
+      "(\\x y. x x y) (\\t f. f) p" `shouldEvalTo` "p"
+      
+
+  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. x (\\t f. f) (\\t f. t)) \\t f. t" `shouldEvalTo` "\\t f. f"
+
+    it "not false = true" $
+      "(\\x. x (\\t f. f) (\\t f. t)) \\t f. f" `shouldEvalTo` "\\t f. t"
+      
+  describe "if" $ do
+    -- if takes a Bool and two values. If returns the first value
+    -- if the Bool is true, and the second otherwise. In other words,
+    -- if p x y = if p then x else y
+    --
+    -- if(true,  x, y) = x
+    -- if(false, x, y) = y
+    -- 
+    -- if is defined by
+    -- if = \p x y. p x y
+    it "if true 0 1 = 0" $
+      "(\\p x y. p x y) (\\t f. t) (\\f x. x) (\\f x. f x)"
+        `shouldEvalTo` "\\f x. x"
+
+    it "if false 0 1 = 1" $
+      "(\\p x y. p x y) (\\t f. f) (\\f x. x) (\\f x. f x)"
+        `shouldEvalTo` "\\f x. f x"
+
+    it "it true p q = p" $
+      "(\\p x y. p x y) (\\t f. t) p q" `shouldEvalTo` "p"
+
+    it "it false p q = q" $
+      "(\\p x y. p x y) (\\t f. f) p q" `shouldEvalTo` "q"
diff --git a/test/Language/Lambda/Untyped/Examples/NatSpec.hs b/test/Language/Lambda/Untyped/Examples/NatSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Language/Lambda/Untyped/Examples/NatSpec.hs
@@ -0,0 +1,104 @@
+{-# LANGUAGE NoImplicitPrelude, OverloadedStrings #-}
+module Language.Lambda.Untyped.Examples.NatSpec where
+
+import RIO
+import Test.Hspec
+
+import Language.Lambda.Untyped.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 x. x
+  -- 1: \f x. f x
+  -- 2: \f x. 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 f x. f (n f x)
+    it "succ 0 = 1" $
+      "(\\n f x. f (n f x)) (\\f x. x)" `shouldEvalTo` "\\f x. f x"
+
+    it "succ 1 = 2" $
+      "(\\n f x. f (n f x)) (\\f x. f x)" `shouldEvalTo` "\\f x. f (f x)"
+
+  describe "add" $ do
+    -- add(m, n) = m + n
+    --
+    -- It is defined by applying successor m times on n:
+    -- add = \m n f x. m f (n f x)
+    it "add 0 2 = 2" $
+      "(\\m n f x. m f (n f x)) (\\f x. x) (\\f x. f (f x))"
+        `shouldEvalTo` "\\f x. f (f x)"
+
+    it "add 3 2 = 5" $
+      "(\\m n f x. m f (n f x)) (\\f x. f (f (f x))) (\\f x. f (f x))"
+        `shouldEvalTo` "\\f x. f (f (f (f (f x))))"
+
+    -- Here, we use `\f x. n f x` instead of `n`. This is because
+    -- I haven't implemented eta conversion
+    it "add 0 n = n" $
+      "(\\m n f x. m f (n f x)) (\\f x. x) n"
+        `shouldEvalTo` "\\f x. n 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 n f. m (n f)) (\\f x. x) (\\f x. f (f x))"
+        `shouldEvalTo` "\\f x. x"
+
+    it "multiply 2 3 = 6" $
+      "(\\m n f. m (n f)) (\\f x. f (f x)) (\\f x. f (f (f x)))"
+        `shouldEvalTo` "\\f x. f (f (f (f (f (f x)))))"
+
+    it "multiply 0 n = 0" $
+      "(\\m n f. m (n f)) (\\f x. x) n"
+        `shouldEvalTo` "\\f x. x"
+
+    it "multiply 1 n = n" $
+      "(\\m n f. m (n f)) (\\f x. f x) n"
+        `shouldEvalTo` "\\f x. n f x"
+
+  describe "power" $ do
+    -- The function power raises m to the power of n.
+    -- power(m, n) = m^n
+    --
+    -- power is defined by applying multiply n times
+    -- power = \m n f x. (n m) f x
+    --
+    -- Using eta conversion again, we can omit the parameter f
+    -- power = \m n = n m
+
+    -- NOTE: Here we use the first form to get more predictable
+    -- variable names. Otherwise, alpha conversion will choose a random
+    -- unique variable.
+    it "power 0 1 = 0" $
+      "(\\m n f x. (n m) f x) (\\f x. x) (\\f x. f x)"
+        `shouldEvalTo` "\\f x. x"
+
+    it "power 2 3 = 8" $
+      "(\\m n f x. (n m) f x) (\\f x. f (f x)) (\\f x. f (f (f x)))"
+        `shouldEvalTo` "\\f x. f (f (f (f (f (f (f (f x)))))))"
+
+    it "power n 0 = 1" $
+      "(\\m n f x. (n m) f x) n (\\f x. x)"
+        `shouldEvalTo` "\\f x. f x"
+
+    it "power n 1 = n" $
+      "(\\m n f x. (n m) f x) n (\\f x. f x)"
+        `shouldEvalTo` "\\f x. n f x"
diff --git a/test/Language/Lambda/Untyped/Examples/PairSpec.hs b/test/Language/Lambda/Untyped/Examples/PairSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Language/Lambda/Untyped/Examples/PairSpec.hs
@@ -0,0 +1,40 @@
+{-# LANGUAGE NoImplicitPrelude, OverloadedStrings #-}
+module Language.Lambda.Untyped.Examples.PairSpec where
+
+import Language.Lambda.Untyped.HspecUtils
+
+import RIO
+import Test.Hspec
+
+spec :: Spec
+spec = describe "Pair" $ do
+  -- Pair is the definition of tuples with two items. Pairs,
+  -- again are represented using Church Encodings:
+  --
+  -- pair = \x y f. f x y
+  describe "first" $ do
+    -- The function first returns the first item in a pair
+    -- first(x, y) = x
+    --
+    -- first is defined by
+    -- first = \p. p (\t f. t)
+    it "first 0 1 = 0" $
+      "(\\p. p (\\t f. t)) ((\\x y f. f x y) (\\f x. x) (\\f x. f x))"
+        `shouldEvalTo` "\\f x. x"
+
+    it "first x y = x" $
+      "(\\p. p (\\t f. t)) ((\\x y f. f x y) x y)" `shouldEvalTo` "x"
+
+  describe "second" $ do
+    -- The function second returns the second item in a pair
+    -- second(x, y) = y
+    --
+    -- second is defined by
+    -- second = \p. p (\t f. f)
+    it "second 0 1 = 1" $
+      "(\\p. p (\\t f. f)) ((\\x y f. f x y) (\\f x. x) (\\f x. f x))"
+        `shouldEvalTo` "\\f x. f x"
+
+    it "second x y = y" $ do
+      "(\\p. p (\\t f. f)) ((\\x y f. f x y) x y)" `shouldEvalTo` "y"
+      "(\\p. p (\\x y z. x)) ((\\x y z f. f x y z) x y z)" `shouldEvalTo` "x"
diff --git a/test/Language/Lambda/Untyped/ExpressionSpec.hs b/test/Language/Lambda/Untyped/ExpressionSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Language/Lambda/Untyped/ExpressionSpec.hs
@@ -0,0 +1,50 @@
+{-# LANGUAGE NoImplicitPrelude, OverloadedStrings #-}
+module Language.Lambda.Untyped.ExpressionSpec where
+
+import Language.Lambda.Untyped.Expression
+
+import RIO
+import Test.Hspec
+
+spec :: Spec
+spec = describe "prettyPrint" $ do
+    let prettyPrint' :: LambdaExpr Text -> Text
+        prettyPrint' = prettyPrint
+  
+    it "prints simple variables" $
+      prettyPrint' (Var "x") `shouldBe` "x"
+
+    it "prints simple abstractions" $
+      prettyPrint' (Abs "x" (Var "x")) `shouldBe` "λx. x"
+
+    it "prints simple applications" $
+      prettyPrint' (App (Var "a") (Var "b"))
+        `shouldBe` "a b"
+
+    it "prints simple let expressions" $
+      prettyPrint' (Let "x" (Var "y")) `shouldBe` "let x = y"
+
+    it "prints nested abstractions" $
+      prettyPrint' (Abs "f" (Abs "x" (Abs "y" (Var "x"))))
+        `shouldBe` "λf x y. x"
+
+    it "prints nested applications" $
+      prettyPrint' (App (App (Var "f") (Var "x")) (Var "y"))
+        `shouldBe` "f x y"
+
+    it "prints parenthesized applications" $ do
+      prettyPrint' (App (Var "f") (App (Var "x") (Var "y")))
+        `shouldBe` "f (x y)"
+
+      prettyPrint' (App (Abs "x" (Var "x")) (Var "y"))
+        `shouldBe` "(λx. x) y"
+
+      prettyPrint' (App (Var "x") (Abs "f" (Var "f")))
+        `shouldBe` "x (λf. f)"
+      
+      prettyPrint' (App (Abs "f" (Var "f")) (Abs "g" (Var "g")))
+        `shouldBe` "(λf. f) (λg. g)"
+
+    it "prints complex let expressions" $
+      prettyPrint' (Let "x" (Abs "a" (Abs "b" (App (Var "a") (Var "b")))))
+        `shouldBe` "let x = λa b. a b"
diff --git a/test/Language/Lambda/Untyped/HspecUtils.hs b/test/Language/Lambda/Untyped/HspecUtils.hs
new file mode 100644
--- /dev/null
+++ b/test/Language/Lambda/Untyped/HspecUtils.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+module Language.Lambda.Untyped.HspecUtils where
+
+import RIO
+import Test.Hspec
+
+import Language.Lambda.Shared.Errors
+import Language.Lambda.Untyped
+
+shouldEvalTo :: Text -> Text -> Expectation
+shouldEvalTo s1 = shouldBe (eval s1) . eval
+
+eval :: Text -> Either LambdaException (LambdaExpr Text)
+eval input = execEval (evalText input) (mkEvalState defaultUniques)
diff --git a/test/Language/Lambda/Untyped/ParserSpec.hs b/test/Language/Lambda/Untyped/ParserSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Language/Lambda/Untyped/ParserSpec.hs
@@ -0,0 +1,56 @@
+{-# LANGUAGE NoImplicitPrelude, OverloadedStrings #-}
+module Language.Lambda.Untyped.ParserSpec (spec) where
+
+import Language.Lambda.Untyped.Expression
+import Language.Lambda.Untyped.Parser
+
+import Data.Either
+import Test.Hspec
+import RIO
+
+spec :: Spec
+spec = describe "parseExpr" $ do
+  it "parses simple variables" $
+    parseExpr "x" `shouldBe` Right (Var "x")
+
+  it "parses parenthesized variables" $
+    parseExpr "(x)" `shouldBe` Right (Var "x")
+
+  it "parses simple abstractions" $
+    parseExpr "\\x. x" `shouldBe` Right (Abs "x" (Var "x"))
+
+  it "parses nested abstractions" $
+    parseExpr "\\f a. a" `shouldBe` Right (Abs "f" (Abs "a" (Var "a")))
+
+  it "parses simple applications" $
+    parseExpr "f x" `shouldBe` Right (App (Var "f") (Var "x"))
+
+  it "parses chained applications" $
+    parseExpr "f x y" `shouldBe` Right (App (App (Var "f") (Var "x")) (Var "y"))
+
+  it "parses simple let expressions" $
+    parseExpr "let x = z" `shouldBe` Right (Let "x" (Var "z"))
+
+  it "parses complex expressions" $ do
+    let exprs = [
+          "\\f x. f x",
+          "(\\p x y. y) (\\p x y. x)",
+          "f (\\x. x)",
+          "(\\x . f x) g y",
+          "(\\f . (\\ x y. f x y) f x y) w x y",
+          "let x = \\f x. f x"
+          ]
+    
+    mapM_ (flip shouldSatisfy isRight . parseExpr) exprs
+
+  it "does not parse trailing errors" $
+    parseExpr "x +" `shouldSatisfy` isLeft
+
+  it "ignores whitespace" $ do
+    let exprs = [
+          " x ",
+          " \\ x . x ",
+          " ( x ) "
+          ]
+    
+    mapM_ (flip shouldSatisfy isRight . parseExpr) exprs
diff --git a/test/Language/Lambda/UntypedSpec.hs b/test/Language/Lambda/UntypedSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Language/Lambda/UntypedSpec.hs
@@ -0,0 +1,77 @@
+{-# LANGUAGE NoImplicitPrelude, OverloadedStrings #-}
+module Language.Lambda.UntypedSpec where
+
+import RIO
+import qualified RIO.Map as Map
+import qualified RIO.Text as Text
+import Test.Hspec
+
+import Language.Lambda.Untyped
+import Language.Lambda.Untyped.HspecUtils
+
+spec :: Spec
+spec = do
+  describe "evalText" $ do
+    it "evaluates simple text" $ do
+      eval "x" `shouldBe` Right (Var "x")
+      eval "\\x. x" `shouldBe` Right (Abs "x" (Var "x"))
+      eval "f y" `shouldBe` Right (App (Var "f") (Var "y"))
+
+    it "reduces simple applications" $
+      eval "(\\x .x) y" `shouldBe` Right (Var "y")
+
+    it "reduces applications with nested redexes" $
+      eval "(\\f x. f x) (\\y. y)" `shouldBe` Right (Abs "x" (Var "x"))
+
+  describe "runEvalText" $ do
+    let runEvalText' input = fst <$> runEvalText input Map.empty
+    
+    it "evaluates simple strings" $ do
+      runEvalText' "x" `shouldBe` Right (Var "x")
+      runEvalText' "\\x. x" `shouldBe` Right (Abs "x" (Var "x"))
+      runEvalText' "f y" `shouldBe` Right (App (Var "f") (Var "y"))
+
+    it "reduces simple applications" $
+      runEvalText' "(\\x .x) y" `shouldBe` Right (Var "y")
+
+    it "reduces applications with nested redexes" $
+      runEvalText' "(\\f x. f x) (\\y. y)" `shouldBe` Right (Abs "x" (Var "x"))
+
+  describe "execEvalText" $ do
+    let execEvalText' input = execEvalText input Map.empty
+    
+    it "evaluates simple texts" $ do
+      execEvalText' "x" `shouldBe` Right (Var "x")
+      execEvalText' "\\x. x" `shouldBe` Right (Abs "x" (Var "x"))
+      execEvalText' "f y" `shouldBe` Right (App (Var "f") (Var "y"))
+
+    it "reduces simple applications" $
+      execEvalText' "(\\x .x) y" `shouldBe` Right (Var "y")
+
+    it "reduces applications with nested redexes" $
+      execEvalText' "(\\f x. f x) (\\y. y)" `shouldBe` Right (Abs "x" (Var "x"))
+
+  describe "unsafeExecEvalText" $ do
+    let unsafeExecEvalText' input = unsafeExecEvalText input Map.empty
+    
+    it "evaluates simple texts" $ do
+      unsafeExecEvalText' "x" `shouldBe` Var "x"
+      unsafeExecEvalText' "\\x. x" `shouldBe` Abs "x" (Var "x")
+      unsafeExecEvalText' "f y" `shouldBe` App (Var "f") (Var "y")
+
+    it "reduces simple applications" $
+      unsafeExecEvalText' "(\\x .x) y" `shouldBe` Var "y"
+
+    it "reduces applications with nested redexes" $
+      unsafeExecEvalText' "(\\f x. f x) (\\y. y)" `shouldBe` Abs "x" (Var "x")
+
+  describe "defaultUniques" $ do
+    let alphabet = reverse ['a'..'z']
+        len = length alphabet
+    
+    it "starts with plain alphabet" $
+      take len defaultUniques `shouldBe` map (`Text.cons` Text.empty) alphabet
+
+    it "adds index afterwards" $
+      take len (drop len defaultUniques)
+        `shouldBe` map (`Text.cons` Text.singleton '0') alphabet
diff --git a/test/Language/Lambda/Util/PrettyPrintSpec.hs b/test/Language/Lambda/Util/PrettyPrintSpec.hs
deleted file mode 100644
--- a/test/Language/Lambda/Util/PrettyPrintSpec.hs
+++ /dev/null
@@ -1,36 +0,0 @@
-module Language.Lambda.Util.PrettyPrintSpec where
-
-import Test.Hspec
-
-import Language.Lambda.Util.PrettyPrint
-  
-spec :: Spec
-spec = describe "PDoc" $ do
-  it "pretty prints empty" $
-    prettyPrint' empty `shouldBe` ""
-
-  it "pretty prints added components" $ do
-    let pdoc = add "f" (add "x" empty)
-    prettyPrint' pdoc `shouldBe` "fx"
-
-  it "pretty prints appended components" $ do
-    let pdoc = append ["f", "x", "y"] empty
-    prettyPrint' pdoc `shouldBe` "fxy"
-
-  it "pretty prints between parens" $ do
-    let pdoc = between (PDoc ["f"]) "(" ")" empty
-    prettyPrint' pdoc `shouldBe` "(f)"
-
-    let pdoc' = betweenParens (PDoc ["f"]) empty
-    prettyPrint' pdoc' `shouldBe` "(f)"
-
-  it "pretty prints intercalated spaces" $ do
-    let pdoc = intercalate ["f", "x", "y"] [space] empty
-    prettyPrint' pdoc `shouldBe` "f x y"
-
-  it "pretty prints lambda" $ do
-    let pdoc = between (PDoc ["x"]) "\\" ". " (add "x" empty)
-    prettyPrint' pdoc `shouldBe` "\\x. x"
-
-prettyPrint' :: PDoc String -> String
-prettyPrint' = prettyPrint
diff --git a/test/Language/LambdaSpec.hs b/test/Language/LambdaSpec.hs
deleted file mode 100644
--- a/test/Language/LambdaSpec.hs
+++ /dev/null
@@ -1,30 +0,0 @@
-module Language.LambdaSpec where
-
-import Test.Hspec
-
-import Language.Lambda
-
-spec :: Spec
-spec = do
-  describe "evalString" $ do
-    it "evaluates simple strings" $ do
-      evalString "x" `shouldBe` Right (Var "x")
-      evalString "\\x. x" `shouldBe` Right (Abs "x" (Var "x"))
-      evalString "f y" `shouldBe` Right (App (Var "f") (Var "y"))
-
-    it "reduces simple applications" $
-      evalString "(\\x .x) y" `shouldBe` Right (Var "y")
-
-    it "reduces applications with nested redexes" $
-      evalString "(\\f x. f x) (\\y. y)" `shouldBe` Right (Abs "x" (Var "x"))
-
-  describe "uniques" $ do
-    let alphabet = reverse ['a'..'z']
-        len = length alphabet
-    
-    it "starts with plain alphabet" $
-      take len uniques `shouldBe` map (:[]) alphabet
-
-    it "adds index afterwards" $
-      take len (drop len uniques) `shouldBe` map (:['0']) alphabet
-
diff --git a/test/Language/SystemF/ExpressionSpec.hs b/test/Language/SystemF/ExpressionSpec.hs
deleted file mode 100644
--- a/test/Language/SystemF/ExpressionSpec.hs
+++ /dev/null
@@ -1,81 +0,0 @@
-{-# LANGUAGE FlexibleInstances #-}
-module Language.SystemF.ExpressionSpec where
-
-import Test.Hspec
-
-import Language.Lambda.Util.PrettyPrint
-import Language.SystemF.Expression
-
-spec :: Spec
-spec = describe "prettyPrint" $ do
-  it "prints simple variables" $
-    prettyPrint' (Var "x") `shouldBe` "x"
-
-  it "prints simple applications" $
-    prettyPrint' (App (Var "a") (Var "b")) `shouldBe` "a b"
-
-  it "prints simple abstractions" $ 
-    prettyPrint (Abs "x" (TyVar "T") (Var "x")) `shouldBe` "λ x:T. x"
-
-  it "prints simple type abstractions" $
-    prettyPrint (TyAbs (TyVar "X") (Var "x")) `shouldBe` "Λ X. x"
-
-  it "prints simple type applications" $ 
-    prettyPrint' (TyApp (Var "t") (TyVar "T")) `shouldBe` "t [T]"
-
-  it "prints nested abstractions" $
-    prettyPrint (Abs "f" (TyVar "F") (Abs "x" (TyVar "X") (Var "x")))
-      `shouldBe` "λ f:F x:X. x"
-
-  it "prints abstractions with composite types" $ do
-    prettyPrint (Abs "f" (TyArrow (TyVar "X") (TyVar "Y")) (Var "f"))
-      `shouldBe ` "λ f:(X->Y). f"
-
-    prettyPrint (Abs "f" (TyArrow (TyVar "X") (TyArrow (TyVar "Y") (TyVar "Z"))) (Var "f"))
-      `shouldBe ` "λ f:(X->Y->Z). f"
-
-  it "prints nested type abstractions" $
-    prettyPrint (TyAbs (TyVar "A") (TyAbs (TyVar "B") (Var "x")))
-      `shouldBe` "Λ A B. x"
-
-  it "prints nested applications" $
-    prettyPrint' (App (App (Var "f") (Var "x")) (Var "y"))
-      `shouldBe` "f x y"
-
-  it "prints parenthesized applications" $ do
-    prettyPrint' (App (Var "w") (App (Var "x") (Var "y")))
-      `shouldBe` "w (x y)"
-
-    prettyPrint (App (Abs "t" (TyVar "T") (Var "t")) (Var "x"))
-      `shouldBe` "(λ t:T. t) x"
-
-    prettyPrint (App (Abs "f" (TyVar "F") (Var "f")) (Abs "g" (TyVar "G") (Var "g")))
-      `shouldBe` "(λ f:F. f) (λ g:G. g)"
-
-  it "prints simple types" $
-    prettyPrint (TyVar "X") `shouldBe` "X"
-
-  it "print simple arrow types" $
-    prettyPrint (TyArrow (TyVar "A") (TyVar "B")) `shouldBe` "A -> B"
-
-  it "prints simple forall types" $
-    prettyPrint (TyForAll "X" (TyVar "X")) `shouldBe` "forall X. X"
-
-  it "prints chained arrow types" $
-    prettyPrint (TyArrow (TyVar "X") (TyArrow (TyVar "Y") (TyVar "Z")))
-      `shouldBe` "X -> Y -> Z"
-
-  it "prints nested arrow types" $
-    prettyPrint (TyArrow (TyArrow (TyVar "T") (TyVar "U")) (TyVar "V"))
-      `shouldBe` "(T -> U) -> V"
-
-  it "prints complex forall types" $
-    prettyPrint (TyForAll "A" (TyArrow (TyVar "A") (TyVar "A")))
-      `shouldBe` "forall A. A -> A"
-
-  it "prints nested forall types" $
-    prettyPrint (TyForAll "W" 
-                  (TyForAll "X" 
-                    (TyArrow (TyVar "W") (TyArrow (TyVar "X") (TyVar "Y")))))
-      `shouldBe` "forall W. forall X. W -> X -> Y"
-
diff --git a/test/Language/SystemF/ParserSpec.hs b/test/Language/SystemF/ParserSpec.hs
deleted file mode 100644
--- a/test/Language/SystemF/ParserSpec.hs
+++ /dev/null
@@ -1,84 +0,0 @@
-module Language.SystemF.ParserSpec (spec) where
-
-import Data.Either
-
-import Test.Hspec
-
-import Language.SystemF.Expression
-import Language.SystemF.Parser
-
-spec :: Spec
-spec = do
-  describe "parseExpr" $ do
-    it "parses simple variables" $
-      parseExpr "x" `shouldBe` Right (Var "x")
-
-    it "parses parenthesized variables" $
-      parseExpr "(x)" `shouldBe` Right (Var "x")
-
-    it "parses simple abstractions" $
-      parseExpr "\\x:T. x" `shouldBe` Right (Abs "x" (TyVar "T") (Var "x"))
-
-    it "parses simple type abstractions" $
-      parseExpr "\\X. x" `shouldBe` Right (TyAbs "X" (Var "x"))
-
-    it "parses simple type applications" $ 
-      parseExpr "x [T]" `shouldBe` Right (TyApp (Var "x") (TyVar "T"))
-
-    it "parses nested abstractions" $
-      parseExpr "\\a:A b:B. b" 
-        `shouldBe` Right (Abs "a" (TyVar "A") (Abs "b" (TyVar "B") (Var "b")))
-
-    it "parses abstractions with arrow types" $
-      parseExpr "\\f:(T->U). f"
-        `shouldBe` Right (Abs "f" (TyArrow (TyVar "T") (TyVar "U")) (Var "f"))
-
-    it "parses simple applications" $
-      parseExpr "f x" `shouldBe` Right (App (Var "f") (Var "x"))
-
-    it "parses chained applications" $
-      parseExpr "a b c" `shouldBe` Right (App (App (Var "a") (Var "b")) (Var "c"))
-
-    it "parses complex expressions"  $ do
-      let exprs = [
-            "\\f:(A->B) x:B. f x",
-            "(\\p:(X->Y->Z) x:X y:Y. y) (\\p:(A->B->C) x:B y:C. x)",
-            "f (\\x:T. x)",
-            "(\\ x:X . f x) g y",
-            "(\\f:(X->Y) . (\\ x:X y:Y. f x y) f x y) w x y",
-            "(\\x:T. x) [U]"
-            ]
-
-      mapM_ (flip shouldSatisfy isRight . parseExpr) exprs
-
-    it "does not parse trailing errors" $
-      parseExpr "x +" `shouldSatisfy` isLeft
-
-    it "ignores whitespace" $ do
-      let exprs = [
-            " x ",
-            " \\ x : X. x ",
-            " ( x ) "
-            ]
-
-      mapM_ (flip shouldSatisfy isRight . parseExpr) exprs
-  
-  describe "parseType" $ do
-    it "parses simple variables" $
-      parseType "X" `shouldBe` Right (TyVar "X")
-
-    it "parses parenthesized variables" $
-      parseType "(T)" `shouldBe` Right (TyVar "T")
-
-    it "parses simple arrow types" $
-      parseType "A -> B" `shouldBe` Right (TyArrow (TyVar "A") (TyVar "B")) 
-
-    it "parses parenthesized arrow types" $
-      parseType "((X)->(Y))" `shouldBe` Right (TyArrow (TyVar "X") (TyVar "Y"))
-
-    it "parses nested arrow types" $ do
-      parseType "T -> U -> V" 
-        `shouldBe` Right (TyArrow (TyVar "T") (TyArrow (TyVar "U") (TyVar "V")))
-
-      parseType "(W -> V) -> U"
-        `shouldBe` Right (TyArrow (TyArrow (TyVar "W") (TyVar "V")) (TyVar "U"))
diff --git a/test/Language/SystemF/TypeCheckSpec.hs b/test/Language/SystemF/TypeCheckSpec.hs
deleted file mode 100644
--- a/test/Language/SystemF/TypeCheckSpec.hs
+++ /dev/null
@@ -1,75 +0,0 @@
-module Language.SystemF.TypeCheckSpec (spec) where
-
-import Data.Either
-import Data.Map
-
-import Test.Hspec
-
-import Language.Lambda.Util.PrettyPrint
-import Language.SystemF.Expression
-import Language.SystemF.TypeCheck
-
-tc :: (Ord n, Eq n, PrettyPrint n)
-          => UniqueSupply n 
-          -> [(n, Ty n)]
-          -> SystemFExpr n n 
-          -> Either String (Ty n)
-tc uniqs ctx = typecheck uniqs (fromList ctx)
-
-spec :: Spec
-spec = describe "typecheck" $ do
-  it "typechecks simple variables in context" $
-    tc [] [("x", TyVar "X")] (Var "x") `shouldBe` Right (TyVar "X")
-
-  it "typechecks simple variables not in context" $ 
-    tc ["A"] [] (Var "x") `shouldBe` Right (TyVar "A")
-
-  it "typechecks simple abstractions" $
-    tc [] [] (Abs "x" (TyVar "A") (Var "x")) 
-      `shouldBe` Right (TyArrow (TyVar "A") (TyVar "A"))
-
-  it "typechecks simple applications" $ do
-    let ctx = [
-          ("f", TyArrow (TyVar "T") (TyVar "U")),
-          ("a", TyVar "T")
-          ]
-
-    tc [] ctx (App (Var "f") (Var "a")) `shouldBe` Right (TyVar "U")
-
-  it "apply variable to variable fails" $ do
-    let ctx = [
-          ("a", TyVar "A"),
-          ("b", TyVar "B")
-          ]
-
-    tc ["C"] ctx (App (Var "a") (Var "b")) 
-      `shouldSatisfy` isLeft
-
-  it "apply arrow to variable of wrong type fails" $ do
-    let ctx = [
-          ("f", TyArrow (TyVar "F") (TyVar "G")),
-          ("b", TyVar "B")
-          ]
-
-    tc [] ctx (App (Var "f") (Var "b")) `shouldSatisfy` isLeft
-
-  it "typechecks simple type abstractions" $
-    tc ["A"] [] (TyAbs "X" (Var "x")) `shouldBe` Right (TyForAll "X" (TyVar "A"))
-
-  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 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")
-
-  it "typechecks simple type applications" $
-    tc [] [("x", TyVar "A")] (TyApp (TyAbs "X" (Var "x")) (TyVar "X"))
-      `shouldBe` Right (TyVar "A")
-
-  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"))
diff --git a/test/Language/SystemFSpec.hs b/test/Language/SystemFSpec.hs
deleted file mode 100644
--- a/test/Language/SystemFSpec.hs
+++ /dev/null
@@ -1,9 +0,0 @@
-module Language.SystemFSpec where
-
-import Test.Hspec
-
-import Language.SystemF
-
-spec :: Spec
-spec = describe "evalString" $ 
-  return ()