diff --git a/app/Main.hs b/app/Main.hs
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -2,41 +2,105 @@
 
 import Data.Version
 
+import Options.Applicative hiding (ParseError)
 import System.Console.Shell
 import System.Console.Shell.ShellMonad
 import System.Console.Shell.Backend.Readline (readlineBackend)
 
+import qualified Paths_lambda_calculator as P
+
 import Language.Lambda
-import Paths_lambda_calculator
+import Language.Lambda.Util.PrettyPrint
+import Language.SystemF
 
 main :: IO ()
-main = runShell mkShellDesc readlineBackend ()
+main = execParser opts >>= runShell'
+  where opts = info (helper <*> cliParser)
+                    (briefDesc <> progDesc "A Lambda Calculus Interpreter")
 
-mkShellDesc :: ShellDescription ()
-mkShellDesc = shellDesc' $ mkShellDescription commands eval
+-- 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
+          prompt = shellPrompt language
           }
 
 shellGreeting :: String
 shellGreeting = "Lambda Calculator (" ++ version' ++ ")\nType :h for help\n"
   
-shellPrompt :: s -> IO String
-shellPrompt _ = return "λ > "
+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 -> Sh s ()
-eval = either shellPutErrLn' shellPutStrLn' . evalString
-  where shellPutErrLn' :: Show s => s -> Sh s' ()
-        shellPutErrLn' = shellPutErrLn . show
+commands = [
+  exitCommand "q",
+  helpCommand "h"
+  ]
 
-        shellPutStrLn' :: PrettyPrint s => s -> Sh s' ()
-        shellPutStrLn' = shellPutStrLn . prettyPrint
+eval :: (String -> Result String) -> String -> Sh s' ()
+eval f = either shellPutErrLn shellPutStrLn . f
 
+-- Get the current version
 version' :: String
-version' = showVersion version
+version' = showVersion P.version
  
diff --git a/lambda-calculator.cabal b/lambda-calculator.cabal
--- a/lambda-calculator.cabal
+++ b/lambda-calculator.cabal
@@ -1,5 +1,5 @@
 name:                lambda-calculator
-version:             1.0.0
+version:             1.1.0
 synopsis:            A lambda calculus interpreter
 description:         Please see README.md
 homepage:            https://github.com/sgillespie/lambda-calculus#readme
@@ -19,7 +19,12 @@
                        Language.Lambda.Expression,
                        Language.Lambda.Eval,
                        Language.Lambda.Parser,
-                       Language.Lambda.PrettyPrint
+
+                       Language.Lambda.Util.PrettyPrint,
+
+                       Language.SystemF,
+                       Language.SystemF.Expression,
+                       Language.SystemF.Parser
   build-depends:       base <= 5,
                        parsec
   default-language:    Haskell2010
@@ -31,6 +36,7 @@
   ghc-options:         -threaded -rtsopts -with-rtsopts=-N
   build-depends:       base,
                        lambda-calculator,
+                       optparse-applicative,
                        Shellac,
                        Shellac-readline
   default-language:    Haskell2010
@@ -47,11 +53,25 @@
                        Language.Lambda.EvalSpec,
                        Language.Lambda.HspecUtils,
                        Language.Lambda.ParserSpec,
-                       Language.Lambda.PrettyPrintSpec
+
+                       Language.Lambda.Util.PrettyPrintSpec,
+
+                       Language.SystemFSpec,
+                       Language.SystemF.ExpressionSpec,
+                       Language.SystemF.ParserSpec
   build-depends:       base <= 5,
                        lambda-calculator,
                        hspec,
                        HUnit
+  ghc-options:         -threaded -rtsopts -with-rtsopts=-N
+  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
 
