diff --git a/CHANGES.md b/CHANGES.md
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,5 +1,17 @@
 # Changes
 
+0.3.0.0 
+
+- bump to GHC 9.8.4 by @ilanashapiro
+
+- new evaluation steps and strategies by @JRB-Prod-UVA
+    - A new operator =e> for the eta reduction has been added.
+    - Definitions introduced with let and the evaluation or confirmation statements can now be used interchangeably. So after an evaluation or confirmation block a new let binding can be introduced.
+    - Reduction and equivalence checking sequence that do not have to end in a strong normal form are now also supported, by replacing the keyword `eval` with `conf`
+    - Different normal form checks on arbitrary reduction and equivalence proof checking results are now supported.
+    - Support for two specific reduction strategies: normal order and applicative order were added. For this, we introduced two new operators (`=n>` and `=p>`).
+
+
 0.2.2.0
 
 - Faster (and correct!) implementation of Normalization by Mark Barbone (@mb64)
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -11,8 +11,9 @@
 
 ## Online Demo
 
-You can try `elsa` online at [this link](http://goto.ucsd.edu/elsa/index.html)
+You can try `elsa` online at [this link](https://elsa.goto.ucsd.edu/index.html)
 
+
 ## Install
 
 You can locally build and run `elsa` by
@@ -31,7 +32,9 @@
 ```
 ## Editor Plugins
 
-- [VSCode](https://github.com/mistzzt/vscode-elsa-lang)
+- [VS Code extension](https://marketplace.visualstudio.com/items?itemName=akainth015.elsa-lang) with syntax highlighting and autocompletion support
+  - [Source](https://github.com/akainth015/vscode-elsa-lang)
+  - Contributed by [**@akainth015**](https://github.com/akainth015/), based on the [original version](https://github.com/mistzzt/vscode-elsa-lang) by [**@mistzzt**](https://github.com/mistzzt)
 - [Vim](https://github.com/glapa-grossklag/elsa.vim)
 
 ## Overview
@@ -51,7 +54,7 @@
   =d> zero                    -- expand definitions
 
 eval id_zero_tr :
-  id zero  
+  id zero
   =*> zero                    -- transitive reductions
 ```
 
@@ -63,6 +66,82 @@
 OK id_zero, id_zero_tr.
 ```
 
+## Operators and Normal Form Checking
+
+Elsa supports several operators with optional normal form checking:
+
+### Basic Operators
+- `=a>` - alpha equivalence
+- `=b>` - single beta reduction
+- `=e>` - single eta reduction
+- `=d>` - definition expansion
+- `=n>` - normal order beta reduction
+- `=p>` - applicative order beta reduction
+- `=*>` - transitive closure of reductions
+
+### Normal Form Extensions
+All operators can be extended with normal form checks:
+- `=op:s>` - check strong normal form after operation
+- `=op:w>` - check weak normal form after operation
+- `=op:h>` - check head normal form after operation
+
+Examples:
+```haskell
+-- nf_0.lc
+let id = \z -> z
+
+-- Check beta reduction to weak normal form
+conf example1:
+  (\x y -> x (\w -> w w)) id
+  =b:w> (\y -> id (\w -> w w))
+
+-- Check beta reduction to head normal form
+conf example2:
+  ((\x -> x) Z) (\x y -> x (\w -> w w)) id
+  =b:h> Z (\x y -> x (\w -> w w)) id
+
+-- Normal order reduction to strong normal form
+conf example3:
+  (\x y -> x) id
+  =n:s> \y -> id
+```
+
+### Strategy-Specific Transitive Reductions
+- `=n*>` - normal order transitive reductions
+- `=p*>` - applicative order transitive reductions
+
+Example:
+```haskell
+-- sptr_0.lc
+
+-- The numbers 0, 1, 3, 6 in church encoding
+let c0 = \f x -> x
+let c1 = \f x -> f x
+let c3 = \f x -> f (f (f x))
+let c6 = \f x -> f (f (f (f (f (f x)))))
+
+-- Boolean functions
+let true = \x y -> x
+let false = \x y -> y
+
+-- Number operations
+let iszero = \n -> n (\x -> false) true
+let pred = \n f x -> n (\g h -> h (g f)) (\u -> x) (\u -> u)
+let mult = \m n f x -> m (n f) x
+
+-- Fixed-point combinator and recursive function
+let Y = \g -> (\x -> g (x x)) (\x -> g (x x))
+let G = \f n -> iszero n c1 (mult n (f (pred n)))
+let fact = Y G
+
+eval factorial:
+  fact c3
+  -- The next line shows that we can show specific intermediate steps and leave out the rest
+  =n*> iszero c3 c1 (mult c3 (((\x -> G (x x)) (\x -> G (x x))) (pred c3)))
+  =n*> c6 --In this case, using =~> also works
+
+```
+
 ## Partial Evaluation
 
 If instead you write a partial sequence of
@@ -110,6 +189,22 @@
   =d> two                             -- optional
 ```
 
+Or you can change evaluation method, by changing
+`eval` to `conf` (see also next section)
+
+```haskell
+-- succ_1_alt.lc
+let one  = \f x -> f x
+let two  = \f x -> f (f x)
+let incr = \n f x -> f (n f x)
+
+conf succ_one :
+  incr one
+  =d> (\n f x -> f (n f x)) (\f x -> f x)
+  =b> \f x -> f ((\f x -> f x) f x)
+  =b> \f x -> f ((\x -> f x) x)
+```
+
 Similarly, `elsa` rejects the following program,
 
 ```haskell
@@ -137,16 +232,32 @@
 You can fix the error by inserting the appropriate
 intermediate term as shown in `id_0.lc` above.
 
+## Confirmation Statements
+
+The `conf` statement works like `eval` but
+doesn't require the final term to be in normal
+form. This is useful for infinite reductions
+or intermediate proofs.
+
+Example:
+```haskell
+-- om_0.lc
+let omega = (\x -> x x) (\x -> x x)
+
+conf omega_reduces_to_self:
+  omega
+  =d> (\x -> x x) (\x -> x x)
+  =b> (\x -> x x) (\x -> x x)
+  =d> omega
+```
+
 ## Syntax of `elsa` Programs
 
 An `elsa` program has the form
 
 ```haskell
--- definitions
-[let <id> = <term>]+
-
--- reductions
-[<reduction>]*
+-- definitions and evaluations can be mixed
+  ([let <id> = <term>] | [<reduction>])*
 ```
 
 where the basic elements are lambda-calulus `term`s
@@ -156,8 +267,7 @@
           \ <id>+ -> <term>
             (<term> <term>)
 ```
-
-and `id` are lower-case identifiers            
+and `id` are lower-case identifiers
 
 ```
 <id>   ::= x, y, z, ...
@@ -167,69 +277,99 @@
 with a `<step>`
 
 ```haskell
-<reduction> ::= eval <id> : <term> (<step> <term>)*
+<reduction> ::= (eval | conf) <id> : <term> (<step> <term>)*
 
-<step>      ::= =a>   -- alpha equivalence
-                =b>   -- beta  equivalence
-                =d>   -- def   equivalence
-                =*>   -- trans equivalence
-                =~>   -- normalizes to
+<step> ::= =, <equivtype>, [:, <nfcheck>], >
+
+<equivtype> ::= a   -- alpha equivalence
+                b   -- beta  equivalence
+                e   -- eta   equivalence
+                d   -- def   equivalence
+                *   -- trans equivalence
+                n   -- normal order            beta equivalence
+                p   -- applicative order       beta equivalence
+                n*  -- normal order      trans beta equivalence
+                p*  -- applicative order trans beta equivalence
+                ~   -- normalizes to
+
+<nfcheck> ::= s -- strong normal form check
+              w -- weak normal form check
+              h -- head normal form check
 ```
 
 
 ## Semantics of `elsa` programs
 
-A `reduction` of the form `t_1 s_1 t_2 s_2 ... t_n` is **valid** if
+An `eval` `reduction` of the form `t_1 s_1 t_2 s_2 ... t_n` is **valid** if
 
 * Each `t_i s_i t_i+1` is **valid**, and
 * `t_n` is in normal form (i.e. cannot be further beta-reduced.)
 
-Furthermore, a `step` of the form  
+Furthermore, a `step` of the form
 
 * `t =a> t'` is valid if `t` and `t'` are equivalent up to **alpha-renaming**,
 * `t =b> t'` is valid if `t` **beta-reduces** to `t'` in a single step,
 * `t =d> t'` is valid if `t` and `t'` are identical after **let-expansion**.
 * `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'`.
+             of the union of the above three relations,
+* `t =n> t'` is valid if `t` **beta-reduces** using normal order to `t'` in
+             a single step,
+* `t =p> t'` is valid if `t` **beta-reduces** using applicative order to `t'`
+             in a single step,
+* `t =n*> t'` is valid if `t` and `t'` are in the reflexive, transitive closure
+             of the union of the `=a>`, `=d>` and `=n>` operator relations,
+* `t =p*> t'` is valid if `t` and `t'` are in the reflexive, transitive closure
+             of the union of the `=a>`, `=d>` and `=p>` operator relations,
+* `t =~> t'` is valid if `t` [normalizes to][normalform] `t'`,
+* `t =e> t'` is valid if `t` **eta-reduces** to `t'` in a single step.
 
+A `conf` `reduction` of the form `t_1 s_1 t_2 s_2 ... t_n` is similar to the
+`eval` `reduction` of the same form, except that `t_n` *does not* have to be
+in normal form.
 
+Each `reduction` supports an optional `nfcheck`, which specifically checks
+whether the operator is in the requested normal form, in addition to checking
+the functionality of the operator. For example, `t =b:w> t'` not only checks
+whether `t` can be reduced to `t'` in a single step, but also whether the
+result is in weak normal form.
+
+
 (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'` 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*. 
+* `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 
+  (\x y -> x y) (\x -> x) b
   =*> b
 
 eval ex2:
-  (\x y -> x y) (\x -> x) b 
+  (\x y -> x y) (\x -> x) b
   =~> b
 
 eval ex3:
-  (\x y -> x y) (\x -> x) (\z -> z) 
-  =*> (\x -> x) (\z -> z) 
+  (\x y -> x y) (\x -> x) (\z -> z)
+  =*> (\x -> x) (\z -> z)
   =b> (\z -> z)
 ```
 
-but `elsa` would *not* accept 
+but `elsa` would *not* accept
 
 ```
 eval ex3:
-  (\x y -> x y) (\x -> x) (\z -> z) 
-  =~> (\x -> x) (\z -> z) 
+  (\x y -> x y) (\x -> x) (\z -> z)
+  =~> (\x -> x) (\z -> z)
   =b> (\z -> z)
 ```
 
diff --git a/elsa.cabal b/elsa.cabal
--- a/elsa.cabal
+++ b/elsa.cabal
@@ -1,5 +1,5 @@
 name:                elsa
-version:             0.2.2.0
+version:             0.3.0.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
@@ -31,16 +31,16 @@
   Default-Extensions: OverloadedStrings
 
   build-depends:       base >= 4 && < 5,
-                       array,
-                       mtl,
-                       megaparsec >= 7.0.4,
-                       ansi-terminal,
-                       hashable,
-                       unordered-containers,
-                       directory,
-                       filepath,
-                       dequeue,
-                       json
+                       array >= 0.5.8 && < 1,
+                       mtl >= 2.3.1 && < 3,
+                       megaparsec >= 9.7.0 && < 10,
+                       ansi-terminal >= 1.1.2 && < 2,
+                       hashable >= 1.5.0 && < 2,
+                       unordered-containers >= 0.2.20 && < 1,
+                       directory >= 1.3.9 && < 2,
+                       filepath >= 1.5.4 && < 2,
+                       dequeue >= 0.1.12 && < 1,
+                       json >= 0.11 && < 1
 
   hs-source-dirs:      src
   default-language:    Haskell2010
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,4 +1,4 @@
-{-# LANGUAGE OverloadedStrings, BangPatterns #-}
+{-# LANGUAGE OverloadedStrings, BangPatterns, ScopedTypeVariables #-}
 
 module Language.Elsa.Eval (elsa, elsaOn) where
 
@@ -7,9 +7,11 @@
 import qualified Data.HashSet         as S
 import qualified Data.List            as L
 import           Control.Monad.State
+import           Control.Monad        (foldM)
 import qualified Data.Maybe           as Mb -- (isJust, maybeToList)
 import           Language.Elsa.Types
 import           Language.Elsa.Utils  (qPushes, qInit, qPop, fromEither)
+import Data.List (group)
 
 --------------------------------------------------------------------------------
 elsa :: Elsa a -> [Result a]
@@ -32,7 +34,7 @@
 checkDupEval = foldM addEvalId S.empty
 
 addEvalId :: S.HashSet Id -> Eval a -> CheckM a (S.HashSet Id)
-addEvalId s e = 
+addEvalId s e =
   if S.member (bindId b) s
     then Left  (errDupEval b)
     else Right (S.insert (bindId b) s)
@@ -46,8 +48,8 @@
 mkEnv = foldM expand M.empty
 
 expand :: Env a -> Defn a -> CheckM a (Env a)
-expand g (Defn b e) = 
-  if dupId 
+expand g (Defn b e) =
+  if dupId
     then Left (errDupDefn b)
     else case zs of
       (x,l) : _ -> Left  (Unbound b x l)
@@ -65,12 +67,17 @@
 --------------------------------------------------------------------------------
 eval :: Env a -> Eval a -> CheckM a (Result a)
 --------------------------------------------------------------------------------
-eval g (Eval n e steps) = go e steps
+eval g (Eval kind n e steps) = go e steps
   where
     go e []
-      | isNormal g e    = return (OK n)
-      | otherwise       = Left (errPartial n e)
-    go e (s:steps)      = step g n e s >>= (`go` steps)
+      | noCheck kind || isNormal g e = return (OK n)
+      | otherwise                    = Left (errPartial n e)
+    go e (s:steps)                   = step g n e s >>= (`go` steps)
+    -- Regular is just "eval", then there is always a strong normal form check
+    -- at the end
+    noCheck Regular = False
+    -- Similar to "Regular" but without a strong normal form check at the end
+    noCheck Conf    = True
 
 step :: Env a -> Bind a -> Expr a -> Step a -> CheckM a (Expr a)
 step g n e (Step k e')
@@ -78,23 +85,37 @@
   | otherwise     = Left (errInvalid n e k e')
 
 isEq :: Eqn a -> Env a -> Expr a -> Expr a -> Bool
-isEq (AlphEq _) = isAlphEq
-isEq (BetaEq _) = isBetaEq
-isEq (UnBeta _) = isUnBeta
-isEq (DefnEq _) = isDefnEq
-isEq (TrnsEq _) = isTrnsEq
-isEq (UnTrEq _) = isUnTrEq
-isEq (NormEq _) = isNormEq
-
+isEq (Eqn op chk _) =
+  case op of
+    EqAlpha          -> isAlphEq chk
+    EqBeta           -> isBetaEq chk
+    EqEta            -> isEtaaEq chk
+    EqDefn           -> isDefnEq chk
+    EqNormOrd        -> isNBetaEq chk
+    EqAppOrd         -> isABetaEq chk
+    EqTrans          -> isTrnsEq chk
+    EqNormTrans      -> toNormEq --chk unnecessary
+    EqNormOrdTrans   -> isNTrnsEq chk
+    EqAppOrdTrans    -> isATrnsEq chk
+    EqUnBeta         -> isUnBeta
+    EqUnEta          -> isUnEtaa
+    EqUnNormOrd      -> isUnNBeta
+    EqUnAppOrd       -> isUnABeta
+    EqUnTrans        -> isUnTrEq
+    EqUnNormOrdTrans -> isUnNTrEq
+    EqUnAppOrdTrans  -> isUnATrEq
 
 --------------------------------------------------------------------------------
 -- | Transitive Reachability
 --------------------------------------------------------------------------------
-isTrnsEq :: Env a -> Expr a -> Expr a -> Bool
-isTrnsEq g e1 e2 = Mb.isJust (findTrans (isEquiv g e2) (canon g e1))
+isTrnsEq :: Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
+isTrnsEq Nothing g e1 e2 = Mb.isJust (findTrans (isEquiv g e2) (canon g e1))
+isTrnsEq (Just Strong) g e1 e2 = isTnsSEq isNormEq g e1 e2
+isTrnsEq (Just Weak) g e1 e2 = isTnsSEq isWnfEq g e1 e2
+isTrnsEq (Just Head) g e1 e2 = isTnsSEq isHnfEq g e1 e2
 
 isUnTrEq :: Env a -> Expr a -> Expr a -> Bool
-isUnTrEq g e1 e2 = isTrnsEq g e2 e1
+isUnTrEq g e1 e2 = isTrnsEq Nothing g e2 e1
 
 findTrans :: (Expr a -> Bool) -> Expr a -> Maybe (Expr a)
 findTrans p e = go S.empty (qInit e)
@@ -107,18 +128,74 @@
              then return e
              else go (S.insert e seen) (qPushes q (betas e))
 
+-- findTrans with selected normal form check
+isTnsSEq :: (Env a -> Expr a -> Expr a -> Bool) -> Env a -> Expr a -> Expr a -> Bool
+isTnsSEq isNfEq g e1 e2 = maybe False (flip (isNfEq g) e2) (findTrans (isEquiv g e2) (canon g e1))
+
+-- Multiple normal order beta, alpha reductions and/or definitions
+isNTrnsEq :: Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
+isNTrnsEq Nothing = isSTrnsEq norStep
+isNTrnsEq (Just Strong) = isSTrnsSEq norStep isNormEq
+isNTrnsEq (Just Weak) = isSTrnsSEq norStep isWnfEq
+isNTrnsEq (Just Head) = isSTrnsSEq norStep isHnfEq
+
+isUnNTrEq :: Env a -> Expr a -> Expr a -> Bool
+isUnNTrEq g e1 e2 = isNTrnsEq Nothing g e2 e1
+
+-- Multiple applicative order beta, alpha reductions and/or definitions
+isATrnsEq :: Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
+isATrnsEq Nothing = isSTrnsEq appStep
+isATrnsEq (Just Strong) = isSTrnsSEq appStep isNormEq
+isATrnsEq (Just Weak) = isSTrnsSEq appStep isWnfEq
+isATrnsEq (Just Head) = isSTrnsSEq appStep isHnfEq
+
+isUnATrEq :: Env a -> Expr a -> Expr a -> Bool
+isUnATrEq g e1 e2 = isATrnsEq Nothing g e2 e1
+
+-- Multiple beta, alpha reductions and/or definitions, using selected strategy
+isSTrnsEq :: forall a. (Expr a -> Maybe (Expr a)) -> Env a -> Expr a -> Expr a -> Bool
+isSTrnsEq step g e1 e2 = Mb.isJust (findSTrans step (isEquiv g e2) (canon g e1))
+
+findSTrans :: (Expr a -> Maybe (Expr a)) -> (Expr a -> Bool) -> Expr a -> Maybe (Expr a)
+findSTrans step f e = do
+  if f e then -- Maybe no reductions are needed
+    return e
+  else do -- One or more reductions are needed
+    e' <- step e
+    if f e' then
+      return e'
+    else
+      findSTrans step f e'
+
+-- isSTrnsEq with selected normal form check
+isSTrnsSEq :: (Expr a -> Maybe (Expr a)) -> (Env a -> Expr a -> Expr a -> Bool) -> Env a -> Expr a -> Expr a -> Bool
+isSTrnsSEq step isNfEq g e1 e2 =
+  case findSTrans step (isEquiv g e2) (canon g e1) of
+    Nothing -> False
+    Just e1' -> isNfEq g e1' e2
+
 --------------------------------------------------------------------------------
 -- | Definition Equivalence
 --------------------------------------------------------------------------------
-isDefnEq :: Env a -> Expr a -> Expr a -> Bool
-isDefnEq g e1 e2 = subst e1 g == subst e2 g
+isDefnEq :: Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
+isDefnEq Nothing g e1 e2 = subst e1 g == subst e2 g
+isDefnEq (Just Strong) g e1 e2 = isNormEq g e1 e2
+isDefnEq (Just Weak) g e1 e2 = isWnfEq g e1 e2
+isDefnEq (Just Head) g e1 e2 = isHnfEq g e1 e2
 
 --------------------------------------------------------------------------------
 -- | Alpha Equivalence
 --------------------------------------------------------------------------------
-isAlphEq :: Env a -> Expr a -> Expr a -> Bool
-isAlphEq _ e1 e2 = alphaNormal e1 == alphaNormal e2
+isAlphEq :: Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
+isAlphEq Nothing _ e1 e2 = alphaNormal e1 == alphaNormal e2
+isAlphEq (Just Strong) g e1 e2 = isAlphPEq isNormEq g e1 e2
+isAlphEq (Just Weak) g e1 e2 = isAlphPEq isWnfEq g e1 e2
+isAlphEq (Just Head) g e1 e2 = isAlphPEq isHnfEq g e1 e2
 
+-- Alpha Equivalence with provided normal form check
+isAlphPEq :: (Env a -> Expr a -> Expr a -> Bool) -> Env a -> Expr a -> Expr a -> Bool
+isAlphPEq isNfEq g e1 e2 = (alphaNormal e1 == alphaNormal e2) && isNfEq g e1 e2
+
 alphaNormal :: Expr a -> Expr a
 alphaNormal = alphaShift 0
 
@@ -165,12 +242,77 @@
 --------------------------------------------------------------------------------
 -- | Beta Reduction
 --------------------------------------------------------------------------------
-isBetaEq :: Env a -> Expr a -> Expr a -> Bool
-isBetaEq _ e1 e2 = or [ e1' == e2  | e1' <- betas e1 ]
+-- Beta reduction, without any normal form check
+isBetaEq :: Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
+isBetaEq Nothing _ e1 e2 = or [ e1' == e2  | e1' <- betas e1 ]
+isBetaEq (Just Strong) g e1 e2 = isBetaPEq isNormEq g e1 e2
+isBetaEq (Just Weak) g e1 e2 = isBetaPEq isWnfEq g e1 e2
+isBetaEq (Just Head) g e1 e2 = isBetaPEq isHnfEq g e1 e2
 
 isUnBeta :: Env a -> Expr a -> Expr a -> Bool
-isUnBeta g e1 e2 = isBetaEq g e2 e1
+isUnBeta g e1 e2 = isBetaEq Nothing g e2 e1
 
+-- Beta reduction, with provided normal form check
+isBetaPEq :: (Env a -> Expr a -> Expr a -> Bool) -> Env a -> Expr a -> Expr a -> Bool
+isBetaPEq isNfEq g e1 e2 = or [ isNfEq g e1' e2  | e1' <- betas e1 ]
+
+-- Use normal order evaluation strategy
+isNBetaEq :: Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
+isNBetaEq = isSBetaEq norStep
+
+isUnNBeta :: Env a -> Expr a -> Expr a -> Bool
+isUnNBeta g e1 e2 = isNBetaEq Nothing g e2 e1
+
+-- Use applicative order evaluation strategy
+isABetaEq :: Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
+isABetaEq = isSBetaEq appStep
+
+isUnABeta :: Env a -> Expr a -> Expr a -> Bool
+isUnABeta g e1 e2 = isABetaEq Nothing g e2 e1
+
+-- Use selected order evaluation strategy
+isSBetaEq :: (Expr a -> Maybe (Expr a)) -> Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
+isSBetaEq step Nothing g e1 e2 = step (subst e1 g) == Just (subst e2 g)
+isSBetaEq step (Just Strong) g e1 e2 = case step (subst e1 g) of
+  Nothing -> False
+  Just e1' -> isNormEq g e1' e2
+isSBetaEq step (Just Weak) g e1 e2 = case step (subst e1 g) of
+  Nothing -> False
+  Just e1' -> isWnfEq g e1' e2
+isSBetaEq step (Just Head) g e1 e2 = case step (subst e1 g) of
+  Nothing -> False
+  Just e1' -> isHnfEq g e1' e2
+
+-- norStep is a single normal order reduction
+norStep :: Expr a -> Maybe (Expr a)
+norStep (EVar {}) = Nothing
+norStep (ELam b e l) = do
+  e' <- norStep e
+  return $ ELam b e' l
+norStep (EApp e1@(ELam {}) e2 _) = beta e1 e2
+norStep (EApp e1 e2 l) = case norStep e1 of
+  Just e1' -> return $ EApp e1' e2 l
+  Nothing -> case norStep e2 of
+    Just e2' -> return $ EApp e1 e2' l
+    Nothing -> Nothing
+
+-- appStep is a single applicative order reduction
+appStep :: Expr a -> Maybe (Expr a)
+appStep (EVar {}) = Nothing
+appStep (ELam b e l) = do
+  e' <- appStep e
+  return $ ELam b e' l
+appStep (EApp e1@(ELam {}) e2 l) = case appStep e1 of
+  Just e1' -> Just $ EApp e1' e2 l
+  Nothing -> case appStep e2 of
+    Just e2' -> Just $ EApp e1 e2' l
+    Nothing -> beta e1 e2
+appStep (EApp e1 e2 l) = case appStep e1 of
+  Just e1' -> return $ EApp e1' e2 l
+  Nothing -> case appStep e2 of
+    Just e2' -> return $ EApp e1 e2' l
+    Nothing -> Nothing
+
 isNormal :: Env a -> Expr a -> Bool
 isNormal g = null . betas . (`subst` g)
 
@@ -208,30 +350,126 @@
 isIn = S.member . bindId
 
 --------------------------------------------------------------------------------
+-- | Eta Reduction
+--------------------------------------------------------------------------------
+-- Eta reduction, without any normal form check
+isEtaaEq :: Maybe NormCheck -> Env a -> Expr a -> Expr a -> Bool
+isEtaaEq Nothing g e1 e2 = go e1 (subst e2 g)
+  where
+    go e1 e2' = or [e1' == e2' | e1' <- etas g e1]
+isEtaaEq (Just Strong) g e1 e2 = isEtaPEq isNormEq g e1 e2
+isEtaaEq (Just Weak) g e1 e2 = isEtaPEq isWnfEq g e1 e2
+isEtaaEq (Just Head) g e1 e2 = isEtaPEq isHnfEq g e1 e2
+
+isUnEtaa :: Env a -> Expr a -> Expr a -> Bool
+isUnEtaa g e1 e2 = isEtaaEq Nothing g e2 e1
+
+-- Eta reduction, with provided normal form check
+isEtaPEq :: (Env a -> Expr a -> Expr a -> Bool) -> Env a -> Expr a -> Expr a -> Bool
+isEtaPEq isNfEq g e1 e2 = or [isNfEq g e1' e2 | e1' <- etas g e1]
+
+-- Search for an eta reduction.
+-- Returns the reduced formula if one can be found,
+-- returns Nothing if no reductions are possible
+eta :: Expr a -> Maybe (Expr a)
+eta (ELam x (EApp e (EVar x' _) _) _) =
+  let zs = freeVars e in
+  if (bindId x == x') && not (isIn x zs)
+    then
+      Just e
+    else Nothing
+eta _ = Nothing
+
+etas :: Env a -> Expr a -> [Expr a]
+etas g e = go (subst e g)
+  where
+    go (EVar {})        = []
+    -- Pattern where reduction might be possible
+    go e'@(ELam b e1 z) = Mb.maybeToList (eta e')
+                       ++ [ELam b e1' z | e1' <- go e1]
+    go (EApp e1 e2 z)   = [EApp e1' e2 z | e1' <- go e1]
+                       ++ [EApp e1 e2' z | e2' <- go e2]
+
+--------------------------------------------------------------------------------
 -- | Evaluation to Normal Form
 --------------------------------------------------------------------------------
+-- Check if e1 is strong normal form
 isNormEq :: Env a -> Expr a -> Expr a -> Bool
-isNormEq g e1 e2 = eqVal (subst e2 g) $ evalNbE ML.empty (subst e1 g)
+isNormEq g e1 e2 = (e1' == e2') && nEqVal e2' (nf e2')
   where
-    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)
+    e1' = alphaNormal $ subst e1 g
+    e2' = alphaNormal $ subst e2 g
+    nf = evalNbE ML.empty
 
-    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
+toNormEq :: Env a -> Expr a -> Expr a -> Bool
+toNormEq g e1 e2 = nEqVal (subst e2 g) $ evalNbE ML.empty (subst e1 g)
 
+evalNbE :: ML.HashMap Id Value -> Expr a -> Value
+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)
+
+nEqVal :: Expr a -> Value -> Bool
+nEqVal (EVar x _) (Neutral x' [])
+  = x == x'
+nEqVal (ELam (Bind x _) b _) (Fun f)
+  = nEqVal b (f (Neutral x []))
+nEqVal (EApp f a _) (Neutral x (a':args))
+  = nEqVal a a' && nEqVal f (Neutral x args)
+nEqVal _ _ = False
+
 -- | NbE semantic domain
 data Value = Fun !(Value -> Value) | Neutral !Id ![Value]
 
 --------------------------------------------------------------------------------
+-- | Evaluation to Weak Normal Form
+--------------------------------------------------------------------------------
+isWnfEq :: Env a -> Expr a -> Expr a -> Bool
+isWnfEq g e1 e2 = (e1' == e2') && (e2' == wnf e2')
+  where
+    e1' = alphaNormal $ subst e1 g
+    e2' = alphaNormal $ subst e2 g
+    wnf :: Expr a -> Expr a
+    wnf e@(EVar {}) = e
+    wnf e@(ELam {}) = e
+    wnf (EApp f arg l) = case wnf f of
+      f'@ELam {} -> maybe (EApp f' (wnf arg) l) wnf (beta f $ wnf arg)
+      f' -> EApp f' (wnf arg) l
+
+--------------------------------------------------------------------------------
+-- | Evaluation to Head Normal Form
+--------------------------------------------------------------------------------
+isHnfEq :: Env a -> Expr a -> Expr a -> Bool
+isHnfEq g e1 e2 = (e1' == e2') && (e2' == hnf e2')
+  where
+    e1' = alphaNormal $ subst e1 g
+    e2' = alphaNormal $ subst e2 g
+    hnf :: Expr a -> Expr a
+    hnf e@(EVar {}) = e
+    hnf (ELam bi b a) = ELam bi (hnf b) a
+    hnf (EApp f arg l) = case hnf f of
+      f'@ELam {} -> maybe (EApp f' (hnf arg) l) hnf (beta f' arg)
+      f' -> EApp f' arg l
+
+--------------------------------------------------------------------------------
+-- | Evaluation to Weak Head Normal Form
+--------------------------------------------------------------------------------
+{- isWhnfEq :: Env a -> Expr a -> Expr a -> Bool
+isWhnfEq g e1 e2 = (e1' == e2') && (e2' == whnf e2')
+  where
+    e1' = subst e1 g
+    e2' = subst e2 g
+    whnf :: Expr a -> Expr a
+    whnf e@(EVar {}) = e
+    whnf e@(ELam {}) = e
+    whnf (EApp f arg l) = case whnf f of
+      f'@ELam {} -> maybe (EApp f' arg l) whnf (beta f arg)
+      f' -> EApp f' arg l -}
+
+--------------------------------------------------------------------------------
 -- | General Helpers
 --------------------------------------------------------------------------------
 freeVars :: Expr a -> S.HashSet Id
@@ -253,7 +491,7 @@
 canon g = alphaNormal . (`subst` g)
 
 isEquiv :: Env a -> Expr a -> Expr a -> Bool
-isEquiv g e1 e2 = isAlphEq g (subst e1 g) (subst e2 g)
+isEquiv g e1 e2 = isAlphEq Nothing g (subst e1 g) (subst e2 g)
 --------------------------------------------------------------------------------
 -- | Error Cases
 --------------------------------------------------------------------------------
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
@@ -103,7 +103,7 @@
 
 -- | list of reserved words
 keywords :: [Text]
-keywords = [ "let"  , "eval" ]
+keywords = [ "let"  , "eval"  , "conf" ]
 
 -- | `identifier` parses identifiers: lower-case alphabets followed by alphas or digits
 identifier :: Parser (String, SourceSpan)
@@ -140,8 +140,18 @@
 --------------------------------------------------------------------------------
 --------------------------------------------------------------------------------
 elsa :: Parser SElsa
-elsa = Elsa <$> many defn <*> many eval
+elsa = do
+  items <- many elsaItem
+  pure $
+    Elsa
+      { defns = [d | DefnItem d <- items],
+        evals = [e | EvalItem e <- items]
+      }
 
+elsaItem :: Parser SElsaItem
+elsaItem = 
+  (DefnItem <$> defn) <|> (EvalItem <$> eval)
+
 defn :: Parser SDefn
 defn = do
   rWord "let"
@@ -151,24 +161,63 @@
 
 eval :: Parser SEval
 eval = do
-  rWord "eval"
+  kind <- (rWord "eval" >> return Regular) <|> (rWord "conf" >> return Conf)
   name  <- binder
   colon
   root  <- expr
   steps <- many step
-  return $ Eval name root steps
+  return $ Eval kind name root steps
 
 step :: Parser SStep
 step = Step <$> eqn <*> expr
 
 eqn :: Parser SEqn
-eqn =  try (withSpan' (symbol "=a>" >> return AlphEq))
-   <|> try (withSpan' (symbol "=b>" >> return BetaEq))
-   <|> try (withSpan' (symbol "<b=" >> return UnBeta))
-   <|> try (withSpan' (symbol "=d>" >> return DefnEq))
-   <|> try (withSpan' (symbol "=*>" >> return TrnsEq))
-   <|> try (withSpan' (symbol "<*=" >> return UnTrEq))
-   <|>     (withSpan' (symbol "=~>" >> return NormEq))
+eqn = withSpan' parseEqn
+
+parseEqn :: Parser (SourceSpan -> Eqn SourceSpan)
+parseEqn = try parseUnEqn <|> parseRegEqn
+
+parseUnEqn :: Parser (SourceSpan -> Eqn SourceSpan)
+parseUnEqn = do
+  void $ char '<'
+  op <- choice
+    [ try (symbol "n*=") >> return EqUnNormOrdTrans
+    , try (symbol "p*=") >> return EqUnAppOrdTrans
+    , try (symbol "b=")  >> return EqUnBeta
+    , try (symbol "n=") >> return EqUnNormOrd
+    , try (symbol "p=") >> return EqUnAppOrd
+    , try (symbol "e=")  >> return EqUnEta
+    , try (symbol "*=")  >> return EqUnTrans
+    ]
+  return $ \sp -> Eqn op Nothing sp
+
+parseRegEqn :: Parser (SourceSpan -> Eqn SourceSpan)
+parseRegEqn = do
+  void $ char '='
+  op <- choice
+    [ try (string "n*") >> return EqNormOrdTrans
+    , try (string "p*") >> return EqAppOrdTrans
+    , try (string "n") >> return EqNormOrd
+    , try (string "p") >> return EqAppOrd
+    , try (string "a")  >> return EqAlpha
+    , try (string "b")  >> return EqBeta
+    , try (string "e")  >> return EqEta
+    , try (string "d")  >> return EqDefn
+    , try (string "*")  >> return EqTrans
+    , try (string "~")  >> return EqNormTrans
+    ]
+  mChk <- optional parseNormCheck
+  void $ symbol ">"
+  return $ \sp -> Eqn op mChk sp
+
+parseNormCheck :: Parser NormCheck
+parseNormCheck = do
+  void $ char ':'
+  choice
+    [ char 's' >> return Strong
+    , char 'w' >> return Weak
+    , char 'h' >> return Head
+    ]
 
 expr :: Parser SExpr
 expr =  try lamExpr
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
@@ -2,6 +2,7 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE DeriveGeneric     #-}
 {-# LANGUAGE DeriveFunctor     #-}
+{-# LANGUAGE InstanceSigs #-}
 
 module Language.Elsa.Types where
 
@@ -11,15 +12,16 @@
 import           Data.Maybe (mapMaybe)
 import           Data.Hashable
 
-type Id      = String
-type SElsa   = Elsa SourceSpan
-type SDefn   = Defn SourceSpan
-type SExpr   = Expr SourceSpan
-type SEval   = Eval SourceSpan
-type SStep   = Step SourceSpan
-type SBind   = Bind SourceSpan
-type SEqn    = Eqn  SourceSpan
-type SResult = Result SourceSpan
+type Id        = String
+type SElsaItem = ElsaItem SourceSpan
+type SElsa     = Elsa SourceSpan
+type SDefn     = Defn SourceSpan
+type SExpr     = Expr SourceSpan
+type SEval     = Eval SourceSpan
+type SStep     = Step SourceSpan
+type SBind     = Bind SourceSpan
+type SEqn      = Eqn  SourceSpan
+type SResult   = Result SourceSpan
 
 --------------------------------------------------------------------------------
 -- | Result
@@ -64,6 +66,8 @@
 --------------------------------------------------------------------------------
 -- | Programs
 --------------------------------------------------------------------------------
+data ElsaItem a = DefnItem (Defn a) | EvalItem (Eval a)
+
 data Elsa a = Elsa
   { defns :: [Defn a]
   , evals :: [Eval a]
@@ -74,27 +78,53 @@
   = Defn !(Bind a) !(Expr a)
   deriving (Eq, Show)
 
+data EvalKind = Regular | Conf deriving (Eq, Show)
+
 data Eval a = Eval
-  { evName  :: !(Bind a)
+  { evKind  :: EvalKind
+  , evName  :: !(Bind a)
   , evRoot  :: !(Expr a)
   , evSteps :: [Step a]
-  }
-  deriving (Eq, Show)
+  } deriving (Eq, Show)
 
 data Step a
   = Step !(Eqn a) !(Expr a)
   deriving (Eq, Show)
 
-data Eqn a
-  = AlphEq a
-  | BetaEq a
-  | UnBeta a
-  | DefnEq a
-  | TrnsEq a
-  | UnTrEq a
-  | NormEq a
+{-
+  EqAlpha         : Alpha equivalence
+  EqBeta          : Beta reduction
+  EqEta           : Eta reduction
+  EqDefn          : Definition unpacking
+  EqNormOrd       : Normal order beta reduction
+  EqAppOrd        : Applicative order beta reduction
+  EqNormOrdTrans  : Normal order beta reduction with alpha equivalence and definition unpacking
+  EqAppOrdTrans   : Applicative order beta reduction with alpha equivalence and definition unpacking
+  EqTrans         : Zero or more beta reductions with alpha equivalence and definition unpacking
+  EqNormTrans     : Acts the same as the "=n*:s>" operator, no matter the normal form check
+  EqUnBeta        : Backwards beta reduction
+  EqUnEta         : Backwards eta reduction
+  EqUnNormOrd     : Backwards normal order beta reduction
+  EqUnAppOrd      : Backwards applicative order beta reduction
+  EqUnTrans       : Backwards zero or more beta reductions with alpha equivalence and definition unpacking
+  EqUnNormOrdTrans: Backwards normal order beta reduction with alpha equivalence and definition unpacking
+  EqUnAppOrdTrans : Backwards applicative order beta reduction with alpha equivalence and definition unpacking
+-}
+data EqnOp
+  = EqAlpha | EqBeta | EqEta | EqDefn
+  | EqNormOrd | EqAppOrd | EqTrans
+  | EqNormOrdTrans | EqAppOrdTrans
+  | EqNormTrans
+  | EqUnBeta | EqUnEta | EqUnNormOrd
+  | EqUnAppOrd | EqUnTrans
+  | EqUnNormOrdTrans | EqUnAppOrdTrans
   deriving (Eq, Show)
 
+-- Strong, weak, or head normal form check
+data NormCheck = Strong | Weak | Head deriving (Eq, Show)
+
+data Eqn a = Eqn EqnOp (Maybe NormCheck) a deriving (Eq, Show)
+
 data Bind a
   = Bind Id a
   deriving (Show, Functor)
@@ -172,13 +202,7 @@
   tag :: t a -> a
 
 instance Tagged Eqn where
-  tag (AlphEq x) = x
-  tag (BetaEq x) = x
-  tag (UnBeta x) = x
-  tag (DefnEq x) = x
-  tag (TrnsEq x) = x
-  tag (UnTrEq x) = x
-  tag (NormEq x) = x
+  tag (Eqn _ _ x) = x
 
 instance Tagged Bind where
   tag (Bind _   x) = x