diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,20 @@
+The MIT License (MIT)
+
+Copyright (c) 2016 Sean D Gillespie
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of
+this software and associated documentation files (the "Software"), to deal in
+the Software without restriction, including without limitation the rights to
+use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
+of the Software, and to permit persons to whom the Software is furnished to do
+so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
+IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/app/Main.hs b/app/Main.hs
new file mode 100644
--- /dev/null
+++ b/app/Main.hs
@@ -0,0 +1,42 @@
+module Main where
+
+import Data.Version
+
+import System.Console.Shell
+import System.Console.Shell.ShellMonad
+import System.Console.Shell.Backend.Readline (readlineBackend)
+
+import Language.Lambda
+import Paths_lambda_calculator
+
+main :: IO ()
+main = runShell mkShellDesc readlineBackend ()
+
+mkShellDesc :: ShellDescription ()
+mkShellDesc = shellDesc' $ mkShellDescription commands eval
+  where shellDesc' d = d {
+          greetingText = Just shellGreeting,
+          prompt = shellPrompt
+          }
+
+shellGreeting :: String
+shellGreeting = "Lambda Calculator (" ++ version' ++ ")\nType :h for help\n"
+  
+shellPrompt :: s -> IO String
+shellPrompt _ = return "λ > "
+
+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
+
+        shellPutStrLn' :: PrettyPrint s => s -> Sh s' ()
+        shellPutStrLn' = shellPutStrLn . prettyPrint
+
+version' :: String
+version' = showVersion version
+ 
diff --git a/lambda-calculator.cabal b/lambda-calculator.cabal
new file mode 100644
--- /dev/null
+++ b/lambda-calculator.cabal
@@ -0,0 +1,60 @@
+name:                lambda-calculator
+version:             0.5.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.PrettyPrint
+  build-depends:       base <= 5,
+                       parsec
+  default-language:    Haskell2010
+
+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,
+                       lambda-calculator,
+                       Shellac,
+                       Shellac-readline
+  default-language:    Haskell2010
+
+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,
+                       Language.Lambda.PrettyPrintSpec
+  build-depends:       base <= 5,
+                       lambda-calculator,
+                       hspec,
+                       HUnit
+  ghc-options:         -threaded -rtsopts -with-rtsopts=-N
+  default-language:    Haskell2010
+
+source-repository head
+  type:     git
+  location: https://github.com/sgillespie/lambda-calculus
diff --git a/src/Language/Lambda.hs b/src/Language/Lambda.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Lambda.hs
@@ -0,0 +1,27 @@
+module Language.Lambda (
+  LambdaExpr(..),
+  PrettyPrint(..),
+  evalExpr,
+  evalString,
+  parseExpr,
+  uniques,
+  ) where
+
+import Control.Monad
+import Text.Parsec
+
+import Language.Lambda.Eval
+import Language.Lambda.Expression
+import Language.Lambda.Parser
+import Language.Lambda.PrettyPrint
+
+evalString :: String -> Either ParseError (LambdaExpr String)
+evalString = liftM (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)..]
+
diff --git a/src/Language/Lambda/Eval.hs b/src/Language/Lambda/Eval.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Lambda/Eval.hs
@@ -0,0 +1,43 @@
+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
+
+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
new file mode 100644
--- /dev/null
+++ b/src/Language/Lambda/Expression.hs
@@ -0,0 +1,51 @@
+{-# LANGUAGE FlexibleInstances #-}
+module Language.Lambda.Expression where
+
+import Prelude hiding (abs, uncurry)
+
+import Language.Lambda.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 body = uncurry' [n] body
+  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
new file mode 100644
--- /dev/null
+++ b/src/Language/Lambda/Parser.hs
@@ -0,0 +1,46 @@
+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/PrettyPrint.hs b/src/Language/Lambda/PrettyPrint.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Lambda/PrettyPrint.hs
@@ -0,0 +1,50 @@
+{-# 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/test/Language/Lambda/EvalSpec.hs b/test/Language/Lambda/EvalSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Language/Lambda/EvalSpec.hs
@@ -0,0 +1,88 @@
+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 "freeVarsOf" $ do
+    it "Returns simple vars" $ do
+      freeVarsOf (Var "x") `shouldBe` ["x"]
+  
+    it "Does not return bound vars" $ do
+      freeVarsOf (Abs "x" (Var "x")) `shouldBe` []
+
+    it "Returns nested simple vars" $ do
+      freeVarsOf (Abs "x" (Var "y")) `shouldBe` ["y"]
+
+    it "Returns applied simple vars" $ do
+      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
new file mode 100644
--- /dev/null
+++ b/test/Language/Lambda/Examples/BoolSpec.hs
@@ -0,0 +1,109 @@
+module Language.Lambda.Examples.BoolSpec where
+
+import Test.Hspec
+
+import Language.Lambda.HspecUtils
+
+spec :: Spec
+spec = do
+  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" $ do
+        "(\\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 "false and false = false" $ do
+        "(\\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 "true and p = false" $ do
+        "(\\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"
+      
+      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 false = false" $ do
+        "(\\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 "false or p = p" $ do
+        "(\\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"
+
+      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 "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 "it true p q = p" $ do
+        "(\\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"
diff --git a/test/Language/Lambda/Examples/NatSpec.hs b/test/Language/Lambda/Examples/NatSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Language/Lambda/Examples/NatSpec.hs
@@ -0,0 +1,103 @@
+module Language.Lambda.Examples.NatSpec where
+
+import Test.Hspec
+
+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
+
+    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"
+
+      it "succ 1 = 2" $ do
+        "(\\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)"
+
+      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))))"
+
+      -- 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"
+
+    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"
+
+      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 0 n = 0" $ do
+        "(\\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"
+
+    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"
+
+      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 n 0 = 1" $ do
+        "(\\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"
diff --git a/test/Language/Lambda/Examples/PairSpec.hs b/test/Language/Lambda/Examples/PairSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Language/Lambda/Examples/PairSpec.hs
@@ -0,0 +1,39 @@
+module Language.Lambda.Examples.PairSpec where
+
+import Language.Lambda.HspecUtils
+
+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:
+    --
+    -- 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"
+
+      it "first x y = x" $ do
+        "(\\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"
+
+      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
new file mode 100644
--- /dev/null
+++ b/test/Language/Lambda/ExpressionSpec.hs
@@ -0,0 +1,40 @@
+module Language.Lambda.ExpressionSpec where
+
+import Test.Hspec
+
+import Language.Lambda.Expression
+import Language.Lambda.PrettyPrint
+
+spec :: Spec
+spec = do
+  describe "prettyPrint" $ do
+    it "prints simple variables" $ do
+      prettyPrint (Var "x") `shouldBe` "x"
+
+    it "prints simple abstractions" $ do
+      prettyPrint (Abs "x" (Var "x")) `shouldBe` "λx. x"
+
+    it "prints simple applications" $ do
+      prettyPrint (App (Var "a") (Var "b"))
+        `shouldBe` "a b"
+
+    it "prints nested applications" $ do
+      prettyPrint (Abs "f" (Abs "x" (Var"x")))
+        `shouldBe` "λf x. x"
+
+    it "prints nested applications" $ do
+      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
new file mode 100644
--- /dev/null
+++ b/test/Language/Lambda/HspecUtils.hs
@@ -0,0 +1,8 @@
+module Language.Lambda.HspecUtils where
+
+import Test.Hspec
+
+import Language.Lambda
+
+shouldEvalTo :: String -> String -> Expectation
+shouldEvalTo s1 = shouldBe (evalString s1) . evalString
diff --git a/test/Language/Lambda/ParserSpec.hs b/test/Language/Lambda/ParserSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Language/Lambda/ParserSpec.hs
@@ -0,0 +1,54 @@
+module Language.Lambda.ParserSpec (spec) where
+
+import Data.Either
+
+import Test.Hspec
+
+import Language.Lambda.Expression
+import Language.Lambda.Parser
+
+spec :: Spec
+spec = do
+  describe "parseExpr" $ do
+    it "parses simple variables" $ do
+      parseExpr "x" `shouldBe` Right (Var "x")
+
+    it "parses parenthesized variables" $ do
+      parseExpr "(x)" `shouldBe` Right (Var "x")
+
+    it "parses simple abstractions" $ do
+      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 simple applications" $ do
+      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 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
+            
+
diff --git a/test/Language/Lambda/PrettyPrintSpec.hs b/test/Language/Lambda/PrettyPrintSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Language/Lambda/PrettyPrintSpec.hs
@@ -0,0 +1,37 @@
+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/LambdaSpec.hs b/test/Language/LambdaSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Language/LambdaSpec.hs
@@ -0,0 +1,30 @@
+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" $ do
+      evalString "(\\x .x) y" `shouldBe` Right (Var "y")
+
+    it "reduces applications with nested redexes" $ do
+      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
+      take len uniques `shouldBe` map (:[]) alphabet
+
+    it "adds index afterwards" $ do
+      take len (drop len uniques) `shouldBe` map (:['0']) alphabet
+
diff --git a/test/Spec.hs b/test/Spec.hs
new file mode 100644
--- /dev/null
+++ b/test/Spec.hs
@@ -0,0 +1,1 @@
+{-# OPTIONS_GHC -F -pgmF hspec-discover #-}