diff --git a/src/Language/Lambda.hs b/src/Language/Lambda.hs
--- a/src/Language/Lambda.hs
+++ b/src/Language/Lambda.hs
@@ -1,5 +1,7 @@
+{-# LANGUAGE FlexibleInstances #-}
 module Language.Lambda (
   LambdaExpr(..),
+  ParseError(..),
   PrettyPrint(..),
   evalExpr,
   evalString,
@@ -13,15 +15,12 @@
 import Language.Lambda.Eval
 import Language.Lambda.Expression
 import Language.Lambda.Parser
-import Language.Lambda.PrettyPrint
+import Language.Lambda.Util.PrettyPrint
 
 evalString :: String -> Either ParseError (LambdaExpr String)
-evalString = liftM (evalExpr uniques) . parseExpr
+evalString = fmap (evalExpr uniques) . parseExpr
 
--- TODO[sgillespie]: Uniques should be [a..z, a0..z0, a1..z1] etc
--- concatMap (\x -> map (\y -> y:x) ['a'..'z']) ([""] ++ map show [0..])
-  
 uniques :: [String]
 uniques = concatMap (\p -> map (:p) . reverse $ ['a'..'z']) suffix
-  where suffix = [""] ++ map show [(0::Int)..]
+  where suffix = "" : map show [(0::Int)..]
 
diff --git a/src/Language/Lambda/Expression.hs b/src/Language/Lambda/Expression.hs
--- a/src/Language/Lambda/Expression.hs
+++ b/src/Language/Lambda/Expression.hs
@@ -3,7 +3,7 @@
 
 import Prelude hiding (abs, uncurry)
 
-import Language.Lambda.PrettyPrint
+import Language.Lambda.Util.PrettyPrint
 
 data LambdaExpr name
   = Var name
@@ -46,6 +46,6 @@
   = pprExpr pdoc e1 `mappend` addSpace (pprExpr pdoc e2)
 
 uncurry :: n -> LambdaExpr n -> ([n], LambdaExpr n)
-uncurry n body = uncurry' [n] body
+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
--- a/src/Language/Lambda/Parser.hs
+++ b/src/Language/Lambda/Parser.hs
@@ -22,7 +22,7 @@
 
 abs :: Parser (LambdaExpr String)
 abs = curry <$> idents <*> expr
-  where idents = (symbol '\\') *> many1 identifier <* (symbol '.')
+  where idents = symbol '\\' *> many1 identifier <* symbol '.'
         curry = flip (foldr Abs)
 
 app :: Parser (LambdaExpr String)
diff --git a/src/Language/Lambda/PrettyPrint.hs b/src/Language/Lambda/PrettyPrint.hs
deleted file mode 100644
--- a/src/Language/Lambda/PrettyPrint.hs
+++ /dev/null
@@ -1,50 +0,0 @@
-{-# LANGUAGE FlexibleInstances #-}
-module Language.Lambda.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) = concat . map 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 = 'λ'
diff --git a/src/Language/Lambda/Util/PrettyPrint.hs b/src/Language/Lambda/Util/PrettyPrint.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Lambda/Util/PrettyPrint.hs
@@ -0,0 +1,53 @@
+{-# 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
new file mode 100644
--- /dev/null
+++ b/src/Language/SystemF.hs
@@ -0,0 +1,16 @@
+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
new file mode 100644
--- /dev/null
+++ b/src/Language/SystemF/Expression.hs
@@ -0,0 +1,136 @@
+{-# LANGUAGE FlexibleInstances #-}
+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)
+  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
+
+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
+
+-- 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
new file mode 100644
--- /dev/null
+++ b/src/Language/SystemF/Parser.hs
@@ -0,0 +1,86 @@
+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/test/HLint.hs b/test/HLint.hs
new file mode 100644
--- /dev/null
+++ b/test/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/test/Language/Lambda/EvalSpec.hs b/test/Language/Lambda/EvalSpec.hs
--- a/test/Language/Lambda/EvalSpec.hs
+++ b/test/Language/Lambda/EvalSpec.hs
@@ -33,7 +33,7 @@
     
     it "reduces simple applications" $ do
       let e1 = Abs "x" (Var "x")
-          e2 = (Var "y")
+          e2 = Var "y"
       betaReduce' e1 e2 `shouldBe` Var "y"
 
     it "reduces nested abstractions" $ do
@@ -97,14 +97,14 @@
       etaConvert expr `shouldBe` expr
 
   describe "freeVarsOf" $ do
-    it "Returns simple vars" $ do
+    it "Returns simple vars" $
       freeVarsOf (Var "x") `shouldBe` ["x"]
   
-    it "Does not return bound vars" $ do
+    it "Does not return bound vars" $
       freeVarsOf (Abs "x" (Var "x")) `shouldBe` []
 
-    it "Returns nested simple vars" $ do
+    it "Returns nested simple vars" $
       freeVarsOf (Abs "x" (Var "y")) `shouldBe` ["y"]
 
-    it "Returns applied simple vars" $ do
+    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
--- a/test/Language/Lambda/Examples/BoolSpec.hs
+++ b/test/Language/Lambda/Examples/BoolSpec.hs
@@ -5,105 +5,104 @@
 import Language.Lambda.HspecUtils
 
 spec :: Spec
-spec = do
-  describe "Bool" $ do
-    -- Bool is the definition of Booleans. We represent bools
-    -- using Church Encodings:
+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
     --
-    -- 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" $ do
-        "(\\x y. x y x) (\\t f. t) (\\t f. t)" `shouldEvalTo` "\\t f. t"
+    -- 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" $ do
-        "(\\x y. x y x) (\\t f. t) (\\t f. f)" `shouldEvalTo` "\\t f. f"
-        
-      it "false and true = false" $ do
-        "(\\x y. x y x) (\\t f. f) (\\t f. t)" `shouldEvalTo` "\\t f. f"
+    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" $ do
-        "(\\x y. x y x) (\\t f. f) (\\t f. f)" `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" $ do
-        "(\\x y. x y x) (\\t f. f) p" `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" $ do
-        "(\\x y. x y x) (\\t f. t) p" `shouldEvalTo` "p"
+    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" $ do
-        "(\\x y. x x y) (\\t f. t) (\\t f. t)" `shouldEvalTo` "\\t f. t"
+  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 "true or false = true" $ do
-        "(\\x y. x x y) (\\t f. t) (\\t f. f)" `shouldEvalTo` "\\t f. t"
-        
-      it "false or true = true" $ do
-        "(\\x y. x x y) (\\t f. f) (\\t f. t)" `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" $ do
-        "(\\x y. x x y) (\\t f. f) (\\t f. f)" `shouldEvalTo` "\\t f. f"
+    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" $ do
-        "(\\x y. x x y) (\\t f. t) p" `shouldEvalTo` "\\t f. t"
+    it "true or p = true" $
+      "(\\x y. x x y) (\\t f. t) p" `shouldEvalTo` "\\t f. t"
 
-      it "false or p = p" $ do
-        "(\\x y. x x y) (\\t f. f) p" `shouldEvalTo` "p"
-        
+    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" $ do
-        "(\\x. x (\\t f. f) (\\t f. t)) \\t f. t" `shouldEvalTo` "\\t f. f"
+  describe "not" $ do
+    -- not takes a Bool and returns its opposite value
+    --
+    -- not(true)  = false
+    -- not(false) = true
+    --
+    -- not is defined by
+    -- not = \x. x (\t f. f) (\t f. t)
+    it "not true = false" $
+      "(\\x. x (\\t f. f) (\\t f. t)) \\t f. t" `shouldEvalTo` "\\t f. f"
 
-      it "not false = true"$ do
-        "(\\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" $ do
-        "(\\p x y. p x y) (\\t f. t) (\\f x. x) (\\f x. f x)"
-          `shouldEvalTo` "\\f x. x"
+    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" $ do
-        "(\\p x y. p x y) (\\t f. f) (\\f x. x) (\\f x. f x)"
-          `shouldEvalTo` "\\f x. f 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" $ do
-        "(\\p x y. p x y) (\\t f. t) p q" `shouldEvalTo` "p"
+    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" $ do
-        "(\\p x y. p x y) (\\t f. f) p q" `shouldEvalTo` "q"
+    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
--- a/test/Language/Lambda/Examples/NatSpec.hs
+++ b/test/Language/Lambda/Examples/NatSpec.hs
@@ -5,99 +5,98 @@
 import Language.Lambda.HspecUtils
 
 spec :: Spec
-spec = do
-  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
+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" $ do
-        "(\\n f x. f (n f x)) (\\f x. x)" `shouldEvalTo` "\\f x. f x"
+  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" $ do
-        "(\\n f x. f (n f x)) (\\f x. f x)" `shouldEvalTo` "\\f x. f (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" $ do
-        "(\\m n f x. m f (n f x)) (\\f x. x) (\\f x. f (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" $ do
-        "(\\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))))"
+    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" $ do
-        "(\\m n f x. m f (n f x)) (\\f x. x) n"
-          `shouldEvalTo` "\\f x. n 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" $ do
-        "(\\m n f. m (n f)) (\\f x. x) (\\f x. f (f x))"
-          `shouldEvalTo` "\\f x. 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" $ do
-        "(\\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 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" $ do
-        "(\\m n f. m (n f)) (\\f x. x) n"
-          `shouldEvalTo` "\\f x. 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" $ do
-        "(\\m n f. m (n f)) (\\f x. f x) n"
-          `shouldEvalTo` "\\f x. n f 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
+  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" $ do
-        "(\\m n f x. (n m) f x) (\\f x. x) (\\f x. f x)"
-          `shouldEvalTo` "\\f x. x"
+    -- 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" $ do
-        "(\\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 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" $ do
-        "(\\m n f x. (n m) f x) n (\\f x. x)"
-          `shouldEvalTo` "\\f x. 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" $ do
-        "(\\m n f x. (n m) f x) n (\\f x. f x)"
-          `shouldEvalTo` "\\f x. n 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
--- a/test/Language/Lambda/Examples/PairSpec.hs
+++ b/test/Language/Lambda/Examples/PairSpec.hs
@@ -5,35 +5,34 @@
 import Test.Hspec
 
 spec :: Spec
-spec = do
-  describe "Pair" $ do
-    -- Pair is the definition of tuples with two items. Pairs,
-    -- again are represented using Church Encodings:
+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
     --
-    -- 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" $ do
-        "(\\p. p (\\t f. t)) ((\\x y f. f x y) (\\f x. x) (\\f x. f x))"
-          `shouldEvalTo` "\\f x. 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" $ do
-        "(\\p. p (\\t f. t)) ((\\x y f. f x y) x y)" `shouldEvalTo` "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" $ do
-        "(\\p. p (\\t f. f)) ((\\x y f. f x y) (\\f x. x) (\\f x. f x))"
-          `shouldEvalTo` "\\f x. f 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"
+    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
--- a/test/Language/Lambda/ExpressionSpec.hs
+++ b/test/Language/Lambda/ExpressionSpec.hs
@@ -3,26 +3,25 @@
 import Test.Hspec
 
 import Language.Lambda.Expression
-import Language.Lambda.PrettyPrint
+import Language.Lambda.Util.PrettyPrint
 
 spec :: Spec
-spec = do
-  describe "prettyPrint" $ do
-    it "prints simple variables" $ do
+spec = describe "prettyPrint" $ do
+    it "prints simple variables" $ 
       prettyPrint (Var "x") `shouldBe` "x"
 
-    it "prints simple abstractions" $ do
+    it "prints simple abstractions" $
       prettyPrint (Abs "x" (Var "x")) `shouldBe` "λx. x"
 
-    it "prints simple applications" $ do
+    it "prints simple applications" $
       prettyPrint (App (Var "a") (Var "b"))
         `shouldBe` "a b"
 
-    it "prints nested applications" $ do
-      prettyPrint (Abs "f" (Abs "x" (Var"x")))
+    it "prints nested abstractions" $
+      prettyPrint (Abs "f" (Abs "x" (Var "x")))
         `shouldBe` "λf x. x"
 
-    it "prints nested applications" $ do
+    it "prints nested applications" $
       prettyPrint (App (App (Var "f") (Var "x")) (Var "y"))
         `shouldBe` "f x y"
 
diff --git a/test/Language/Lambda/HspecUtils.hs b/test/Language/Lambda/HspecUtils.hs
--- a/test/Language/Lambda/HspecUtils.hs
+++ b/test/Language/Lambda/HspecUtils.hs
@@ -5,4 +5,7 @@
 import Language.Lambda
 
 shouldEvalTo :: String -> String -> Expectation
-shouldEvalTo s1 = shouldBe (evalString s1) . evalString
+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
--- a/test/Language/Lambda/ParserSpec.hs
+++ b/test/Language/Lambda/ParserSpec.hs
@@ -8,47 +8,46 @@
 import Language.Lambda.Parser
 
 spec :: Spec
-spec = do
-  describe "parseExpr" $ do
-    it "parses simple variables" $ do
-      parseExpr "x" `shouldBe` Right (Var "x")
+spec = describe "parseExpr" $ do
+  it "parses simple variables" $
+    parseExpr "x" `shouldBe` Right (Var "x")
 
-    it "parses parenthesized variables" $ do
-      parseExpr "(x)" `shouldBe` Right (Var "x")
+  it "parses parenthesized variables" $
+    parseExpr "(x)" `shouldBe` Right (Var "x")
 
-    it "parses simple abstractions" $ do
-      parseExpr "\\x. x" `shouldBe` Right (Abs "x" (Var "x"))
+  it "parses simple abstractions" $
+    parseExpr "\\x. x" `shouldBe` Right (Abs "x" (Var "x"))
 
-    it "parses nested abstractions" $ do
-      parseExpr "\\f a. a" `shouldBe` Right (Abs "f" (Abs "a" (Var "a")))
+  it "parses nested abstractions" $
+    parseExpr "\\f a. a" `shouldBe` Right (Abs "f" (Abs "a" (Var "a")))
 
-    it "parses simple applications" $ do
-      parseExpr "f x" `shouldBe` Right (App (Var "f") (Var "x"))
+  it "parses simple applications" $
+    parseExpr "f x" `shouldBe` Right (App (Var "f") (Var "x"))
 
-    it "parses chained applications" $ do
-      parseExpr "f x y" `shouldBe` Right (App (App (Var "f") (Var "x")) (Var "y"))
+  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 "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" $ do
-      parseExpr "x +" `shouldSatisfy` isLeft
-  
-    it "ignores whitespace" $ do
-      let exprs = [
-            " x ",
-            " \\ x . x ",
-            " ( 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/PrettyPrintSpec.hs b/test/Language/Lambda/PrettyPrintSpec.hs
deleted file mode 100644
--- a/test/Language/Lambda/PrettyPrintSpec.hs
+++ /dev/null
@@ -1,37 +0,0 @@
-module Language.Lambda.PrettyPrintSpec where
-
-import Test.Hspec
-
-import Language.Lambda.PrettyPrint
-  
-spec :: Spec
-spec = do
-  describe "PDoc" $ do
-    it "pretty prints empty" $ do
-      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/Lambda/Util/PrettyPrintSpec.hs b/test/Language/Lambda/Util/PrettyPrintSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Language/Lambda/Util/PrettyPrintSpec.hs
@@ -0,0 +1,36 @@
+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
--- a/test/Language/LambdaSpec.hs
+++ b/test/Language/LambdaSpec.hs
@@ -12,19 +12,19 @@
       evalString "\\x. x" `shouldBe` Right (Abs "x" (Var "x"))
       evalString "f y" `shouldBe` Right (App (Var "f") (Var "y"))
 
-    it "reduces simple applications" $ do
+    it "reduces simple applications" $
       evalString "(\\x .x) y" `shouldBe` Right (Var "y")
 
-    it "reduces applications with nested redexes" $ do
+    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" $ do
+    it "starts with plain alphabet" $
       take len uniques `shouldBe` map (:[]) alphabet
 
-    it "adds index afterwards" $ do
+    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
new file mode 100644
--- /dev/null
+++ b/test/Language/SystemF/ExpressionSpec.hs
@@ -0,0 +1,67 @@
+{-# 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 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"
diff --git a/test/Language/SystemF/ParserSpec.hs b/test/Language/SystemF/ParserSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Language/SystemF/ParserSpec.hs
@@ -0,0 +1,84 @@
+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/SystemFSpec.hs b/test/Language/SystemFSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Language/SystemFSpec.hs
@@ -0,0 +1,9 @@
+module Language.SystemFSpec where
+
+import Test.Hspec
+
+import Language.SystemF
+
+spec :: Spec
+spec = describe "evalString" $ 
+  return ()