diff --git a/CHANGES.md b/CHANGES.md
new file mode 100644
--- /dev/null
+++ b/CHANGES.md
@@ -0,0 +1,7 @@
+# Changes
+
+0.2.2.0
+
+- Faster (and correct!) implementation of Normalization by Mark Barbone (@mb64)
+- Better parse error messages by Justin Yao Du (@justinyaodo)
+- Updated to work with GHC 8.10.7 by Rose Kunkel (@rosekunkel)
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -11,7 +11,7 @@
 
 ## Online Demo
 
-You can try `elsa` online at [this link](http://goto.ucsd.edu:8095/index.html)
+You can try `elsa` online at [this link](http://goto.ucsd.edu/elsa/index.html)
 
 ## Install
 
@@ -29,7 +29,11 @@
 $ cd elsa
 $ stack install
 ```
+## Editor Plugins
 
+- [VSCode](https://github.com/mistzzt/vscode-elsa-lang)
+- [Vim](https://github.com/glapa-grossklag/elsa.vim)
+
 ## Overview
 
 `elsa` programs look like:
@@ -188,6 +192,48 @@
 * `t =*> t'` is valid if `t` and `t'` are in the reflexive, transitive closure
              of the union of the above three relations.
 * `t =~> t'` is valid if `t` [normalizes to][normalform] `t'`.
+
+
+(Due to Michael Borkowski)
+
+The difference between `=*>` and `=~>` is as follows.
+
+* `t =*> t'` is _any_ sequence of zero or more steps from `t` to `t'`. 
+  So if you are working forwards from the start, backwards from the end, 
+  or a combination of both, you could use `=*>` as a quick check to see 
+  if you're on the right track. 
+
+* `t =~> t'` says that `t` reduces to `t'` in zero or more steps **and** 
+   that `t'` is in **normal form** (i.e. `t'` cannot be reduced further). 
+   This means you can only place it as the *final step*. 
+
+So `elsa` would accept these three
+
+```
+eval ex1:
+  (\x y -> x y) (\x -> x) b 
+  =*> b
+
+eval ex2:
+  (\x y -> x y) (\x -> x) b 
+  =~> b
+
+eval ex3:
+  (\x y -> x y) (\x -> x) (\z -> z) 
+  =*> (\x -> x) (\z -> z) 
+  =b> (\z -> z)
+```
+
+but `elsa` would *not* accept 
+
+```
+eval ex3:
+  (\x y -> x y) (\x -> x) (\z -> z) 
+  =~> (\x -> x) (\z -> z) 
+  =b> (\z -> z)
+```
+
+because the right hand side of `=~>` can still be reduced further.
 
 [normalform]: http://dl.acm.org/citation.cfm?id=860276
 [normalform-pdf]: http://www.cs.cornell.edu/courses/cs6110/2014sp/Handouts/Sestoft.pdf
diff --git a/elsa.cabal b/elsa.cabal
--- a/elsa.cabal
+++ b/elsa.cabal
@@ -1,5 +1,5 @@
 name:                elsa
-version:             0.2.1.2
+version:             0.2.2.0
 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
@@ -13,7 +13,7 @@
 category:            Language
 Homepage:            http://github.com/ucsd-progsys/elsa
 build-type:          Simple
-extra-source-files:  README.md
+extra-source-files:  README.md, CHANGES.md
 cabal-version:       >=1.10
 
 Source-Repository head
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
@@ -1,14 +1,15 @@
-{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE OverloadedStrings, BangPatterns #-}
 
 module Language.Elsa.Eval (elsa, elsaOn) where
 
 import qualified Data.HashMap.Strict  as M
+import qualified Data.HashMap.Lazy    as ML
 import qualified Data.HashSet         as S
 import qualified Data.List            as L
 import           Control.Monad.State
 import qualified Data.Maybe           as Mb -- (isJust, maybeToList)
 import           Language.Elsa.Types
-import           Language.Elsa.Utils  (traceShow, qPushes, qInit, qPop, fromEither)
+import           Language.Elsa.Utils  (qPushes, qInit, qPop, fromEither)
 
 --------------------------------------------------------------------------------
 elsa :: Elsa a -> [Result a]
@@ -21,11 +22,23 @@
 elsaOn cond p =
   case mkEnv (defns p) of
     Left err -> [err]
-    Right g  -> [result g e | e <- evals p, check e ]
+    Right g  -> case checkDupEval (evals p) of
+      Left err -> [err]
+      Right _  -> [result g e | e <- evals p, check e ]
   where
     check = cond . bindId . evName
 
+checkDupEval :: [Eval a] -> CheckM a (S.HashSet Id)
+checkDupEval = foldM addEvalId S.empty
 
+addEvalId :: S.HashSet Id -> Eval a -> CheckM a (S.HashSet Id)
+addEvalId s e = 
+  if S.member (bindId b) s
+    then Left  (errDupEval b)
+    else Right (S.insert (bindId b) s)
+  where
+    b = evName e
+
 result :: Env a -> Eval a -> Result a
 result g e = fromEither (eval g e)
 
@@ -33,10 +46,14 @@
 mkEnv = foldM expand M.empty
 
 expand :: Env a -> Defn a -> CheckM a (Env a)
-expand g (Defn b e) = case zs of
-                        (x,l) : _ -> Left  (Unbound b x l)
-                        []        -> Right (M.insert (bindId b) e' g)
+expand g (Defn b e) = 
+  if dupId 
+    then Left (errDupDefn b)
+    else case zs of
+      (x,l) : _ -> Left  (Unbound b x l)
+      []        -> Right (M.insert (bindId b) e' g)
   where
+    dupId           = M.member (bindId b) g
     e'              = subst e g
     zs              = M.toList (freeVars' e')
 
@@ -192,34 +209,27 @@
 
 --------------------------------------------------------------------------------
 -- | Evaluation to Normal Form
---   http://www.cs.cornell.edu/courses/cs6110/2014sp/Handouts/Sestoft.pdf
 --------------------------------------------------------------------------------
 isNormEq :: Env a -> Expr a -> Expr a -> Bool
-isNormEq g e1 e2 = isEquiv g e1' e2
+isNormEq g e1 e2 = eqVal (subst e2 g) $ evalNbE ML.empty (subst e1 g)
   where
-    e1'          = traceShow ("evalNO" ++ show e1) $ evalNO (traceShow "CANON" $ canon g e1)
-
--- | normal-order reduction
-evalNO :: Expr a -> Expr a
-evalNO e@(EVar {})    = e
-evalNO (ELam b e l)   = ELam b (evalNO e) l
-evalNO (EApp e1 e2 l) = case evalCBN e1 of
-                          ELam b e1' _ -> evalNO (bSubst e1' (bindId b) e2)
-                          e1'          -> EApp (evalNO e1') (evalNO e2) l
+    evalNbE !env e = case e of
+      EVar x _            -> Mb.fromMaybe (Neutral x []) $ ML.lookup x env
+      ELam (Bind x _) b _ -> Fun $ \val -> evalNbE (ML.insert x val env) b
+      EApp f arg _        -> case evalNbE env f of
+        Fun f' -> f' (evalNbE env arg)
+        Neutral x args -> Neutral x (evalNbE env arg:args)
 
--- | call-by-name reduction
-evalCBN :: Expr a -> Expr a
-evalCBN e@(EVar {}) = e
-evalCBN e@(ELam {}) = e
-evalCBN (EApp e1 e2 l) = case evalCBN e1 of
-                          ELam b e1' _ -> evalCBN (bSubst e1' (bindId b) e2)
-                          e1'          -> EApp e1' e2 l
+    eqVal (EVar x _) (Neutral x' [])
+      = x == x'
+    eqVal (ELam (Bind x _) b _) (Fun f)
+      = eqVal b (f (Neutral x []))
+    eqVal (EApp f a _) (Neutral x (a':args))
+      = eqVal a a' && eqVal f (Neutral x args)
+    eqVal _ _ = False
 
--- | Force alpha-renaming to ensure capture avoiding subst
-bSubst :: Expr a -> Id -> Expr a -> Expr a
-bSubst e x e' = subst e (M.singleton x e'')
-  where
-    e''       = e' -- alphaShift n e'
+-- | NbE semantic domain
+data Value = Fun !(Value -> Value) | Neutral !Id ![Value]
 
 --------------------------------------------------------------------------------
 -- | General Helpers
@@ -253,3 +263,9 @@
 
 errPartial :: Bind a -> Expr a -> Result a
 errPartial b e = Partial b (tag e)
+
+errDupDefn :: Bind a -> Result a
+errDupDefn b = DupDefn b (tag b)
+
+errDupEval :: Bind a -> Result a
+errDupEval b = DupEval b (tag b)
diff --git a/src/Language/Elsa/Parser.hs b/src/Language/Elsa/Parser.hs
--- a/src/Language/Elsa/Parser.hs
+++ b/src/Language/Elsa/Parser.hs
@@ -25,14 +25,20 @@
 
 parseWith  :: Parser a -> FilePath -> Text -> a
 parseWith p f s = case runParser (whole p) f s of
-                    Left pErrs -> Ex.throw (mkErrors pErrs) -- panic (show err) (posSpan . NE.head . errorPos $ err)
+                    Left pErrs -> Ex.throw (mkErrors pErrs f s) -- panic (show err) (posSpan . NE.head . errorPos $ err)
                     Right e  -> e
 
+mkErrors :: ParseErrorBundle Text SourcePos -> FilePath -> Text -> [UserError]
+mkErrors b f s = [ mkError (parseErrorPretty e) (span e) | e <- NE.toList (bundleErrors b)]
+  where
+    span e = let (l, c) = lineCol s (errorOffset e) in posSpan (SourcePos f (mkPos l) (mkPos c))
 
-mkErrors :: ParseErrorBundle Text SourcePos -> [UserError]
-mkErrors b = [ mkError (parseErrorPretty e) (sp b) | e <- NE.toList (bundleErrors b)]
-  where 
-    sp     = posSpan . pstateSourcePos . bundlePosState
+-- PosState looks relevant for finding line/column, but I (Justin) don't know how to use it
+
+lineCol :: String -> Int -> (Int, Int)
+lineCol s i = foldl f (1, 1) (Prelude.take i s)
+  where
+    f (l, c) char = if char == '\n' then (l + 1, 1) else (l, c + 1)
 
 instance ShowErrorComponent SourcePos where
   showErrorComponent = show
diff --git a/src/Language/Elsa/Types.hs b/src/Language/Elsa/Types.hs
--- a/src/Language/Elsa/Types.hs
+++ b/src/Language/Elsa/Types.hs
@@ -30,6 +30,8 @@
   | Partial (Bind a)    a
   | Invalid (Bind a)    a
   | Unbound (Bind a) Id a
+  | DupDefn (Bind a)    a
+  | DupEval (Bind a)    a
   deriving (Eq, Show, Functor)
 
 failures :: [Result a] -> [Id]
@@ -38,6 +40,8 @@
     go (Partial b _)   = Just (bindId b)
     go (Invalid b _)   = Just (bindId b)
     go (Unbound b _ _) = Just (bindId b)
+    go (DupDefn b _)   = Just (bindId b)
+    go (DupEval b _)   = Just (bindId b)
     go _               = Nothing
 
 successes :: [Result a] -> [Id]
@@ -50,6 +54,8 @@
 resultError (Partial b l)   = mkErr l (bindId b ++ " can be further reduced!")
 resultError (Invalid b l)   = mkErr l (bindId b ++ " has an invalid reduction!")
 resultError (Unbound b x l) = mkErr l (bindId b ++ " has an unbound variable " ++ x )
+resultError (DupDefn b l)   = mkErr l ("Definition " ++ (bindId b) ++ " has already been declared")
+resultError (DupEval b l)   = mkErr l ("Evaluation " ++ (bindId b) ++ " has already been declared")
 resultError _               = Nothing
 
 mkErr :: (Located a) => a -> Text -> Maybe UserError
diff --git a/tests/Test.hs b/tests/Test.hs
--- a/tests/Test.hs
+++ b/tests/Test.hs
@@ -22,6 +22,8 @@
   [ testGroup "ok"      <$> dirTests "tests/ok"       TestOk
   , testGroup "further" <$> dirTests "tests/further"  TestPartial
   , testGroup "invalid" <$> dirTests "tests/invalid"  TestInvalid
+  , testGroup "dupdefn" <$> dirTests "tests/dupdefn"  TestDupDefn
+  , testGroup "dupeval" <$> dirTests "tests/dupeval"  TestDupEval
   ]
 
 data Outcome
@@ -29,6 +31,8 @@
   | TestPartial
   | TestInvalid
   | TestMixed
+  | TestDupDefn
+  | TestDupEval
   deriving (Eq, Ord, Show)
 
 --------------------------------------------------------------------------------
@@ -54,15 +58,19 @@
 doTest f =  resultOutcome . elsa <$> parseFile f
 
 resultOutcome :: [Result a] -> Outcome
-resultOutcome rs = case (oks, invs, parts) of
-                     (True, False, False) -> TestOk
-                     (False, True, False) -> TestInvalid
-                     (False, False, True) -> TestPartial
+resultOutcome rs = case (oks, invs, parts, ddefn, deval) of
+                     (True, False, False, False, False) -> TestOk
+                     (False, True, False, False, False) -> TestInvalid
+                     (False, False, True, False, False) -> TestPartial
+                     (False, False, False, True, False) -> TestDupDefn
+                     (False, False, False, False, True) -> TestDupEval
                      _                    -> TestMixed
   where
     oks          = notNull [ r | r@(OK {})      <- rs ]
     invs         = notNull [ r | r@(Invalid {}) <- rs ]
     parts        = notNull [ r | r@(Partial {}) <- rs ]
+    ddefn        = notNull [ r | r@(DupDefn {}) <- rs ]
+    deval        = notNull [ r | r@(DupEval {}) <- rs ]
     notNull      = not . null
 
 ----------------------------------------------------------------------------------------