diff --git a/elsa.cabal b/elsa.cabal
--- a/elsa.cabal
+++ b/elsa.cabal
@@ -1,5 +1,5 @@
 name:                elsa
-version:             0.2.0.0
+version:             0.2.0.1
 synopsis:            A tiny language for understanding the lambda-calculus
 description:         elsa is a small proof checker for verifying sequences of
                      reductions of lambda-calculus terms. The goal is to help
diff --git a/src/Language/Elsa/Eval.hs b/src/Language/Elsa/Eval.hs
--- a/src/Language/Elsa/Eval.hs
+++ b/src/Language/Elsa/Eval.hs
@@ -171,18 +171,20 @@
 beta _                    _   = Nothing
 
 substCA :: Expr a -> Id -> Expr a -> Maybe (Expr a)
-substCA e x e' = go [] e
+substCA e x e'           = go [] e
   where
     zs                   = freeVars e'
-    bnd bs zs            = or [ b `isIn` zs | b <- bs ]
+    bnd  bs zs           = or [ b `isIn` zs | b <- bs ]
     go bs e@(EVar y _)
       | y /= x           = Just e            -- different var, no subst
-      | bnd bs zs        = Nothing           -- same var, but free-var-captured
+      | bnd  bs zs       = Nothing           -- same var, but free-var-captured
       | otherwise        = Just e'           -- same var, but no capture
     go bs (EApp e1 e2 l) = do e1' <- go bs e1
                               e2' <- go bs e2
                               Just (EApp e1' e2' l)
-    go bs (ELam b e1  l) = do e1' <- go (b:bs) e1
+    go bs e@(ELam b e1  l)
+      | x == bindId b    = Just e            -- subst-var has been rebound
+      | otherwise        = do e1' <- go (b:bs) e1
                               Just (ELam b e1' l)
 
 isIn :: Bind a -> S.HashSet Id -> Bool
diff --git a/src/Language/Elsa/Runner.hs b/src/Language/Elsa/Runner.hs
--- a/src/Language/Elsa/Runner.hs
+++ b/src/Language/Elsa/Runner.hs
@@ -15,6 +15,7 @@
 import System.Environment   (getArgs)
 import System.FilePath
 import System.Directory
+import System.Timeout
 import Language.Elsa.Parser
 import Language.Elsa.Types
 import Language.Elsa.UX
@@ -24,8 +25,26 @@
 topMain = do
   (m, f) <- getSrcFile
   s      <- readFile f
-  runElsa m f s `catch` exitErrors m f
+  res    <- timeout (timeLimit * 10 ^ 6) (runElsa m f s `catch` exitErrors m f)
+  case res of
+    Just z  -> return z
+    Nothing -> putStrLn timeMsg >> exitFailure
 
+timeLimit :: Int
+timeLimit = 10
+
+timeMsg :: String
+timeMsg = "Timed out after " ++ show timeLimit ++ " seconds."
+
+getSrcFile :: IO (Mode, Text)
+getSrcFile = do
+  args <- getArgs
+  case args of
+    ["--json"  , f] -> return (Json,    f)
+    ["--server", f] -> return (Server,  f)
+    [f]             -> return (Cmdline, f)
+    _               -> error "Please run with a single file as input"
+
 exitErrors :: Mode -> FilePath -> [UserError] -> IO ()
 exitErrors mode f es = esHandle mode (modeWriter mode f) resultExit es
 
@@ -46,7 +65,9 @@
                             jsonDir  = takeDirectory f </> ".elsa"
                             jsonFile = jsonDir </> addExtension (takeFileName f) ".json"
 
+---------------------------------------------------------------------------------------------------------
 runElsa :: Mode -> FilePath -> Text -> IO ()
+---------------------------------------------------------------------------------------------------------
 runElsa mode f s = do
   let rs = elsa (parse f s)
   let es = mapMaybe resultError rs
@@ -54,16 +75,6 @@
   exitErrors mode f es
 
 okMessage rs = "OK " ++ intercalate ", " (successes rs) ++ "."
-
-getSrcFile :: IO (Mode, Text)
-getSrcFile = do
-  args <- getArgs
-  case args of
-    ["--json"  , f] -> return (Json,    f)
-    ["--server", f] -> return (Server,  f)
-    [f]             -> return (Cmdline, f)
-    _               -> error "Please run with a single file as input"
-
 
 --------------------------------------------------------------------------------
 runElsaId :: FilePath -> Id -> IO (Maybe (Result ()))
diff --git a/src/Language/Elsa/Utils.hs b/src/Language/Elsa/Utils.hs
--- a/src/Language/Elsa/Utils.hs
+++ b/src/Language/Elsa/Utils.hs
@@ -40,7 +40,7 @@
 traceShow msg x
   | False
   = trace (printf "TRACE: %s = %s" msg (show x)) x
-  | otherwise 
+  | otherwise
   = x
 
 safeHead :: a -> [a] -> a