diff --git a/Changelog.md b/Changelog.md
new file mode 100644
--- /dev/null
+++ b/Changelog.md
@@ -0,0 +1,2 @@
+* 0.0.0.90
+  Initial (re-)implementation effort.
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2014, Aleksey Kliger
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Aleksey Kliger nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,20 @@
+# unbound-generics
+
+[![Build Status](https://travis-ci.org/lambdageek/unbound-generics.svg)](https://travis-ci.org/lambdageek/unbound-generics)
+
+
+This is a reimplementation of (parts of) [unbound](http://hackage.haskell.org/package/unbound) but using [GHC generics](http://www.haskell.org/ghc/docs/latest/html/libraries/base-4.7.0.1/GHC-Generics.html) instead of [RepLib](https://hackage.haskell.org/package/RepLib).
+
+## Differences from `unbound`
+
+For the most part, I tried to keep the same methods with the same signatures.  However there are a few differences.
+
+1. `fv :: Alpha t => t -> Fold t (Name n)`
+
+   The `fv` method returns a `Fold` (in the sense of the [lens](http://hackage.haskell.org/package/lens) library),
+   rather than an `Unbound.Util.Collection` instance.  That means you will generally have to write `toListOf fv t` or some    other summary operation.
+
+2. `isPat :: Alpha t => t -> DisjointSet AnyName`
+
+   You should olnly notice this if you're implementing an instance of `Alpha` by hand (rather than by using the default
+   generic instance).  The original `unbound` returned a `Maybe [AnyName]` here with the same interpretation as `DisjointSet`: `Nothing` means an inconsistency was encountered, or `Just` the free variables of the pattern.
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/examples/F.hs b/examples/F.hs
new file mode 100644
--- /dev/null
+++ b/examples/F.hs
@@ -0,0 +1,170 @@
+{-# LANGUAGE DeriveGeneric,
+             DeriveDataTypeable,
+             FlexibleInstances,
+             FlexibleContexts,
+             MultiParamTypeClasses,
+             ScopedTypeVariables
+  #-}
+
+module F where
+
+import Unbound.Generics.LocallyNameless
+
+import GHC.Generics
+import Data.Typeable (Typeable)
+
+import Control.Monad.Identity
+import Control.Monad.Writer hiding (All)
+import Control.Monad.Trans.Error
+import Data.List as List
+
+
+-- System F with type and term variables
+
+type TyName = Name Ty
+type TmName = Name Tm
+
+data Ty = TyVar TyName
+        | Arr Ty Ty
+        | All (Bind TyName Ty)
+   deriving (Show, Generic, Typeable)
+
+data Tm = TmVar TmName
+        | Lam (Bind (TmName, Embed Ty) Tm)
+        | TLam (Bind TyName Tm)
+        | App Tm Tm
+        | TApp Tm Ty
+   deriving (Show, Generic, Typeable)
+
+------------------------------------------------------
+instance Alpha Ty
+instance Alpha Tm
+
+instance Subst Tm Ty
+instance Subst Tm Tm where
+  isvar (TmVar v) = Just (SubstName v)
+  isvar _  = Nothing
+
+instance Subst Ty Ty where
+  isvar (TyVar v) = Just (SubstName v)
+  isvar _ = Nothing
+
+------------------------------------------------------
+-- Example terms
+------------------------------------------------------
+
+x :: Name Tm
+y :: Name Tm
+z :: Name Tm
+(x,y,z) = (string2Name "x", string2Name "y", string2Name "z")
+
+a :: Name Ty
+b :: Name Ty
+c :: Name Ty
+(a,b,c) = (string2Name "a", string2Name "b", string2Name "c")
+
+-- /\a. \x:a. x
+polyid :: Tm
+polyid = TLam (bind a (Lam (bind (x, Embed (TyVar a)) (TmVar x))))
+
+-- All a. a -> a
+polyidty :: Ty
+polyidty = All (bind a (Arr (TyVar a) (TyVar a)))
+
+-- /\b. \y:b. y
+polyid2 :: Tm
+polyid2 = TLam (bind b (Lam (bind (y, Embed (TyVar b)) (TmVar y))))
+
+-- /\c. \y:b. y
+bad_polyid2 :: Tm
+bad_polyid2 = TLam (bind c (Lam (bind (y, Embed (TyVar b)) (TmVar y))))
+
+
+-----------------------------------------------------------------
+-- Typechecker
+-----------------------------------------------------------------
+type Delta = [ TyName ]
+type Gamma = [ (TmName, Ty) ]
+
+data Ctx = Ctx { getDelta :: Delta , getGamma :: Gamma }
+           deriving (Show)
+                    
+emptyCtx :: Ctx
+emptyCtx = Ctx { getDelta = [], getGamma = [] }
+
+type M = ErrorT String (WriterT [String] (FreshMT Identity))
+
+runM :: M a -> (a, [String])
+runM m = case (runIdentity $ runFreshMT $ runWriterT (runErrorT m)) of
+   (Left s, msgs)  -> error $ s ++ "\nLog: " ++ show msgs
+   (Right ans, msgs) -> (ans, msgs)
+
+checkTyVar :: Ctx -> TyName -> M ()
+checkTyVar g v = do
+    if List.elem v (getDelta g) then
+      return ()
+    else
+      throwError $ "NotFound: " ++ show v ++ " in " ++ show g
+
+lookupTmVar :: Ctx -> TmName -> M Ty
+lookupTmVar g v = do
+    case lookup v (getGamma g) of
+      Just s -> return s
+      Nothing -> throwError "NotFound"
+
+extendTy :: TyName -> Ctx -> Ctx
+extendTy n ctx = ctx { getDelta =  n : (getDelta ctx) }
+
+extendTm :: TmName -> Ty -> Ctx -> Ctx
+extendTm n ty ctx = ctx { getGamma = (n, ty) : (getGamma ctx) }
+
+tcty :: Ctx -> Ty -> M ()
+tcty g  (TyVar alpha) = do
+   trace $ "looking up tyvar " ++ show alpha
+   checkTyVar g alpha
+tcty g  (All bnder) = do
+   trace $ "checking " ++ show (All bnder)
+   (alpha, ty') <- unbind bnder
+   trace $ "unbinding All gave " ++ show alpha ++ " in " ++ show ty'
+   tcty (extendTy alpha g) ty'
+tcty g  (Arr t1 t2) = do
+   trace $ "checking " ++ show (Arr t1 t2)
+   tcty g  t1
+   tcty g  t2
+
+trace :: String -> M ()
+trace s = lift (tell [s])
+
+ti :: Ctx -> Tm -> M Ty
+ti g (TmVar v) = trace ("looking up " ++ show v) >> lookupTmVar g v
+ti g (Lam bnd) = do
+  trace $ "checking " ++ show (Lam bnd)
+  ((v, Embed ty1), t) <- unbind bnd
+  tcty g ty1
+  ty2 <- ti (extendTm v ty1 g) t
+  return (Arr ty1 ty2)
+ti g (App t1 t2) = do
+  trace $ "checking " ++ show (App t1 t2)
+  ty1 <- ti g t1
+  ty2 <- ti g t2
+  case ty1 of
+    Arr ty11 ty21 | ty2 `aeq` ty11 ->
+      return ty21
+    _ -> throwError "TypeError"
+ti g (TLam bnd) = do
+  trace $ "checking " ++ show (TLam bnd)
+  (v, t) <- unbind bnd
+  trace $ "unbinding TLam gave " ++ show v ++ " in " ++ show t
+  ty <- ti (extendTy v g) t
+  return (All (bind v ty))
+ti g (TApp t ty) = do
+  trace $ "checking " ++ show (TApp t ty)
+  tyt <- ti g t
+  case tyt of
+   (All bnder) -> do
+      tcty g  ty
+      (n1, ty1) <- unbind bnder
+      return $ subst n1 ty ty1
+   _ -> throwError $ "Expected a ForAll in a type application, got " ++ show tyt
+
+
diff --git a/src/Unbound/Generics/LocallyNameless.hs b/src/Unbound/Generics/LocallyNameless.hs
new file mode 100644
--- /dev/null
+++ b/src/Unbound/Generics/LocallyNameless.hs
@@ -0,0 +1,30 @@
+-- |
+-- Module     : Unbound.Generics.LocallyNameless
+-- Copyright  : (c) 2014, Aleksey Kliger
+-- License    : BSD3 (See LICENSE)
+-- Maintainer : Aleksey Kliger
+-- Stability  : experimental
+--
+--
+-- See 'Alpha', 'Bind', "Unbound.Generics.LocallyNameless.Operations" to get started. 
+module Unbound.Generics.LocallyNameless (
+  module Unbound.Generics.LocallyNameless.Alpha,
+  module Unbound.Generics.LocallyNameless.Name,
+  module Unbound.Generics.LocallyNameless.Operations,
+  module Unbound.Generics.LocallyNameless.Bind,
+  module Unbound.Generics.LocallyNameless.Embed,
+  module Unbound.Generics.LocallyNameless.Rebind,
+  module Unbound.Generics.LocallyNameless.Fresh,
+  module Unbound.Generics.LocallyNameless.LFresh,
+  module Unbound.Generics.LocallyNameless.Subst
+  ) where
+
+import Unbound.Generics.LocallyNameless.Alpha
+import Unbound.Generics.LocallyNameless.Name hiding (Bn, Fn)
+import Unbound.Generics.LocallyNameless.Bind hiding (B)
+import Unbound.Generics.LocallyNameless.Embed
+import Unbound.Generics.LocallyNameless.Rebind hiding (Rebnd)
+import Unbound.Generics.LocallyNameless.Fresh
+import Unbound.Generics.LocallyNameless.LFresh
+import Unbound.Generics.LocallyNameless.Operations
+import Unbound.Generics.LocallyNameless.Subst
diff --git a/src/Unbound/Generics/LocallyNameless/Alpha.hs b/src/Unbound/Generics/LocallyNameless/Alpha.hs
new file mode 100644
--- /dev/null
+++ b/src/Unbound/Generics/LocallyNameless/Alpha.hs
@@ -0,0 +1,610 @@
+{-# OPTIONS_HADDOCK show-extensions #-}
+-- |
+-- Module     : Unbound.Generics.LocallyNameless.Alpha
+-- Copyright  : (c) 2014, Aleksey Kliger
+-- License    : BSD3 (See LICENSE)
+-- Maintainer : Aleksey Kliger
+-- Stability  : experimental
+--
+-- Use the 'Alpha' typeclass to mark types that may contain 'Name's.
+{-# LANGUAGE DefaultSignatures
+             , FlexibleContexts
+             , TypeOperators #-}
+module Unbound.Generics.LocallyNameless.Alpha (
+  -- * Name-aware opertions
+  Alpha(..)
+  -- * Binder variables
+  , DisjointSet(..)
+  , inconsistentDisjointSet
+  , singletonDisjointSet
+  , isConsistentDisjointSet
+  -- * Implementation details
+  , NthPatFind
+  , NamePatFind
+  , AlphaCtx
+  , initialCtx
+  , patternCtx
+  , termCtx
+  , isTermCtx
+  , incrLevelCtx
+  ) where
+
+import Control.Applicative (Applicative(..), (<$>))
+import Control.Arrow (first)
+import Control.Monad (liftM)
+import Data.Function (on)
+import Data.Functor.Contravariant (Contravariant(..))
+import Data.Foldable (Foldable(..))
+import Data.List (intersect)
+import Data.Monoid (Monoid(..), (<>))
+import Data.Ratio (Ratio)
+import Data.Typeable (Typeable, gcast)
+import GHC.Generics
+
+import Unbound.Generics.LocallyNameless.Name
+import Unbound.Generics.LocallyNameless.Fresh
+import Unbound.Generics.LocallyNameless.LFresh
+import Unbound.Generics.PermM
+
+-- | Some 'Alpha' operations need to record information about their
+-- progress.  Instances should just pass it through unchanged.
+--
+-- The context records whether we are currently operating on terms or patterns,
+-- and how many binding levels we've descended.
+data AlphaCtx = AlphaCtx { ctxMode :: !Mode, ctxLevel :: !Integer }
+
+data Mode = Term | Pat
+          deriving Eq
+
+-- | The starting context for alpha operations: we are expecting to
+-- work on terms and we are under no binders.
+initialCtx :: AlphaCtx
+initialCtx = AlphaCtx { ctxMode = Term, ctxLevel = 0 }
+
+-- | Switches to a context where we expect to operate on patterns.
+patternCtx :: AlphaCtx -> AlphaCtx
+patternCtx ctx = ctx { ctxMode = Pat }
+
+-- | Switches to a context where we expect to operate on terms.
+termCtx :: AlphaCtx -> AlphaCtx
+termCtx ctx = ctx { ctxMode = Term }
+
+-- | Returns 'True' iff we are in a context where we expect to see terms.
+isTermCtx :: AlphaCtx -> Bool
+isTermCtx (AlphaCtx {ctxMode = Term}) = True
+isTermCtx _                           = False
+
+-- | Increment the number of binders that we are operating under.
+incrLevelCtx :: AlphaCtx -> AlphaCtx
+incrLevelCtx ctx = ctx { ctxLevel = 1 + ctxLevel ctx }
+
+-- | A @DisjointSet a@ is a 'Just' a list of distinct @a@s.  In addition to a monoidal
+-- structure, a disjoint set also has an annihilator 'inconsistentDisjointSet'.
+--
+-- @
+--   inconsistentDisjointSet \<> s == inconsistentDisjointSet
+--   s \<> inconsistentDisjoinSet == inconsistentDisjointSet
+-- @
+newtype DisjointSet a = DisjointSet (Maybe [a])
+
+instance Eq a => Monoid (DisjointSet a) where
+  mempty = DisjointSet (Just [])
+  mappend s1 s2 =
+    case (s1, s2) of
+      (DisjointSet (Just xs), DisjointSet (Just ys)) | disjointLists xs ys -> DisjointSet (Just (xs <> ys))
+      _ -> inconsistentDisjointSet
+
+instance Foldable DisjointSet where
+  foldMap summarize (DisjointSet ms) = foldMap (foldMap summarize) ms
+
+-- | Returns a @DisjointSet a@ that is the annihilator element for the 'Monoid' instance of 'DisjointSet'.
+inconsistentDisjointSet :: DisjointSet a
+inconsistentDisjointSet = DisjointSet Nothing
+
+-- | @singletonDisjointSet x@ a @DisjointSet a@ that contains the single element @x@
+singletonDisjointSet :: a -> DisjointSet a
+singletonDisjointSet x = DisjointSet (Just [x])
+
+disjointLists :: Eq a => [a] -> [a] -> Bool
+disjointLists xs ys = null (intersect xs ys)
+
+-- | @isConsistentDisjointSet@ returns @True@ iff the given disjoint set is not inconsistent.
+isConsistentDisjointSet :: DisjointSet a -> Bool
+isConsistentDisjointSet (DisjointSet Nothing) = False
+isConsistentDisjointSet _ = True
+
+-- | Types that are instances of @Alpha@ may participate in name representation.
+--
+-- Minimal instance is entirely empty, provided that your type is an instance of
+-- 'Generic'.
+class (Show a) => Alpha a where
+  -- | See 'Unbound.Generics.LocallyNameless.Operations.aeq'.
+  aeq' :: AlphaCtx -> a -> a -> Bool
+  default aeq' :: (Generic a, GAlpha (Rep a)) => AlphaCtx -> a -> a -> Bool
+  aeq' c = (gaeq c) `on` from
+
+  -- | See 'Unbound.Generics.LocallyNameless.Operations.fvAny'.
+  -- @@@ fvAny' :: AlphaCtx -> Fold a AnyName @@@
+  fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> a -> f a
+  default fvAny' :: (Generic a, GAlpha (Rep a), Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> a -> f a
+  fvAny' c nfn = fmap to . gfvAny c nfn . from
+
+  -- | Replace free names by bound names.
+  close :: Alpha b => AlphaCtx -> b -> a -> a
+  default close :: (Generic a, GAlpha (Rep a), Alpha b) => AlphaCtx -> b -> a -> a
+  close c b = to . gclose c b . from
+
+  -- | Replace bound names by free names.
+  open :: Alpha b => AlphaCtx -> b -> a -> a
+  default open :: (Generic a, GAlpha (Rep a), Alpha b) => AlphaCtx -> b -> a -> a
+  open c b = to . gopen c b . from
+
+  -- | @isPat x@ dynamically checks whether @x@ can be used as a valid pattern.
+  isPat :: a -> DisjointSet AnyName
+  default isPat :: (Generic a, GAlpha (Rep a)) => a -> DisjointSet AnyName
+  isPat = gisPat . from
+
+  -- | @isPat x@ dynamically checks whether @x@ can be used as a valid term.
+  isTerm :: a -> Bool
+  default isTerm :: (Generic a, GAlpha (Rep a)) => a -> Bool
+  isTerm = gisTerm . from
+
+  -- | @isEmbed@ is needed internally for the implementation of
+  --   'isPat'.  @isEmbed@ is true for terms wrapped in 'Embed' and zero
+  --   or more occurrences of 'Shift'.  The default implementation
+  --   simply returns @False@.
+  isEmbed :: a -> Bool
+  isEmbed _ = False
+
+  -- | If @a@ is a pattern, finds the @n@th name in the pattern
+  -- (starting from zero), returning the number of names encountered
+  -- if not found.
+  nthPatFind :: a -> NthPatFind
+  default nthPatFind :: (Generic a, GAlpha (Rep a)) => a -> NthPatFind
+  nthPatFind = gnthPatFind . from
+
+  -- | If @a@ is a pattern, find the index of the given name in the pattern.
+  namePatFind :: a -> NamePatFind
+  default namePatFind :: (Generic a, GAlpha (Rep a)) => a -> NamePatFind
+  namePatFind = gnamePatFind . from
+
+  -- | See 'Unbound.Generics.LocallyNameless.Operations.swaps'. Apply
+  -- the given permutation of variable names to the given pattern.
+  swaps' :: AlphaCtx -> Perm AnyName -> a -> a
+  default swaps' :: (Generic a, GAlpha (Rep a)) => AlphaCtx -> Perm AnyName -> a -> a
+  swaps' ctx perm = to . gswaps ctx perm . from
+
+  -- | See 'Unbound.Generics.LocallyNameless.Operations.freshen'.
+  lfreshen' :: LFresh m => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b
+  default lfreshen' :: (LFresh m, Generic a, GAlpha (Rep a))
+                       => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b
+  lfreshen' ctx m cont = glfreshen ctx (from m) (cont . to)
+
+  -- | See 'Unbound.Generics.LocallyNameless.Operations.freshen'.  Rename the free variables
+  -- in the given term to be distinct from all other names seen in the monad @m@.
+  freshen' :: Fresh m => AlphaCtx -> a -> m (a, Perm AnyName)
+  default freshen'  :: (Generic a, GAlpha (Rep a), Fresh m) => AlphaCtx -> a -> m (a, Perm AnyName)
+  freshen' ctx = liftM (first to) . gfreshen ctx . from
+
+-- | The result of @'nthPatFind' a i@ is @Left k@ where @k@ is the
+-- number of names in pattern @a@ with @k < i@ or @Right x@ where @x@
+-- is the @i@th name in @a@
+type NthPatFind = Integer -> Either Integer AnyName
+
+-- | The result of @'namePatFind' a x@ is either @Left i@ if @a@ is a pattern that
+-- contains @i@ free names none of which are @x@, or @Right j@ if @x@ is the @j@th name
+-- in @a@
+type NamePatFind = AnyName -> Either Integer Integer -- Left - names skipped over
+                                                     -- Right - index of the name we found
+
+-- | The "Generic" representation version of 'Alpha'
+class GAlpha f where
+  gaeq :: AlphaCtx -> f a -> f a -> Bool
+
+  gfvAny :: (Contravariant g, Applicative g) => AlphaCtx -> (AnyName -> g AnyName) -> f a -> g (f a)
+
+  gclose :: Alpha b => AlphaCtx -> b -> f a -> f a
+  gopen :: Alpha b => AlphaCtx -> b -> f a -> f a
+
+  gisPat :: f a -> DisjointSet AnyName
+  gisTerm :: f a -> Bool
+
+  gnthPatFind :: f a -> NthPatFind
+  gnamePatFind :: f a -> NamePatFind
+
+  gswaps :: AlphaCtx -> Perm AnyName -> f a -> f a
+  gfreshen :: Fresh m => AlphaCtx -> f a -> m (f a, Perm AnyName)
+
+  glfreshen :: LFresh m => AlphaCtx -> f a -> (f a -> Perm AnyName -> m b) -> m b
+  
+instance (Alpha c) => GAlpha (K1 i c) where
+  gaeq ctx (K1 c1) (K1 c2) = aeq' ctx c1 c2
+
+  gfvAny ctx nfn = fmap K1 . fvAny' ctx nfn . unK1
+
+  gclose ctx b = K1 . close ctx b . unK1
+  gopen ctx b = K1 . open ctx b . unK1
+
+  gisPat = isPat . unK1
+  gisTerm = isTerm . unK1
+
+  gnthPatFind = nthPatFind . unK1
+  gnamePatFind = namePatFind . unK1
+
+  gswaps ctx perm = K1 . swaps' ctx perm . unK1
+  gfreshen ctx = liftM (first K1) . freshen' ctx . unK1
+
+  glfreshen ctx (K1 c) cont = lfreshen' ctx c (cont . K1)
+
+instance GAlpha f => GAlpha (M1 i c f) where
+  gaeq ctx (M1 f1) (M1 f2) = gaeq ctx f1 f2
+
+  gfvAny ctx nfn = fmap M1 . gfvAny ctx nfn . unM1
+
+  gclose ctx b = M1 . gclose ctx b . unM1
+  gopen ctx b = M1 . gopen ctx b . unM1
+
+  gisPat = gisPat . unM1
+  gisTerm = gisTerm . unM1
+
+  gnthPatFind = gnthPatFind . unM1
+  gnamePatFind = gnamePatFind . unM1
+  
+  gswaps ctx perm = M1 . gswaps ctx perm . unM1
+  gfreshen ctx = liftM (first M1) . gfreshen ctx . unM1
+
+  glfreshen ctx (M1 f) cont =
+    glfreshen ctx f (cont . M1)
+
+instance GAlpha U1 where
+  gaeq _ctx _ _ = True
+
+  gfvAny _ctx _nfn _ = pure U1
+
+  gclose _ctx _b _ = U1
+  gopen _ctx _b _ = U1
+
+  gisPat _ = mempty
+  gisTerm _ = True
+
+  gnthPatFind _ = Left
+  gnamePatFind _ _ = Left 0
+
+  gswaps _ctx _perm _ = U1
+  gfreshen _ctx _ = return (U1, mempty)
+
+  glfreshen _ctx _ cont = cont U1 mempty
+
+instance GAlpha V1 where
+  gaeq _ctx _ _ = False
+
+  gfvAny _ctx _nfn = pure
+
+  gclose _ctx _b _ = undefined
+  gopen _ctx _b _ = undefined
+
+  gisPat _ = mempty
+  gisTerm _ = False
+
+  gnthPatFind _ = Left
+  gnamePatFind _ _ = Left 0
+
+  gswaps _ctx _perm _ = undefined
+  gfreshen _ctx _ = return (undefined, mempty)
+
+  glfreshen _ctx _ cont = cont undefined mempty
+
+instance (GAlpha f, GAlpha g) => GAlpha (f :*: g) where
+  gaeq ctx (f1 :*: g1) (f2 :*: g2) =
+    gaeq ctx f1 f2 && gaeq ctx g1 g2
+
+  gfvAny ctx nfn (f :*: g) = (:*:) <$> gfvAny ctx nfn f
+                                   <*> gfvAny ctx nfn g
+
+  gclose ctx b (f :*: g) = gclose ctx b f :*: gclose ctx b g
+  gopen ctx b (f :*: g) = gopen ctx b f :*: gopen ctx b g
+
+  gisPat (f :*: g) = gisPat f <> gisPat g
+  gisTerm (f :*: g) = gisTerm f && gisTerm g
+
+  gnthPatFind (f :*: g) i = case gnthPatFind f i of
+    Left i' -> gnthPatFind g i'
+    Right ans -> Right ans
+  gnamePatFind (f :*: g) n = case gnamePatFind f n of
+    Left j -> case gnamePatFind g n of
+      Left i -> Left $! j + i
+      Right k -> Right $! j + k
+    Right k -> Right k
+
+  gswaps ctx perm (f :*: g) =
+    gswaps ctx perm f :*: gswaps ctx perm g
+
+  gfreshen ctx (f :*: g) = do
+    (g', perm2) <- gfreshen ctx g
+    (f', perm1) <- gfreshen ctx (gswaps ctx perm2 f)
+    return (f' :*: g', perm1 <> perm2)
+
+  glfreshen ctx (f :*: g) cont =
+    glfreshen ctx g $ \g' perm2 ->
+    glfreshen ctx (gswaps ctx perm2 f) $ \f' perm1 ->
+    cont (f' :*: g') (perm1 <> perm2)
+
+instance (GAlpha f, GAlpha g) => GAlpha (f :+: g) where
+  gaeq ctx  (L1 f1) (L1 f2) = gaeq ctx f1 f2
+  gaeq ctx  (R1 g1) (R1 g2) = gaeq ctx g1 g2
+  gaeq _ctx _       _       = False
+
+  gfvAny ctx nfn (L1 f) = fmap L1 (gfvAny ctx nfn f)
+  gfvAny ctx nfn (R1 g) = fmap R1 (gfvAny ctx nfn g)
+
+  gclose ctx b (L1 f) = L1 (gclose ctx b f)
+  gclose ctx b (R1 g) = R1 (gclose ctx b g)
+  gopen ctx b (L1 f) = L1 (gopen ctx b f)
+  gopen ctx b (R1 g) = R1 (gopen ctx b g)
+
+  gisPat (L1 f) = gisPat f
+  gisPat (R1 g) = gisPat g
+
+  gisTerm (L1 f) = gisTerm f
+  gisTerm (R1 g) = gisTerm g
+
+  gnthPatFind (L1 f) i = gnthPatFind f i
+  gnthPatFind (R1 g) i = gnthPatFind g i
+  
+  gnamePatFind (L1 f) n = gnamePatFind f n
+  gnamePatFind (R1 g) n = gnamePatFind g n
+
+  gswaps ctx perm (L1 f) = L1 (gswaps ctx perm f)
+  gswaps ctx perm (R1 f) = R1 (gswaps ctx perm f)
+
+  gfreshen ctx (L1 f) = liftM (first L1) (gfreshen ctx f)
+  gfreshen ctx (R1 f) = liftM (first R1) (gfreshen ctx f)
+  
+  glfreshen ctx (L1 f) cont =
+    glfreshen ctx f (cont . L1)
+  glfreshen ctx (R1 g) cont =
+    glfreshen ctx g (cont . R1)
+  
+
+-- ============================================================
+-- Alpha instances for the usual types
+
+instance Alpha Int where
+  aeq' _ctx i j = i == j
+
+  fvAny' _ctx _nfn i = pure i
+
+  close _ctx _b i = i
+  open _ctx _b i = i
+
+  isPat _ = mempty
+  isTerm _ = True
+
+  nthPatFind _ = Left
+  namePatFind _ _ = Left 0
+
+  swaps' _ctx _p i = i
+  freshen' _ctx i = return (i, mempty)
+  lfreshen' _ctx i cont = cont i mempty
+
+instance Alpha Char where
+  aeq' _ctx i j = i == j
+
+  fvAny' _ctx _nfn i = pure i
+
+  close _ctx _b i = i
+  open _ctx _b i = i
+
+  isPat _ = mempty
+  isTerm _ = True
+
+  nthPatFind _ = Left
+  namePatFind _ _ = Left 0
+
+  swaps' _ctx _p i = i
+  freshen' _ctx i = return (i, mempty)
+  lfreshen' _ctx i cont = cont i mempty
+
+instance Alpha Integer where
+  aeq' _ctx i j = i == j
+
+  fvAny' _ctx _nfn i = pure i
+
+  close _ctx _b i = i
+  open _ctx _b i = i
+
+  isPat _ = mempty
+  isTerm _ = True
+
+  nthPatFind _ = Left
+  namePatFind _ _ = Left 0
+
+  swaps' _ctx _p i = i
+  freshen' _ctx i = return (i, mempty)
+  lfreshen' _ctx i cont = cont i mempty
+
+instance Alpha Float where
+  aeq' _ctx i j = i == j
+
+  fvAny' _ctx _nfn i = pure i
+
+  close _ctx _b i = i
+  open _ctx _b i = i
+
+  isPat _ = mempty
+  isTerm _ = True
+
+  nthPatFind _ = Left
+  namePatFind _ _ = Left 0
+
+  swaps' _ctx _p i = i
+  freshen' _ctx i = return (i, mempty)
+  lfreshen' _ctx i cont = cont i mempty
+
+instance Alpha Double where
+  aeq' _ctx i j = i == j
+
+  fvAny' _ctx _nfn i = pure i
+
+  close _ctx _b i = i
+  open _ctx _b i = i
+
+  isPat _ = mempty
+  isTerm _ = True
+
+  nthPatFind _ = Left
+  namePatFind _ _ = Left 0
+
+  swaps' _ctx _p i = i
+  freshen' _ctx i = return (i, mempty)
+  lfreshen' _ctx i cont = cont i mempty
+
+instance (Integral n, Alpha n) => Alpha (Ratio n) where
+  aeq' _ctx i j = i == j
+
+  fvAny' _ctx _nfn i = pure i
+
+  close _ctx _b i = i
+  open _ctx _b i = i
+
+  isPat _ = mempty
+  isTerm _ = True
+
+  nthPatFind _ = Left
+  namePatFind _ _ = Left 0
+
+  swaps' _ctx _p i = i
+  freshen' _ctx i = return (i, mempty)
+  lfreshen' _ctx i cont = cont i mempty
+
+instance Alpha Bool
+
+instance Alpha a => Alpha (Maybe a)
+instance Alpha a => Alpha [a]
+instance (Alpha a,Alpha b) => Alpha (Either a b)
+instance (Alpha a,Alpha b) => Alpha (a,b)
+instance (Alpha a,Alpha b,Alpha c) => Alpha (a,b,c)
+instance (Alpha a, Alpha b,Alpha c, Alpha d) => Alpha (a,b,c,d)
+instance (Alpha a, Alpha b,Alpha c, Alpha d, Alpha e) =>
+   Alpha (a,b,c,d,e)
+
+-- ============================================================
+-- Alpha instances for interesting types
+
+instance Typeable a => Alpha (Name a) where
+  aeq' ctx n1 n2 =
+    if isTermCtx ctx
+    then n1 == n2 -- in terms, better be the same name
+    else True     -- in a pattern, names are always equivlent (since
+                  -- they're both bound, so they can vary).
+
+  fvAny' ctx nfn nm = if isTermCtx ctx && isFreeName nm
+                      then contramap AnyName  (nfn (AnyName nm))
+                      else pure nm
+
+  open ctx b a@(Bn l k) =
+    if ctxMode ctx == Term && ctxLevel ctx == l
+    then case nthPatFind b k of
+      Right (AnyName nm) -> case gcast nm of
+        Just nm' -> nm'
+        Nothing -> error "LocallyNameless.open: inconsistent sorts"
+      Left _ -> error "LocallyNameless.open : inconsistency - pattern had too few variables"
+    else
+      a
+  open _ctx _ a = a
+
+  close ctx b a@(Fn _ _) =
+    if isTermCtx ctx
+    then case namePatFind b (AnyName a) of
+      Right k -> Bn (ctxLevel ctx) k
+      Left _ -> a
+    else a
+  close _ctx _ a = a
+  
+
+  isPat n = if isFreeName n
+            then singletonDisjointSet (AnyName n)
+            else inconsistentDisjointSet
+
+  isTerm _ = True
+
+  nthPatFind nm i =
+    if i == 0 then Right (AnyName nm) else Left $! i-1
+
+  namePatFind nm1 (AnyName nm2) =
+    case gcast nm1 of
+      Just nm1' -> if nm1' == nm2 then Right 0 else Left 1
+      Nothing -> Left 1
+
+  swaps' ctx perm nm =
+    if isTermCtx ctx
+    then case apply perm (AnyName nm) of
+      AnyName nm' ->
+        case gcast nm' of
+          Just nm'' -> nm''
+          Nothing -> error "Internal error swaps' on a Name returned permuted name of wrong sort"
+    else nm
+      
+  freshen' ctx nm =
+    if not (isTermCtx ctx)
+    then do
+      nm' <- fresh nm
+      return (nm', single (AnyName nm) (AnyName nm'))
+    else error "freshen' on a Name in term position"
+
+  lfreshen' ctx nm cont =
+    if not (isTermCtx ctx)
+    then do
+      nm' <- lfresh nm
+      avoid [AnyName nm'] $ cont nm' $ single (AnyName nm) (AnyName nm')
+    else error "lfreshen' on a Name in term position"
+
+instance Alpha AnyName where
+  aeq' ctx x y =
+    if x == y
+    then True
+    else
+      -- in a term unequal variables are unequal, in a pattern it's
+      -- ok.
+      not (isTermCtx ctx)
+
+  fvAny' ctx nfn n@(AnyName nm) = if isTermCtx ctx && isFreeName nm
+                                  then nfn n
+                                  else pure n
+
+  isTerm _ = True
+
+  isPat n@(AnyName nm) = if isFreeName nm
+                         then singletonDisjointSet n
+                         else inconsistentDisjointSet
+
+  swaps' ctx perm n =
+    if isTermCtx ctx
+    then apply perm n
+    else n
+
+  freshen' ctx (AnyName nm) =
+    if isTermCtx ctx
+    then error "LocallyNameless.freshen' on AnyName in Term mode"
+    else do
+      nm' <- fresh nm
+      return (AnyName nm', single (AnyName nm) (AnyName nm'))
+
+  lfreshen' ctx (AnyName nm) cont =
+    if isTermCtx ctx
+    then error "LocallyNameless.lfreshen' on AnyName in Term mode"
+    else do
+      nm' <- lfresh nm
+      avoid [AnyName nm'] $ cont (AnyName nm') $ single (AnyName nm) (AnyName nm')
+
+  open ctx b (AnyName nm) = AnyName (open ctx b nm)
+
+  close ctx b (AnyName nm) = AnyName (close ctx b nm)
+    
+  nthPatFind nm i =
+    if i == 0 then Right nm else Left $! i - 1
+
+  namePatFind nmHave nmWant =
+    if nmHave == nmWant
+    then Right 0
+    else Left 1
diff --git a/src/Unbound/Generics/LocallyNameless/Bind.hs b/src/Unbound/Generics/LocallyNameless/Bind.hs
new file mode 100644
--- /dev/null
+++ b/src/Unbound/Generics/LocallyNameless/Bind.hs
@@ -0,0 +1,77 @@
+{-# OPTIONS_HADDOCK show-extensions #-}
+-- |
+-- Module     : Unbound.Generics.LocallyNameless.Bind
+-- Copyright  : (c) 2014, Aleksey Kliger
+-- License    : BSD3 (See LICENSE)
+-- Maintainer : Aleksey Kliger
+-- Stability  : experimental
+--
+-- The fundamental binding form.  The type @'Bind' p t@ allows you to
+-- place a pattern @p@ in a term @t@ such that the names in the
+-- pattern scope over the term.  Use 'Unbound.Generics.LocallyNameless.Operations.bind'
+-- and 'Unbound.Generics.LocallyNameless.Operations.unbind' and 'Unbound.Generics.LocallyNameless.Operations.lunbind'
+-- to work with @'Bind' p t@
+{-# LANGUAGE DeriveGeneric #-}
+module Unbound.Generics.LocallyNameless.Bind (
+  -- * Name binding
+  Bind(..)
+  ) where
+
+import Control.Applicative (Applicative(..), (<$>))
+import Data.Monoid ((<>))
+
+import GHC.Generics (Generic)
+
+import Unbound.Generics.LocallyNameless.Alpha
+
+-- | A term of type @'Bind' p t@ is a term that binds the free
+-- variable occurrences of the variables in pattern @p@ in the term
+-- @t@.  In the overall term, those variables are now bound. See also
+-- 'Unbound.Generics.LocallyNameless.Operations.bind' and
+-- 'Unbound.Generics.LocallyNameless.Operations.unbind' and
+-- 'Unbound.Generics.LocallyNameless.Operations.lunbind'
+data Bind p t = B p t
+              deriving (Generic)
+
+instance (Show p, Show t) => Show (Bind p t) where
+  showsPrec prec (B p t) =
+    showParen (prec > 0) (showString "<"
+                          . showsPrec prec p
+                          . showString "> "
+                          . showsPrec 0 t)
+
+instance (Alpha p, Alpha t) => Alpha (Bind p t) where
+
+  aeq' ctx (B p1 t1) (B p2 t2) =
+    aeq' (patternCtx ctx) p1 p2
+    && aeq' (incrLevelCtx ctx) t1 t2
+
+  fvAny' ctx nfn (B p t) = B <$> fvAny' (patternCtx ctx) nfn p
+                             <*> fvAny' (incrLevelCtx ctx) nfn t
+
+  isPat _ = inconsistentDisjointSet
+
+  isTerm (B p t) = isConsistentDisjointSet (isPat p) && isTerm t
+
+  close ctx b (B p t) =
+    B (close (patternCtx ctx) b p) (close (incrLevelCtx ctx) b t)
+
+  open ctx b (B p t) =
+    B (open (patternCtx ctx) b p) (open (incrLevelCtx ctx) b t)
+
+  nthPatFind b = error $ "Binding " ++ show b ++ " used as a pattern"
+  namePatFind b = error $ "Binding " ++ show b ++ " used as a pattern"
+
+  swaps' ctx perm (B p t) =
+    B (swaps' (patternCtx ctx) perm p)
+      (swaps' (incrLevelCtx ctx) perm t)
+
+  freshen' ctx (B p t) = do
+    (p', perm1) <- freshen' (patternCtx ctx) p
+    (t', perm2) <- freshen' (incrLevelCtx ctx) (swaps' (incrLevelCtx ctx) perm1 t)
+    return (B p' t', perm1 <> perm2)
+
+  lfreshen' ctx (B p t) cont =
+    lfreshen' (patternCtx ctx) p $ \p' pm1 ->
+    lfreshen' (incrLevelCtx ctx) (swaps' (incrLevelCtx ctx) pm1 t) $ \t' pm2 ->
+    cont (B p' t') (pm1 <> pm2)
diff --git a/src/Unbound/Generics/LocallyNameless/Embed.hs b/src/Unbound/Generics/LocallyNameless/Embed.hs
new file mode 100644
--- /dev/null
+++ b/src/Unbound/Generics/LocallyNameless/Embed.hs
@@ -0,0 +1,77 @@
+{-# OPTIONS_HADDOCK show-extensions #-}
+-- |
+-- Module     : Unbound.Generics.LocallyNameless.Embed
+-- Copyright  : (c) 2014, Aleksey Kliger
+-- License    : BSD3 (See LICENSE)
+-- Maintainer : Aleksey Kliger
+-- Stability  : experimental
+--
+-- The pattern @'Embed' t@ contains a term @t@.
+{-# LANGUAGE DeriveGeneric #-}
+module Unbound.Generics.LocallyNameless.Embed where
+
+import Control.Applicative (pure, (<$>))
+import Data.Monoid (mempty)
+import GHC.Generics (Generic)
+
+import Unbound.Generics.LocallyNameless.Alpha
+
+-- | @Embed@ allows for terms to be /embedded/ within patterns.  Such
+--   embedded terms do not bind names along with the rest of the
+--   pattern.  For examples, see the tutorial or examples directories.
+--
+--   If @t@ is a /term type/, then @Embed t@ is a /pattern type/.
+--
+--   @Embed@ is not abstract since it involves no binding, and hence
+--   it is safe to manipulate directly.  To create and destruct
+--   @Embed@ terms, you may use the @Embed@ constructor directly.
+--   (You may also use the functions 'embed' and 'unembed', which
+--   additionally can construct or destruct any number of enclosing
+--   'Shift's at the same time.)
+newtype Embed t = Embed t deriving (Eq, Generic)
+
+instance Show a => Show (Embed a) where
+  showsPrec _ (Embed a) = showString "{" . showsPrec 0 a . showString "}"
+
+instance Alpha t => Alpha (Embed t) where
+  isPat (Embed t) = if (isTerm t) then mempty else inconsistentDisjointSet
+
+  isTerm _ = False
+
+  isEmbed (Embed t) = isTerm t
+
+  swaps' ctx perm (Embed t) =
+    if isTermCtx ctx
+    then Embed t
+    else Embed (swaps' (termCtx ctx) perm t)
+
+  freshen' ctx p =
+    if isTermCtx ctx
+    then error "LocallyNameless.freshen' called on a term"
+    else return (p, mempty)
+
+  lfreshen' ctx p cont =
+    if isTermCtx ctx
+    then error "LocallyNameless.lfreshen' called on a term"
+    else cont p mempty
+
+
+  aeq' ctx (Embed x) (Embed y) = aeq' (termCtx ctx) x y
+
+  fvAny' ctx afa ex@(Embed x) =
+    if isTermCtx ctx
+    then pure ex
+    else Embed <$> fvAny' (termCtx ctx) afa x
+
+  close ctx b (Embed x) =
+    if isTermCtx ctx
+    then error "LocallyNameless.close on Embed"
+    else Embed (close (termCtx ctx) b x)
+
+  open ctx b (Embed x) =
+    if isTermCtx ctx
+    then error "LocallyNameless.open on Embed"
+    else Embed (open (termCtx ctx) b x)
+
+  nthPatFind _ = Left
+  namePatFind _ _ = Left 0
diff --git a/src/Unbound/Generics/LocallyNameless/Fresh.hs b/src/Unbound/Generics/LocallyNameless/Fresh.hs
new file mode 100644
--- /dev/null
+++ b/src/Unbound/Generics/LocallyNameless/Fresh.hs
@@ -0,0 +1,140 @@
+-- |
+-- Module     : Unbound.Generics.LocallyNameless.Fresh
+-- Copyright  : (c) 2014, Aleksey Kliger
+-- License    : BSD3 (See LICENSE)
+-- Maintainer : Aleksey Kliger
+-- Stability  : experimental
+--
+-- Global freshness monad.
+{-# LANGUAGE CPP, GeneralizedNewtypeDeriving,
+             FlexibleInstances, MultiParamTypeClasses,
+             UndecidableInstances
+  #-}
+-- (we expect deprecation warnings about Control.Monad.Trans.Error)
+{-# OPTIONS_GHC -Wwarn #-}
+module Unbound.Generics.LocallyNameless.Fresh where
+
+import Control.Applicative (Applicative, Alternative)
+import Control.Monad ()
+
+import Control.Monad.Identity
+
+import Control.Monad.Trans
+#if MIN_VERSION_transformers(0,4,0)
+import Control.Monad.Trans.Except
+#endif
+import Control.Monad.Trans.Error
+import Control.Monad.Trans.Maybe
+import Control.Monad.Trans.Reader
+import Control.Monad.Trans.State.Lazy as Lazy
+import Control.Monad.Trans.State.Strict as Strict
+import Control.Monad.Trans.Writer.Lazy as Lazy
+import Control.Monad.Trans.Writer.Strict as Strict
+
+import qualified Control.Monad.Cont.Class as CC
+import qualified Control.Monad.Error.Class as EC
+import qualified Control.Monad.State.Class as StC
+import qualified Control.Monad.Reader.Class as RC
+import qualified Control.Monad.Writer.Class as WC
+
+import Data.Monoid (Monoid)
+
+import qualified Control.Monad.State as St
+
+import Unbound.Generics.LocallyNameless.Name
+
+-- | The @Fresh@ type class governs monads which can generate new
+--   globally unique 'Name's based on a given 'Name'.
+class Monad m => Fresh m where
+
+  -- | Generate a new globally unique name based on the given one.
+  fresh :: Name a -> m (Name a)
+
+
+-- | The @FreshM@ monad transformer.  Keeps track of the lowest index
+--   still globally unused, and increments the index every time it is
+--   asked for a fresh name.
+newtype FreshMT m a = FreshMT { unFreshMT :: St.StateT Integer m a }
+  deriving (Functor, Applicative, Alternative, Monad, MonadPlus, MonadIO, MonadFix)
+
+-- | Run a 'FreshMT' computation (with the global index starting at zero).
+runFreshMT :: Monad m => FreshMT m a -> m a
+runFreshMT m = contFreshMT m 0
+
+-- | Run a 'FreshMT' computation given a starting index for fresh name
+--   generation.
+contFreshMT :: Monad m => FreshMT m a -> Integer -> m a
+contFreshMT (FreshMT m) = St.evalStateT m
+
+instance MonadTrans FreshMT where
+  lift = FreshMT . lift
+
+instance CC.MonadCont m => CC.MonadCont (FreshMT m) where
+  callCC c = FreshMT $ CC.callCC (unFreshMT . (\k -> c (FreshMT . k)))
+
+instance EC.MonadError e m => EC.MonadError e (FreshMT m) where
+  throwError = lift . EC.throwError
+  catchError m h = FreshMT $ EC.catchError (unFreshMT m) (unFreshMT . h)
+
+instance StC.MonadState s m => StC.MonadState s (FreshMT m) where
+  get = lift StC.get
+  put = lift . StC.put
+
+instance RC.MonadReader r m => RC.MonadReader r (FreshMT m) where
+  ask   = lift RC.ask
+  local f = FreshMT . RC.local f . unFreshMT
+
+instance WC.MonadWriter w m => WC.MonadWriter w (FreshMT m) where
+  tell   = lift . WC.tell
+  listen = FreshMT . WC.listen . unFreshMT
+  pass   = FreshMT . WC.pass . unFreshMT
+
+
+instance Monad m => Fresh (FreshMT m) where
+  fresh (Fn s _) = FreshMT $ do
+    n <- St.get
+    St.put $! n + 1
+    return $ (Fn s n)
+  fresh nm@(Bn {}) = return nm
+
+instance (Error e, Fresh m) => Fresh (ErrorT e m) where
+  fresh = lift . fresh
+
+#if MIN_VERSION_transformers(0,4,0)
+instance Fresh m => Fresh (ExceptT e m) where
+  fresh = lift . fresh
+#endif
+
+instance Fresh m => Fresh (MaybeT m) where
+  fresh = lift . fresh
+
+instance Fresh m => Fresh (ReaderT r m) where
+  fresh = lift . fresh
+
+instance Fresh m => Fresh (Lazy.StateT s m) where
+  fresh = lift . fresh
+
+instance Fresh m => Fresh (Strict.StateT s m) where
+  fresh = lift . fresh
+
+instance (Monoid w, Fresh m) => Fresh (Lazy.WriterT w m) where
+  fresh = lift . fresh
+
+instance (Monoid w, Fresh m) => Fresh (Strict.WriterT w m) where
+  fresh = lift . fresh
+
+------------------------------------------------------------
+-- FreshM monad
+
+-- | A convenient monad which is an instance of 'Fresh'.  It keeps
+--   track of a global index used for generating fresh names, which is
+--   incremented every time 'fresh' is called.
+type FreshM = FreshMT Identity
+
+-- | Run a FreshM computation (with the global index starting at zero).
+runFreshM :: FreshM a -> a
+runFreshM = runIdentity . runFreshMT
+
+-- | Run a FreshM computation given a starting index.
+contFreshM :: FreshM a -> Integer -> a
+contFreshM m = runIdentity . contFreshMT m
diff --git a/src/Unbound/Generics/LocallyNameless/Internal/Fold.hs b/src/Unbound/Generics/LocallyNameless/Internal/Fold.hs
new file mode 100644
--- /dev/null
+++ b/src/Unbound/Generics/LocallyNameless/Internal/Fold.hs
@@ -0,0 +1,44 @@
+-- |
+-- Module     : Unbound.Generics.LocallyNameless.Internal.Fold
+-- Copyright  : (c) 2014, Aleksey Kliger
+-- License    : BSD3 (See LICENSE)
+-- Maintainer : Aleksey Kliger
+-- Stability  : experimental
+--
+-- | Some utilities for working with Folds.
+{-# LANGUAGE RankNTypes #-}
+module Unbound.Generics.LocallyNameless.Internal.Fold (Fold, Traversal', toListOf, filtered, justFiltered) where
+
+import Control.Applicative
+import Data.Maybe (fromJust)
+import Data.Functor.Contravariant
+import Data.Monoid
+
+type Getting r s a = (a -> Const r a) -> s -> Const r s
+
+type Fold s a = forall f . (Contravariant f, Applicative f) => (a -> f a) -> s -> f s
+
+type Traversal' s a = forall f . Applicative f => (a -> f a) -> s -> f s
+
+toListOf :: Fold s a -> s -> [a]
+-- toListOf :: Getting (Endo [a]) s a -> s -> [a]
+toListOf l = foldrOf l (:) []
+{-# INLINE toListOf #-}
+
+foldMapOf :: Getting r s a -> (a -> r) -> s -> r
+foldMapOf l f = getConst . l (Const . f)
+{-# INLINE foldMapOf #-}
+
+foldrOf :: Getting (Endo r) s a -> (a -> r -> r) -> r -> s -> r
+foldrOf l f z = fmap (flip appEndo z) (foldMapOf l (Endo .f))
+{-# INLINE foldrOf #-}
+
+filtered :: (a -> Bool) -> Traversal' a a
+filtered p afa x = if p x then afa x else pure x
+{-# INLINE filtered #-}
+
+justFiltered :: (a -> Maybe b) -> Fold a b
+justFiltered p bfb x = case p x of
+                        Just b -> contramap (fromJust . p) (bfb b)
+                        Nothing -> pure x
+{-# INLINE justFiltered #-}
diff --git a/src/Unbound/Generics/LocallyNameless/LFresh.hs b/src/Unbound/Generics/LocallyNameless/LFresh.hs
new file mode 100644
--- /dev/null
+++ b/src/Unbound/Generics/LocallyNameless/LFresh.hs
@@ -0,0 +1,220 @@
+{-# OPTIONS_HADDOCK show-extensions #-}
+-- |
+-- Module     : Unbound.Generics.LocallyNameless.LFresh
+-- Copyright  : (c) 2011, Stephanie Weirich
+-- License    : BSD3 (See LFresh.hs)
+-- Maintainer : Aleksey Kliger
+-- Stability  : experimental
+--
+-- Local freshness monad.
+{-
+Copyright (c)2011, Stephanie Weirich
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Stephanie Weirich nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+-}
+-- we expect deprecation warnings about Control.Monad.Trans.Error
+{-# OPTIONS_GHC -Wwarn #-}
+{-# LANGUAGE CPP
+             , GeneralizedNewtypeDeriving
+             , FlexibleInstances
+             , MultiParamTypeClasses
+             , UndecidableInstances #-}
+module Unbound.Generics.LocallyNameless.LFresh
+       (
+         -- * The 'LFresh' class
+
+         LFresh(..),
+
+         LFreshM, runLFreshM, contLFreshM,
+         LFreshMT(..), runLFreshMT, contLFreshMT
+
+       ) where
+
+import Data.Set (Set)
+import qualified Data.Set as S
+
+import Data.Monoid
+import Data.Typeable (Typeable)
+
+import Control.Monad.Reader
+import Control.Monad.Identity
+import Control.Applicative (Applicative, Alternative)
+
+import Control.Monad.Trans.Cont
+import Control.Monad.Trans.Error
+#if MIN_VERSION_transformers(0,4,0)
+import Control.Monad.Trans.Except
+#endif
+import Control.Monad.Trans.Identity
+import Control.Monad.Trans.List
+import Control.Monad.Trans.Maybe
+import Control.Monad.Trans.State.Lazy as Lazy
+import Control.Monad.Trans.State.Strict as Strict
+import Control.Monad.Trans.Writer.Lazy as Lazy
+import Control.Monad.Trans.Writer.Strict as Strict
+
+import qualified Control.Monad.Cont.Class as CC
+import qualified Control.Monad.Error.Class as EC
+import qualified Control.Monad.State.Class as StC
+import qualified Control.Monad.Reader.Class as RC
+import qualified Control.Monad.Writer.Class as WC
+
+import Unbound.Generics.LocallyNameless.Name
+
+-- | This is the class of monads that support freshness in an
+--   (implicit) local scope.  Generated names are fresh for the current
+--   local scope, not necessarily globally fresh.
+class Monad m => LFresh m where
+  -- | Pick a new name that is fresh for the current (implicit) scope.
+  lfresh  :: Typeable a => Name a -> m (Name a)
+  -- | Avoid the given names when freshening in the subcomputation,
+  --   that is, add the given names to the in-scope set.
+  avoid   :: [AnyName] -> m a -> m a
+  -- | Get the set of names currently being avoided.
+  getAvoids :: m (Set AnyName)
+
+-- | The LFresh monad transformer.  Keeps track of a set of names to
+-- avoid, and when asked for a fresh one will choose the first numeric
+-- prefix of the given name which is currently unused.
+newtype LFreshMT m a = LFreshMT { unLFreshMT :: ReaderT (Set AnyName) m a }
+  deriving (Functor, Applicative, Alternative, Monad, MonadIO, MonadPlus, MonadFix)
+
+-- | Run an 'LFreshMT' computation in an empty context.
+runLFreshMT :: LFreshMT m a -> m a
+runLFreshMT m = contLFreshMT m S.empty
+
+-- | Run an 'LFreshMT' computation given a set of names to avoid.
+contLFreshMT :: LFreshMT m a -> Set AnyName -> m a
+contLFreshMT (LFreshMT m) = runReaderT m
+
+instance Monad m => LFresh (LFreshMT m) where
+  lfresh nm = LFreshMT $ do
+    let s = name2String nm
+    used <- ask
+    return $ head (filter (\x -> not (S.member (AnyName x) used))
+                          (map (makeName s) [0..]))
+  avoid names = LFreshMT . local (S.union (S.fromList names)) . unLFreshMT
+
+  getAvoids = LFreshMT ask
+
+-- | A convenient monad which is an instance of 'LFresh'.  It keeps
+--   track of a set of names to avoid, and when asked for a fresh one
+--   will choose the first unused numerical name.
+type LFreshM = LFreshMT Identity
+
+-- | Run a LFreshM computation in an empty context.
+runLFreshM :: LFreshM a -> a
+runLFreshM = runIdentity . runLFreshMT
+
+-- | Run a LFreshM computation given a set of names to avoid.
+contLFreshM :: LFreshM a -> Set AnyName -> a
+contLFreshM m = runIdentity . contLFreshMT m
+
+instance LFresh m => LFresh (ContT r m) where
+  lfresh = lift . lfresh
+  avoid  = mapContT . avoid
+  getAvoids = lift getAvoids
+
+instance (Error e, LFresh m) => LFresh (ErrorT e m) where
+  lfresh = lift . lfresh
+  avoid  = mapErrorT . avoid
+  getAvoids = lift getAvoids
+
+#if MIN_VERSION_transformers(0,4,0)
+instance LFresh m => LFresh (ExceptT e m) where
+  lfresh = lift . lfresh
+  avoid = mapExceptT . avoid
+  getAvoids = lift getAvoids
+#endif
+
+instance LFresh m => LFresh (IdentityT m) where
+  lfresh = lift . lfresh
+  avoid  = mapIdentityT . avoid
+  getAvoids = lift getAvoids
+
+instance LFresh m => LFresh (ListT m) where
+  lfresh = lift . lfresh
+  avoid  = mapListT . avoid
+  getAvoids = lift getAvoids
+
+instance LFresh m => LFresh (MaybeT m) where
+  lfresh = lift . lfresh
+  avoid  = mapMaybeT . avoid
+  getAvoids = lift getAvoids
+
+instance LFresh m => LFresh (ReaderT r m) where
+  lfresh = lift . lfresh
+  avoid  = mapReaderT . avoid
+  getAvoids = lift getAvoids
+
+instance LFresh m => LFresh (Lazy.StateT s m) where
+  lfresh = lift . lfresh
+  avoid  = Lazy.mapStateT . avoid
+  getAvoids = lift getAvoids
+
+instance LFresh m => LFresh (Strict.StateT s m) where
+  lfresh = lift . lfresh
+  avoid  = Strict.mapStateT . avoid
+  getAvoids = lift getAvoids
+
+instance (Monoid w, LFresh m) => LFresh (Lazy.WriterT w m) where
+  lfresh = lift . lfresh
+  avoid  = Lazy.mapWriterT . avoid
+  getAvoids = lift getAvoids
+
+instance (Monoid w, LFresh m) => LFresh (Strict.WriterT w m) where
+  lfresh = lift . lfresh
+  avoid  = Strict.mapWriterT . avoid
+  getAvoids = lift getAvoids
+
+-- Instances for applying LFreshMT to other monads
+
+instance MonadTrans LFreshMT where
+  lift = LFreshMT . lift
+
+instance CC.MonadCont m => CC.MonadCont (LFreshMT m) where
+  callCC c = LFreshMT $ CC.callCC (unLFreshMT . (\k -> c (LFreshMT . k)))
+
+instance EC.MonadError e m => EC.MonadError e (LFreshMT m) where
+  throwError = lift . EC.throwError
+  catchError m h = LFreshMT $ EC.catchError (unLFreshMT m) (unLFreshMT . h)
+
+instance StC.MonadState s m => StC.MonadState s (LFreshMT m) where
+  get = lift StC.get
+  put = lift . StC.put
+
+instance RC.MonadReader r m => RC.MonadReader r (LFreshMT m) where
+  ask   = lift RC.ask
+  local f = LFreshMT . mapReaderT (RC.local f) . unLFreshMT
+
+instance WC.MonadWriter w m => WC.MonadWriter w (LFreshMT m) where
+  tell   = lift . WC.tell
+  listen = LFreshMT . WC.listen . unLFreshMT
+  pass   = LFreshMT . WC.pass . unLFreshMT
diff --git a/src/Unbound/Generics/LocallyNameless/Name.hs b/src/Unbound/Generics/LocallyNameless/Name.hs
new file mode 100644
--- /dev/null
+++ b/src/Unbound/Generics/LocallyNameless/Name.hs
@@ -0,0 +1,96 @@
+-- |
+-- Module     : Unbound.Generics.LocallyNameless.Name
+-- Copyright  : (c) 2014, Aleksey Kliger
+-- License    : BSD3 (See LICENSE)
+-- Maintainer : Aleksey Kliger
+-- Stability  : experimental
+--
+-- Names stand for values.  They may be bound or free.
+{-# LANGUAGE DeriveDataTypeable
+             , DeriveGeneric
+             , ExistentialQuantification
+             , FlexibleContexts
+             , GADTs #-}
+module Unbound.Generics.LocallyNameless.Name
+       (
+         -- * Names over terms
+         Name(..)
+       , isFreeName
+         -- * Name construction
+       , string2Name
+       , s2n
+       , makeName
+         -- * Name inspection
+       , name2String
+         -- * Heterogeneous names
+       , AnyName(..)
+       ) where
+
+import Data.Typeable (Typeable, gcast, typeOf)
+import GHC.Generics (Generic)
+
+-- | An abstract datatype of names @Name a@ that stand for terms of
+-- type @a@.  The type @a@ is used as a tag to distinguish these names
+-- from names that may stand for other sorts of terms.
+--
+-- Two names in a term are consider
+-- 'Unbound.Generics.LocallyNameless.Operations.aeq' equal when they
+-- are the same name (in the sense of '(==)').  In patterns, however,
+-- any two names are equal if they occur in the same place within the
+-- pattern.  This induces alpha equivalence on terms in general.
+--
+-- Names may either be free or bound (see 'isFreeName').  Free names
+-- may be extracted from patterns using
+-- 'Unbound.Generics.LocallyNameless.Alpha.isPat'.  Bound names
+-- cannot be.
+-- 
+data Name a = Fn String !Integer    -- free names
+            | Bn !Integer !Integer  -- bound names / binding level + pattern index
+            deriving (Eq, Ord, Typeable, Generic)
+
+-- | Returns 'True' iff the given @Name a@ is free.
+isFreeName :: Name a -> Bool
+isFreeName (Fn _ _) = True
+isFreeName _ = False
+
+-- | Make a free 'Name a' from a 'String'
+string2Name :: String -> Name a
+string2Name s = makeName s 0
+
+-- | Synonym for 'string2Name'.
+s2n :: String -> Name a
+s2n = string2Name
+
+-- | Make a name from a 'String' and an 'Integer' index
+makeName :: String -> Integer -> Name a
+makeName = Fn
+
+-- | Get the string part of a 'Name'.
+name2String :: Name a -> String
+name2String (Fn s _) = s
+name2String (Bn _ _)   = error "Internal Error: cannot call name2Integer for bound names"
+
+instance Show (Name a) where
+  show (Fn "" n) = "_" ++ (show n)
+  show (Fn x 0) = x
+  show (Fn x n) = x ++ (show n)
+  show (Bn x y) = show x ++ "@" ++ show y
+
+-- | An @AnyName@ is a name that stands for a term of some (existentially hidden) type.
+data AnyName where
+  AnyName :: Typeable a => Name a -> AnyName
+
+instance Show AnyName where
+  show (AnyName nm) = show nm
+
+instance Eq AnyName where
+  (AnyName n1) == (AnyName n2) = case gcast n2 of
+    Just n2' -> n1 == n2'
+    Nothing -> False
+
+instance Ord AnyName where
+  compare (AnyName n1) (AnyName n2) = case compare (typeOf n1) (typeOf n2) of
+    EQ -> case gcast n2 of
+      Just n2' -> compare n1 n2'
+      Nothing -> error "Equal type representations, but gcast failed in comparing two AnyName values"
+    ord -> ord
diff --git a/src/Unbound/Generics/LocallyNameless/Operations.hs b/src/Unbound/Generics/LocallyNameless/Operations.hs
new file mode 100644
--- /dev/null
+++ b/src/Unbound/Generics/LocallyNameless/Operations.hs
@@ -0,0 +1,162 @@
+-- |
+-- Module     : Unbound.Generics.LocallyNameless.Operations
+-- Copyright  : (c) 2014, Aleksey Kliger
+-- License    : BSD3 (See LICENSE)
+-- Maintainer : Aleksey Kliger
+-- Stability  : experimental
+--
+-- Operations on terms and patterns that contain names.
+{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}
+module Unbound.Generics.LocallyNameless.Operations
+       (-- * Equivalence, free variables, freshness
+         aeq
+       , fvAny
+       , fv
+       , freshen
+       , lfreshen
+       , swaps
+         -- * Binding, unbinding
+       , Bind
+       , bind
+       , unbind
+       , lunbind
+       , unbind2
+       , unbind2Plus
+         -- * Rebinding, embedding
+       , Rebind
+       , rebind
+       , unrebind
+       , Embed(..)
+       , embed
+       , unembed
+       ) where
+
+import Control.Applicative (Applicative)
+import Control.Monad (MonadPlus(mzero))
+import Data.Functor.Contravariant (Contravariant)
+import Data.Monoid ((<>))
+import Data.Typeable (Typeable, cast)
+import Unbound.Generics.LocallyNameless.Alpha
+import Unbound.Generics.LocallyNameless.Fresh
+import Unbound.Generics.LocallyNameless.LFresh
+import Unbound.Generics.LocallyNameless.Name
+import Unbound.Generics.LocallyNameless.Bind
+import Unbound.Generics.LocallyNameless.Embed (Embed(..))
+import Unbound.Generics.LocallyNameless.Rebind
+import Unbound.Generics.LocallyNameless.Internal.Fold (toListOf, justFiltered)
+import Unbound.Generics.PermM
+
+-- | @'aeq' t1 t2@ returns @True@ iff @t1@ and @t2@ are alpha-equivalent terms.
+aeq :: Alpha a => a -> a -> Bool
+aeq = aeq' initialCtx
+
+-- | @'fvAny' t@ returns the free variables of the term @t@.
+--
+-- @
+--   fvAny :: Alpha a => a -> Fold a AnyName
+-- @
+fvAny :: (Alpha a, Contravariant f, Applicative f) => (AnyName -> f AnyName) -> a -> f a
+fvAny = fvAny' initialCtx
+
+-- | @'fv' t@ returns the free @b@ variables of term @t@.
+--
+-- @
+--  fv :: (Alpha a, Typeable b) => a -> Fold a (Name b)
+-- @
+fv :: forall a f b . (Alpha a, Typeable b, Contravariant f, Applicative f)
+      => (Name b -> f (Name b)) -> a -> f a
+fv = fvAny . justFiltered f
+  where f :: AnyName -> Maybe (Name b)
+        f (AnyName n) = cast n
+
+-- | Freshen a pattern by replacing all old binding 'Name's with new
+--   fresh 'Name's, returning a new pattern and a @'Perm' 'Name'@
+--   specifying how 'Name's were replaced.
+freshen :: (Alpha p, Fresh m) => p -> m (p, Perm AnyName)
+freshen = freshen' (patternCtx initialCtx)
+
+-- | \"Locally\" freshen a pattern, replacing all binding names with
+--   new names that are not already \"in scope\". The second argument
+--   is a continuation, which takes the renamed term and a permutation
+--   that specifies how the pattern has been renamed.  The resulting
+--   computation will be run with the in-scope set extended by the
+--   names just generated.
+lfreshen :: (Alpha p, LFresh m) => p -> (p -> Perm AnyName -> m b) -> m b
+lfreshen = lfreshen' (patternCtx initialCtx)
+
+-- | Apply the given permutation of variable names to the given term.
+swaps :: Alpha t => Perm AnyName -> t -> t
+swaps = swaps' initialCtx
+
+  
+-- | @'bind' p t@ closes over the variables of pattern @p@ in the term @t@
+bind :: (Alpha p, Alpha t) => p -> t -> Bind p t
+bind p t = B p (close initialCtx p t)
+
+-- | @'unbind' b@ lets you descend beneath a binder @b :: 'Bind' p t@
+-- by returning the pair of the pattern @p@ and the term @t@ where the
+-- variables in the pattern have been made globally fresh with respect
+-- to the freshness monad @m@.
+unbind :: (Alpha p, Alpha t, Fresh m) => Bind p t -> m (p, t)
+unbind (B p t) = do
+  (p', _) <- freshen p
+  return (p', open initialCtx p' t)
+
+-- | @lunbind@ opens a binding in an 'LFresh' monad, ensuring that the
+--   names chosen for the binders are /locally/ fresh.  The components
+--   of the binding are passed to a /continuation/, and the resulting
+--   monadic action is run in a context extended to avoid choosing new
+--   names which are the same as the ones chosen for this binding.
+--
+--   For more information, see the documentation for the 'LFresh' type
+--   class.
+lunbind :: (LFresh m, Alpha p, Alpha t) => Bind p t -> ((p, t) -> m c) -> m c
+lunbind (B p t) cont =
+  lfreshen p (\x _ -> cont (x, open initialCtx x t))
+
+
+-- | Simultaneously unbind two patterns in two terms, returning 'Nothing' if
+-- the two patterns don't bind the same number of variables.
+unbind2 :: (Fresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2)
+           => Bind p1 t1
+           -> Bind p2 t2
+           -> m (Maybe (p1, t1, p2, t2))
+unbind2 (B p1 t1) (B p2 t2) = do
+      case mkPerm (toListOf fvAny p2) (toListOf fvAny p1) of
+         Just pm -> do
+           (p1', pm') <- freshen p1
+           return $ Just (p1', open initialCtx p1' t1,
+                          swaps (pm' <> pm) p2, open initialCtx p1' t2)
+         Nothing -> return Nothing
+
+
+-- | Simultaneously unbind two patterns in two terms, returning 'mzero' if
+-- the patterns don't bind the same number of variables.
+unbind2Plus :: (MonadPlus m, Fresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2)
+         => Bind p1 t1
+         -> Bind p2 t2
+         -> m (p1, t1, p2, t2)
+unbind2Plus bnd bnd' = maybe mzero return =<< unbind2 bnd bnd'
+
+
+-- | @'rebind' p1 p2@ is a smart constructor for 'Rebind'.  It
+-- captures the variables of pattern @p1@ that occur within @p2@ in
+-- addition to providing binding occurrences for all the variables of @p1@ and @p2@
+rebind :: (Alpha p1, Alpha p2) => p1 -> p2 -> Rebind p1 p2
+rebind p1 p2 = Rebnd p1 (close (patternCtx initialCtx) p1 p2)
+
+-- | @'unrebind' p@ is the elimination form for 'Rebind'. It is not
+-- monadic (unlike 'unbind') because a @Rebind@ pattern can only occur
+-- somewhere in a pattern position of a 'Bind', and therefore 'unbind'
+-- must have already been called and all names apropriately
+-- 'freshen'ed.
+unrebind :: (Alpha p1, Alpha p2) => Rebind p1 p2 -> (p1, p2)
+unrebind (Rebnd p1 p2) = (p1, open (patternCtx initialCtx) p1 p2)
+
+-- | An alias for 'Embed'
+embed :: t -> Embed t
+embed = Embed
+
+-- | @'unembed' p@ extracts the term embedded in the pattern @p@.
+unembed :: Embed t -> t
+unembed (Embed t) = t
diff --git a/src/Unbound/Generics/LocallyNameless/Rebind.hs b/src/Unbound/Generics/LocallyNameless/Rebind.hs
new file mode 100644
--- /dev/null
+++ b/src/Unbound/Generics/LocallyNameless/Rebind.hs
@@ -0,0 +1,85 @@
+{-# OPTIONS_HADDOCK show-extensions #-}
+-- |
+-- Module     : Unbound.Generics.LocallyNameless.Rebind
+-- Copyright  : (c) 2014, Aleksey Kliger
+-- License    : BSD3 (See LICENSE)
+-- Maintainer : Aleksey Kliger
+-- Stability  : experimental
+--
+-- The pattern @'Rebind' p1 p2@ binds the names in @p1@ and @p2@ just as @(p1, p2)@ would,
+-- however it additionally also brings the names of @p1@ into scope in @p2@.
+--
+{-# LANGUAGE DeriveGeneric #-}
+module Unbound.Generics.LocallyNameless.Rebind where
+
+import Control.Applicative ((<*>), (<$>))
+import Data.Monoid ((<>))
+import GHC.Generics
+
+import Unbound.Generics.LocallyNameless.Alpha
+
+
+-- | @'Rebind' p1 p2@ is a pattern that binds the names of @p1@ and @p2@, and additionally
+-- brings the names of @p1@ into scope over @p2@.
+--
+-- This may be used, for example, to faithfully represent Scheme's @let*@ binding form, defined by:
+-- 
+-- >  (let* () body) ≙ body
+-- >  (let* ([v1, e1] binds ...) body) ≙ (let ([v1, e1]) (let* (binds ...) body))
+-- 
+-- using the following AST:
+--
+-- @
+-- type Var = Name Expr
+-- data Lets = EmptyLets
+--           | Bind (Rebind (Var, Embed Expr) Lets)
+-- data Expr = ...
+--           | LetStar { letStarBindings :: Lets
+--                     , letStarBody :: Expr
+--                     }
+--           | ...
+-- @
+data Rebind p1 p2 = Rebnd p1 p2
+                  deriving (Generic, Eq)
+
+instance (Show p1, Show p2) => Show (Rebind p1 p2) where
+  showsPrec paren (Rebnd p1 p2) =
+    showParen (paren > 0) (showString "<<"
+                           . showsPrec paren p1
+                           . showString ">> "
+                           . showsPrec 0 p2)
+
+instance (Alpha p1, Alpha p2) => Alpha (Rebind p1 p2) where
+  isTerm _ = False
+
+  isPat (Rebnd p1 p2) = isPat p1 <> isPat p2
+
+  swaps' ctx perm (Rebnd p1 p2) =
+    Rebnd (swaps' ctx perm p1) (swaps' (incrLevelCtx ctx) perm p2)
+
+  freshen' ctx (Rebnd p1 p2) =
+    if isTermCtx ctx
+    then error "freshen' on Rebind in Term mode"
+    else do
+      (p1', perm1) <- freshen' ctx p1
+      (p2', perm2) <- freshen' (incrLevelCtx ctx) (swaps' (incrLevelCtx ctx) perm1 p2)
+      return (Rebnd p1' p2', perm1 <> perm2)
+
+  lfreshen' ctx (Rebnd p q) cont =
+    if isTermCtx ctx
+    then error "lfreshen' on Rebind in Term mode"
+    else
+      lfreshen' ctx p $ \ p' pm1 ->
+      lfreshen' (incrLevelCtx ctx) (swaps' (incrLevelCtx ctx) pm1 q) $ \ q' pm2 ->
+      cont (Rebnd p' q') (pm1 <> pm2)
+
+
+  aeq' ctx (Rebnd p1 p2) (Rebnd q1 q2) =
+    -- XXX TODO: Unbound had (aeq' ctx p2 q2) here.  But that doesn't seem right.
+    aeq' ctx p1 q1 && aeq' (incrLevelCtx ctx) p2 q2
+
+  fvAny' ctx afa (Rebnd p1 p2) = Rebnd <$> fvAny' ctx afa p1
+                                       <*> fvAny' (incrLevelCtx ctx) afa p2
+
+  open ctx b (Rebnd p1 p2) = Rebnd (open ctx b p1) (open (incrLevelCtx ctx) b p2)
+  close ctx b (Rebnd p1 p2) = Rebnd (close ctx b p1) (close (incrLevelCtx ctx) b p2)
diff --git a/src/Unbound/Generics/LocallyNameless/Subst.hs b/src/Unbound/Generics/LocallyNameless/Subst.hs
new file mode 100644
--- /dev/null
+++ b/src/Unbound/Generics/LocallyNameless/Subst.hs
@@ -0,0 +1,177 @@
+-- |
+-- Module     : Unbound.Generics.LocallyNameless.Subst
+-- Copyright  : (c) 2014, Aleksey Kliger
+-- License    : BSD3 (See LICENSE)
+-- Maintainer : Aleksey Kliger
+-- Stability  : experimental
+--
+-- A typeclass for types that may participate in capture-avoiding substitution
+--
+-- The minimal definition is empty, provided your type is an instance of 'GHC.Generics.Generic'
+-- 
+-- @
+-- type Var = Name Factor
+-- data Expr = SumOf [Summand]
+--           deriving (Show, Generic)
+-- data Summand = ProductOf [Factor]
+--           deriving (Show, Generic)
+-- instance Subst Var Expr
+-- instance Subst Var Summand
+-- @
+-- 
+-- The default instance just propagates the substitution into the constituent factors.
+-- 
+-- If you identify the variable occurrences by implementing the 'isvar' function, the derived 'subst' function
+-- will be able to substitute a factor for a variable.
+-- 
+-- @
+-- data Factor = V Var
+--             | C Int
+--             | Subexpr Expr
+--           deriving (Show, Generic)
+-- instance Subst Var Factor where
+--   isvar (V v) = Just (SubstName v)
+--   isvar _     = Nothing
+-- @
+--
+{-# LANGUAGE DefaultSignatures
+             , FlexibleContexts
+             , FlexibleInstances
+             , GADTs
+             , MultiParamTypeClasses
+             , ScopedTypeVariables
+             , TypeOperators
+ #-}
+module Unbound.Generics.LocallyNameless.Subst (
+  SubstName(..)
+  , SubstCoerce(..)
+  , Subst(..)
+  ) where
+
+import GHC.Generics
+
+import Data.List (find)
+
+import Unbound.Generics.LocallyNameless.Name
+import Unbound.Generics.LocallyNameless.Alpha
+import Unbound.Generics.LocallyNameless.Embed
+import Unbound.Generics.LocallyNameless.Bind
+import Unbound.Generics.LocallyNameless.Rebind
+
+-- | See 'isVar'
+data SubstName a b where
+  SubstName :: (a ~ b) => Name a -> SubstName a b
+
+-- | See 'isCoerceVar'  
+data SubstCoerce a b where  
+  SubstCoerce :: Name b -> (b -> Maybe a) -> SubstCoerce a b
+
+-- | Instances of @'Subst' b a@ are terms of type @a@ that may contain
+-- variables of type @b@ that may participate in capture-avoiding
+-- substitution.
+class Subst b a where
+  -- | This is the only method that must be implemented
+  isvar :: a -> Maybe (SubstName a b)
+  isvar _ = Nothing
+
+  -- | This is an alternative version to 'isvar', useable in the case 
+  --   that the substituted argument doesn't have *exactly* the same type
+  --   as the term it should be substituted into.
+  --   The default implementation always returns 'Nothing'.
+  isCoerceVar :: a -> Maybe (SubstCoerce a b)
+  isCoerceVar _ = Nothing
+
+  -- | @'subst' nm e tm@ substitutes @e@ for @nm@ in @tm@.  It has
+  -- a default generic implementation in terms of @isvar@
+  subst :: Name b -> b -> a -> a
+  default subst :: (Generic a, GSubst b (Rep a)) => Name b -> b -> a -> a
+  subst n u x =
+    if (isFreeName n)
+    then case (isvar x :: Maybe (SubstName a b)) of
+      Just (SubstName m) -> if m == n then u else x
+      Nothing -> case (isCoerceVar x :: Maybe (SubstCoerce a b)) of
+        Just (SubstCoerce m f) -> if m == n then maybe x id (f u) else x
+        Nothing -> to $ gsubst n u (from x)
+    else error $ "Cannot substitute for bound variable " ++ show n
+
+  substs :: [(Name b, b)] -> a -> a
+  default substs :: (Generic a, GSubst b (Rep a)) => [(Name b, b)] -> a -> a
+  substs ss x
+    | all (isFreeName . fst) ss =
+      case (isvar x :: Maybe (SubstName a b)) of
+        Just (SubstName m) ->
+          case find ((==m) . fst) ss of
+            Just (_, u) -> u
+            Nothing     -> x
+        Nothing -> case isCoerceVar x :: Maybe (SubstCoerce a b) of 
+            Just (SubstCoerce m f) ->
+              case find ((==m) . fst) ss of 
+                  Just (_, u) -> maybe x id (f u)
+                  Nothing -> x
+            Nothing -> to $ gsubsts ss (from x)
+    | otherwise =
+      error $ "Cannot substitute for bound variable in: " ++ show (map fst ss)
+
+---- generic structural substitution.
+
+class GSubst b f where
+  gsubst :: Name b -> b -> f c -> f c
+  gsubsts :: [(Name b, b)] -> f c -> f c
+
+instance Subst b c => GSubst b (K1 i c) where
+  gsubst nm val = K1 . subst nm val . unK1
+  gsubsts ss = K1 . substs ss . unK1
+
+instance GSubst b f => GSubst b (M1 i c f) where
+  gsubst nm val = M1 . gsubst nm val . unM1
+  gsubsts ss = M1 . gsubsts ss . unM1
+
+instance GSubst b U1 where
+  gsubst _nm _val _ = U1
+  gsubsts _ss _ = U1
+
+instance GSubst b V1 where
+  gsubst _nm _val = id
+  gsubsts _ss = id
+
+instance (GSubst b f, GSubst b g) => GSubst b (f :*: g) where
+  gsubst nm val (f :*: g) = gsubst nm val f :*: gsubst nm val g
+  gsubsts ss (f :*: g) = gsubsts ss f :*: gsubsts ss g
+
+instance (GSubst b f, GSubst b g) => GSubst b (f :+: g) where
+  gsubst nm val (L1 f) = L1 $ gsubst nm val f
+  gsubst nm val (R1 g) = R1 $ gsubst nm val g
+
+  gsubsts ss (L1 f) = L1 $ gsubsts ss f
+  gsubsts ss (R1 g) = R1 $ gsubsts ss g
+
+-- these have a Generic instance, but
+-- it's self-refential (ie: Rep Int = D1 (C1 (S1 (Rec0 Int))))
+-- so our structural GSubst instances get stuck in an infinite loop.
+instance Subst b Int where subst _ _ = id ; substs _ = id
+instance Subst b Bool where subst _ _ = id ; substs _ = id
+instance Subst b () where subst _ _ = id ; substs _ = id
+instance Subst b Char where subst _ _ = id ; substs _ = id
+instance Subst b Float where subst _ _ = id ; substs _ = id
+instance Subst b Double where subst _ _ = id ; substs _ = id
+
+-- huh, apparently there's no instance Generic Integer. 
+instance Subst b Integer where subst _ _ = id ; substs _ = id
+
+instance (Subst c a, Subst c b) => Subst c (a,b)
+instance (Subst c a, Subst c b, Subst c d) => Subst c (a,b,d)
+instance (Subst c a, Subst c b, Subst c d, Subst c e) => Subst c (a,b,d,e)
+instance (Subst c a, Subst c b, Subst c d, Subst c e, Subst c f) =>
+   Subst c (a,b,d,e,f)
+instance (Subst c a) => Subst c [a]
+instance (Subst c a) => Subst c (Maybe a)
+instance (Subst c a, Subst c b) => Subst c (Either a b)
+
+instance Generic a => Subst b (Name a) where subst _ _ = id ; substs _ = id
+instance Subst b AnyName where subst _ _ = id ; substs _ = id
+
+instance (Subst c a) => Subst c (Embed a)
+
+instance (Subst c b, Subst c a, Alpha a, Alpha b) => Subst c (Bind a b)
+
+instance (Subst c p1, Subst c p2) => Subst c (Rebind p1 p2)
diff --git a/src/Unbound/Generics/LocallyNameless/Unsafe.hs b/src/Unbound/Generics/LocallyNameless/Unsafe.hs
new file mode 100644
--- /dev/null
+++ b/src/Unbound/Generics/LocallyNameless/Unsafe.hs
@@ -0,0 +1,24 @@
+{-# OPTIONS_HADDOCK show-extensions #-}
+-- |
+-- Module     : Unbound.Generics.LocallyNameless.Unsafe
+-- Copyright  : (c) 2014, Aleksey Kliger
+-- License    : BSD3 (See LICENSE)
+-- Maintainer : Aleksey Kliger
+-- Stability  : experimental
+--
+-- Dangerous operations that may disturb the invariants of
+-- "Unbind.Generics.LocallyNameless" or of your AST.
+{-# LANGUAGE DeriveGeneric #-}
+module Unbound.Generics.LocallyNameless.Unsafe
+       (
+         unsafeUnbind
+       ) where
+
+import Unbound.Generics.LocallyNameless.Alpha
+import Unbound.Generics.LocallyNameless.Bind
+
+-- | A destructor for binders that does /not/ guarantee fresh
+--   names for the binders.
+unsafeUnbind :: (Alpha p, Alpha t) => Bind p t -> (p, t)
+unsafeUnbind (B p t) = (p, open initialCtx p t)
+       
diff --git a/src/Unbound/Generics/PermM.hs b/src/Unbound/Generics/PermM.hs
new file mode 100644
--- /dev/null
+++ b/src/Unbound/Generics/PermM.hs
@@ -0,0 +1,165 @@
+----------------------------------------------------------------------
+-- |
+-- Module      :  Unbound.Generics.PermM
+-- Copyright   :  (c) 2011, Stephanie Weirich <sweirich@cis.upenn.edu>
+-- License     :  BSD-like (see PermM.hs)
+-- Maintainer  :  Aleksey Kliger
+-- Portability :  portable
+--
+-- A slow, but hopefully correct implementation of permutations.
+--
+----------------------------------------------------------------------
+{-
+Copyright (c)2011, Stephanie Weirich
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Stephanie Weirich nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+-}
+{-# LANGUAGE PatternGuards #-}
+module Unbound.Generics.PermM (
+    Perm(..), permValid, single, compose, apply, support, isid, join, empty, restrict, mkPerm
+  ) where
+
+import Prelude (Eq(..), Show(..), (.), ($), Monad(return), Ord(..), Maybe(..), otherwise, (&&), Bool(..), id, uncurry, Functor(..))
+import Data.Monoid
+import Data.List
+import Data.Map (Map)
+import qualified Data.Map as M
+import qualified Data.Set as S
+import Control.Arrow ((&&&))
+import Control.Monad ((>=>))
+
+-- | A /permutation/ is a bijective function from names to names
+--   which is the identity on all but a finite set of names.  They
+--   form the basis for nominal approaches to binding, but can
+--   also be useful in general.
+newtype Perm a = Perm (Map a a)
+
+-- | @'permValid' p@ returns @True@ iff the perumation is /valid/: if
+-- each value in the range of the permutation is also a key.
+permValid :: Ord a => Perm a -> Bool
+permValid (Perm p) = all (\(_,v) -> M.member v p) (M.assocs p)
+  -- a Map sends every key uniquely to a value by construction.  So if
+  -- every value is also a key, the sizes of the domain and range must
+  -- be equal and hence the mapping is a bijection.
+
+instance Ord a => Eq (Perm a) where
+  (Perm p1) == (Perm p2) =
+    all (\x -> M.findWithDefault x x p1 == M.findWithDefault x x p2) (M.keys p1) &&
+    all (\x -> M.findWithDefault x x p1 == M.findWithDefault x x p2) (M.keys p2)
+
+instance Show a => Show (Perm a) where
+  show (Perm p) = show p
+
+-- | Apply a permutation to an element of the domain.
+apply :: Ord a => Perm a -> a -> a
+apply (Perm p) x = M.findWithDefault x x p
+
+-- | Create a permutation which swaps two elements.
+single :: Ord a => a -> a -> Perm a
+single x y = if x == y then Perm M.empty else
+    Perm (M.insert x y (M.insert y x M.empty))
+
+-- | The empty (identity) permutation.
+empty :: Perm a
+empty = Perm M.empty
+
+-- | Compose two permutations.  The right-hand permutation will be
+--   applied first.
+compose :: Ord a => Perm a -> Perm a -> Perm a
+compose (Perm b) (Perm a) =
+  Perm (M.fromList ([ (x,M.findWithDefault y y b) | (x,y) <- M.toList a]
+         ++ [ (x, M.findWithDefault x x b) | x <- M.keys b, M.notMember x a]))
+
+-- | Permutations form a monoid under composition.
+instance Ord a => Monoid (Perm a) where
+  mempty  = empty
+  mappend = compose
+
+-- | Is this the identity permutation?
+isid :: Ord a => Perm a -> Bool
+isid (Perm p) =
+     M.foldrWithKey (\ a b r -> r && a == b) True p
+
+-- | /Join/ two permutations by taking the union of their relation
+--   graphs. Fail if they are inconsistent, i.e. map the same element
+--   to two different elements.
+join :: Ord a => Perm a -> Perm a -> Maybe (Perm a)
+join (Perm p1) (Perm p2) =
+     let overlap = M.intersectionWith (==) p1 p2 in
+     if M.fold (&&) True overlap then
+       Just (Perm (M.union p1 p2))
+       else Nothing
+
+-- | The /support/ of a permutation is the set of elements which are
+--   not fixed.
+support :: Ord a => Perm a -> [a]
+support (Perm p) = [ x | x <- M.keys p, M.findWithDefault x x p /= x]
+
+-- | Restrict a permutation to a certain domain.
+restrict :: Ord a => Perm a -> [a] -> Perm a
+restrict (Perm p) l = Perm (foldl' (\p' k -> M.delete k p') p l)
+
+-- | A partial permutation consists of two maps, one in each direction
+--   (inputs -> outputs and outputs -> inputs).
+data PartialPerm a = PP (M.Map a a) (M.Map a a)
+  deriving Show
+
+emptyPP :: PartialPerm a
+emptyPP = PP M.empty M.empty
+
+extendPP :: Ord a => a -> a -> PartialPerm a -> Maybe (PartialPerm a)
+extendPP x y pp@(PP mfwd mrev)
+  | Just y' <- M.lookup x mfwd = if y == y' then Just pp
+                                            else Nothing
+  | Just x' <- M.lookup y mrev = if x == x' then Just pp
+                                            else Nothing
+  | otherwise = Just $ PP (M.insert x y mfwd) (M.insert y x mrev)
+
+-- | Convert a partial permutation into a full permutation by closing
+--   off any remaining open chains into a cycles.
+ppToPerm :: Ord a => PartialPerm a -> Perm a
+ppToPerm (PP mfwd mrev) = Perm $ foldr (uncurry M.insert) mfwd
+                                       (map (findEnd &&& id) chainStarts)
+        -- beginnings of open chains are elements which map to
+        -- something in the forward direction but have no ancestor.
+  where chainStarts = S.toList (M.keysSet mfwd `S.difference` M.keysSet mrev)
+        findEnd x = case M.lookup x mfwd of
+                      Nothing -> x
+                      Just x' -> findEnd x'
+
+-- | @mkPerm l1 l2@ creates a permutation that sends @l1@ to @l2@.
+--   Fail if there is no such permutation, either because the lists
+--   have different lengths or because they are inconsistent (which
+--   can only happen if @l1@ or @l2@ have repeated elements).
+mkPerm :: Ord a => [a] -> [a] -> Maybe (Perm a)
+mkPerm xs ys
+  | length xs /= length ys = Nothing
+  | otherwise =
+    fmap ppToPerm . ($emptyPP) . foldr (>=>) return $ zipWith extendPP xs ys
diff --git a/test/Calc.hs b/test/Calc.hs
new file mode 100644
--- /dev/null
+++ b/test/Calc.hs
@@ -0,0 +1,165 @@
+-- |
+-- Module     : Calc
+-- Copyright  : (c) 2014, Aleksey Kliger
+-- License    : BSD3 (See LICENSE)
+-- Maintainer : Aleksey Kliger
+-- Stability  : experimental
+--
+{-# LANGUAGE DeriveGeneric, DeriveDataTypeable #-}
+module Calc where
+
+import Control.Arrow (second)
+import Data.Typeable (Typeable)
+import GHC.Generics (Generic)
+
+import Unbound.Generics.LocallyNameless
+import Unbound.Generics.LocallyNameless.Internal.Fold (toListOf)
+
+-- variables will range over expressions
+type Var = Name Expr
+
+-- expression is either a variable, a constant int, a summation of two
+-- expressions, a list of variables bound to expressions that may
+-- occur in the body of an expression (where the expressions in the
+-- list of bindings refer to an outer scope), or a sequence of nested bindings
+-- where each binding expression can refer to previously bound variables.
+data Expr = V Var
+          | C Int
+          | Add Expr Expr
+          | Let (Bind [(Var, Embed Expr)] Expr)
+          | LetStar (Bind LetStarBinds Expr)
+          deriving (Generic, Typeable, Show)
+
+data LetStarBinds = EmptyLSB
+                  | ConsLSB (Rebind (Var, Embed Expr) LetStarBinds)
+                  deriving (Generic, Typeable, Show)
+
+instance Alpha Expr
+instance Alpha LetStarBinds
+
+mkVar :: String -> Var
+mkVar = s2n
+
+anyFreeVarList :: Alpha a => a -> [AnyName]
+anyFreeVarList = toListOf fvAny
+
+freeVarList :: (Alpha a, Typeable b) => a -> [Name b]
+freeVarList = toListOf fv
+
+-- smart constructor for Let
+mkLet :: [(Var, Expr)] -> Expr -> Expr
+mkLet binds body = Let (bind (map (second Embed) binds) body)
+
+-- smart constructor for Let*
+mkLetStar :: [(Var, Expr)] -> Expr -> Expr
+mkLetStar binds body = LetStar (bind (mkLsb binds) body)
+  where
+    mkLsb [] = EmptyLSB
+    mkLsb ((v,e):rest) = ConsLSB (rebind (v, Embed e) (mkLsb rest))
+
+-- environments are partial maps from (free) variables to expressions.
+type Env = Var -> Maybe Expr
+
+emptyEnv :: Env
+emptyEnv = const Nothing
+
+extendEnv :: Var -> Expr -> Env -> Env
+extendEnv v e rho w =
+  if v == w then Just e else rho w
+
+whnf :: (Fresh m) => Env -> Expr -> m Expr
+whnf rho (V v) = case rho v of
+  Just e -> return e
+  Nothing -> fail $ "unbound variable " ++ show v
+whnf _rho (C i) = return (C i)
+whnf rho (Add e1 e2) = do
+  v1 <- whnf rho e1
+  v2 <- whnf rho e2
+  add v1 v2
+  where add :: Monad m => Expr -> Expr -> m Expr
+        add (C i1) (C i2) = return (C $ i1 + i2)
+        add _ _ = fail "add of two non-integers"
+whnf rho0 (Let b) = do
+  (binds, body) <- unbind b
+  binds' <- mapM (\(v, Embed e) -> do
+                     e' <- whnf rho0 e
+                     return (v, e')) binds
+  let rho' = foldl (\rho (v,e) -> extendEnv v e rho) rho0 binds'
+  whnf rho' body
+whnf rho0 (LetStar b) = do
+  (lsb, body) <- unbind b
+  rho' <- whnfLsb lsb rho0
+  whnf rho' body
+
+whnfLsb :: Fresh m => LetStarBinds -> Env -> m Env
+whnfLsb EmptyLSB = return
+whnfLsb (ConsLSB rbnd) = \rho -> do
+  let ((v, Embed e), lsb) = unrebind rbnd
+  e' <- whnf rho e
+  whnfLsb lsb (extendEnv v e' rho)
+
+runWhnf :: Env -> Expr -> Maybe Expr
+runWhnf rho e = runFreshMT (whnf rho e)
+
+ex1 :: Expr
+ex1 = Add (C 1) (C 2)
+
+ex2x :: Expr
+ex2x = V (mkVar "x")
+
+ex2y :: Expr
+ex2y = V (mkVar "y")
+
+ex2xc :: Expr
+ex2xc = close initialCtx (mkVar "x") ex2x
+
+ex2yc :: Expr
+ex2yc = close initialCtx (mkVar "y") ex2y
+
+ex3x :: Expr
+ex3x = let x = mkVar "x"
+       in mkLet [(x, (C 1))] $ Add (V x) (C 2)
+
+ex3y :: Expr
+ex3y = let y = mkVar "y"
+       in mkLet [(y, (C 1))] $ Add (V y) (C 2)
+
+ex4 :: Expr
+ex4 = let
+  x = mkVar "x"
+  y = mkVar "y"
+  in
+   mkLet [(y, (C 5))]
+   $ mkLet [(y, (C 200))
+           , (x, (Add (V y) -- refers to the outer y
+                  (C 6)))]
+   $ Add (V x) (V x) -- expect (C 22), not (C 412)
+
+ex4_ans :: Expr
+ex4_ans = C 22
+   
+ex5 :: Expr
+ex5 = let
+  x = mkVar "x"
+  y = mkVar "y"
+  in
+   mkLet [(y, (C 5))]
+   $ mkLetStar [(y, (C 200))
+               , (x, (Add (V y) -- refers to the inner y
+                      (C 6)))]
+   $ Add (V x) (V x) -- expect (C 412), not (C 22)
+
+ex5_ans :: Expr
+ex5_ans = C 412
+
+ex6 :: [Expr]
+ex6 = [V (mkVar "x"), V (mkVar "z"), mkLet [(mkVar "y", C 1)] (V (mkVar "y"))]
+
+ex6_ans :: [AnyName]
+ex6_ans = [AnyName (mkVar "x"), AnyName (mkVar "z")]
+
+ex7 :: [Expr]
+ex7 = [V (mkVar "x"), V (mkVar "z"), mkLet [(mkVar "y", C 1)] (V (mkVar "y"))]
+
+ex7_ans :: [Var]
+ex7_ans = [mkVar "x", mkVar "z"]
diff --git a/test/ParallelReduction.hs b/test/ParallelReduction.hs
new file mode 100644
--- /dev/null
+++ b/test/ParallelReduction.hs
@@ -0,0 +1,92 @@
+--
+-- We implement the parallel reduction relation e ⇛ e'
+-- that is a key to some kinds of confluence proofs for lambda calculi.
+{-# LANGUAGE DeriveGeneric, DeriveDataTypeable, MultiParamTypeClasses #-}
+module ParallelReduction where
+
+import Control.Applicative 
+import Control.Monad.Identity
+import GHC.Generics (Generic)
+import Data.Typeable (Typeable)
+
+import Unbound.Generics.LocallyNameless
+
+type Var = Name Expr
+
+-- in this case we just have an untyped lambda calculus
+data Expr = V Var
+          | Lam (Bind Var Expr)
+          | App Expr Expr
+          deriving (Show, Generic, Typeable)
+
+instance Alpha Expr
+
+instance Subst Expr Expr where
+  isvar (V n) = Just (SubstName n)
+  isvar _     = Nothing
+
+run :: FreshMT Identity Expr -> Expr
+run = runIdentity . runFreshMT
+
+-- parallel reduction is the compatible closure of cbn beta : (λx.e)f ⇛ {f'/x}e' where e⇛e' and f⇛f'
+-- we choose to allow reduction under a lambda.
+parStep :: (Applicative m, Fresh m) => Expr -> m Expr
+parStep v@(V _) = return v
+parStep (App e1 e2) =
+  case e1 of
+    Lam b -> betaStep e2 b
+    _ -> App <$> parStep e1 <*> parStep e2
+parStep (Lam b) = do
+  (v, e) <- unbind b
+  (Lam . (bind v)) <$> parStep e
+
+betaStep :: (Applicative m, Fresh m) => Expr -> Bind Var Expr -> m Expr
+betaStep f b = do
+  f' <- parStep f
+  (v, e) <- unbind b
+  e' <- parStep e
+  return (subst v f' e')
+
+-- repeatedly take parStep steps until the term doesn't change anymore.
+parSteps :: (Applicative m, Fresh m) => Expr -> m Expr
+parSteps e = do
+  e' <- parStep e
+  if (e `aeq` e')
+    then return e
+    else parSteps e'
+
+ex1 :: Bind Var Expr
+ex1 = let
+  x = s2n "x"
+  in bind x (V x)
+ex1' :: (Var, Expr)
+ex1' = let
+  y = s2n "y"
+  in
+   (y, V y)
+
+ex2 :: Expr
+ex2 = App (Lam ex2_1) ex2_2
+
+ex2_1 :: Bind Var Expr
+ex2_1 = let
+  x = s2n "x"
+  y = s2n "y"
+  in
+   bind x $ Lam $ bind y $ App (V x) (V y)
+
+ex2_2 :: Expr
+ex2_2 = let
+  z = s2n "z"
+  in
+   (Lam $ bind z $ V z)
+
+ident :: Expr
+ident = let
+  u = s2n "u"
+  in Lam $ bind u $ V u
+
+-- same as ex2 but with some extra beta redices in both halves of the application
+ex2_alt :: Expr
+ex2_alt = App (App ident (Lam ex2_1)) (App (App ident ident) ex2_2)
+  
diff --git a/test/test-calc.hs b/test/test-calc.hs
new file mode 100644
--- /dev/null
+++ b/test/test-calc.hs
@@ -0,0 +1,55 @@
+-- |
+-- Module     : test-stlc
+-- Copyright  : (c) 2014, Aleksey Kliger
+-- License    : BSD3 (See LICENSE)
+-- Maintainer : Aleksey Kliger
+-- Stability  : experimental
+--
+{-# LANGUAGE DeriveGeneric, DeriveDataTypeable #-}
+module Main where
+
+import Unbound.Generics.LocallyNameless
+
+import Calc
+
+import Test.HUnit
+
+test_ex1 :: Test
+test_ex1 = TestCase $ assertBool "example 1" (runWhnf emptyEnv ex1 `aeq` (Just $ C 3))
+
+test_ex2_open :: Test
+test_ex2_open = TestCase $ assertBool "example 2 (open)" (not $ aeq ex2x ex2y)
+
+test_ex2_closed :: Test
+test_ex2_closed = TestCase $ assertBool "example 2 (closed)" (aeq ex2xc ex2yc)
+
+test_ex3 :: Test
+test_ex3 = TestCase $ assertBool "example 3" (aeq ex3x ex3y)
+
+test_ex4 :: Test
+test_ex4 = TestCase $ assertBool "example 4 (let scoping)" (runWhnf emptyEnv ex4 `aeq` Just ex4_ans)
+
+test_ex5 :: Test
+test_ex5 = TestCase $ assertBool "example 5 (let* scoping)" (runWhnf emptyEnv ex5 `aeq` Just ex5_ans)
+
+test_ex6 :: Test
+test_ex6 = TestCase $ assertBool "example 6 (free variables)" (anyFreeVarList ex6 `aeq` ex6_ans)
+
+test_ex7 :: Test
+test_ex7 = TestCase $ assertBool "example 7 (sorted free variables)" (freeVarList ex7 `aeq` ex7_ans)
+
+
+main :: IO ()
+main = do
+  result <- runTestTT $ TestList [test_ex1
+                                 , test_ex2_open
+                                 , test_ex2_closed
+                                 , test_ex3
+                                 , test_ex4
+                                 , test_ex5
+                                 , test_ex6
+                                 , test_ex7
+                            ]
+  if failures result > 0
+    then fail "Some tests failed!"
+    else return ()
diff --git a/test/test-parallelreduction.hs b/test/test-parallelreduction.hs
new file mode 100644
--- /dev/null
+++ b/test/test-parallelreduction.hs
@@ -0,0 +1,25 @@
+module Main where
+
+import Test.HUnit
+
+import Unbound.Generics.LocallyNameless (subst, aeq)
+
+import ParallelReduction
+
+
+
+
+test_ex1 :: Test
+test_ex1 = TestCase $ assertBool "simple substitution" (subst (fst ex1') (Lam ex1) (snd ex1') `aeq` (Lam ex1))
+
+test_ex2 :: Test
+test_ex2 = TestCase $ assertBool "parallel reduction" (run (parSteps ex2) `aeq` run (parSteps ex2_alt))
+
+main :: IO ()
+main = do
+  result <- runTestTT $ TestList [test_ex1
+                                 , test_ex2
+                                 ]
+  if failures result > 0
+    then fail "Some tests failed!"
+    else return ()
diff --git a/unbound-generics.cabal b/unbound-generics.cabal
new file mode 100644
--- /dev/null
+++ b/unbound-generics.cabal
@@ -0,0 +1,83 @@
+-- Initial unbound-generics.cabal generated by cabal init.  For further 
+-- documentation, see http://haskell.org/cabal/users-guide/
+
+name:                unbound-generics
+version:             0.0.0.90
+synopsis:            Reimplementation of Unbound using GHC Generics
+description:         Specify the binding structure of your data type with an
+                     expressive set of type combinators, and unbound-generics
+                     handles the rest!  Automatically derives
+                     alpha-equivalence, free variable calculation,
+                     capture-avoiding substitution, and more. See
+                     @Unbound.Generics.LocallyNameless@ to get started.
+                     .
+                     This is an independent re-implementation of <http://hackage.haskell.org/package/unbound Unbound>
+                     but using <http://www.haskell.org/ghc/docs/latest/html/libraries/base-4.7.0.1/GHC-Generics.html GHC.Generics>
+                     instead of <http://http://hackage.haskell.org/package/RepLib RepLib>.
+                     See the accompanying README for some porting notes.
+                     
+homepage:            http://github.com/lambdageek/unbound-generics
+bug-reports:         http://github.com/lambdageek/unbound-generics/issues
+license:             BSD3
+license-file:        LICENSE
+author:              Aleksey Kliger
+maintainer:          aleksey@lambdageek.org
+copyright:           (c) 2014, Aleksey Kliger
+category:            Language
+build-type:          Simple
+extra-source-files:  examples/*.hs,
+                     README.md,
+                     Changelog.md
+cabal-version:       >=1.10
+
+library
+  exposed-modules:     Unbound.Generics.LocallyNameless
+                       Unbound.Generics.LocallyNameless.Name
+                       Unbound.Generics.LocallyNameless.Fresh
+                       Unbound.Generics.LocallyNameless.LFresh
+                       Unbound.Generics.LocallyNameless.Alpha
+                       Unbound.Generics.LocallyNameless.Bind
+                       Unbound.Generics.LocallyNameless.Rebind
+                       Unbound.Generics.LocallyNameless.Embed
+                       Unbound.Generics.LocallyNameless.Operations
+                       Unbound.Generics.LocallyNameless.Unsafe
+                       Unbound.Generics.LocallyNameless.Internal.Fold
+                       Unbound.Generics.PermM
+                       Unbound.Generics.LocallyNameless.Subst
+  -- other-modules:       
+  -- other-extensions:    
+  build-depends:       base >=4.6 && <5,
+                       mtl >= 2.1,
+                       transformers >= 0.3,
+                       containers == 0.5.*,
+                       contravariant >= 0.5
+  hs-source-dirs:      src
+  default-language:    Haskell2010
+  ghc-options:         -Wall
+
+Test-Suite test-calc
+  type:                exitcode-stdio-1.0
+  main-is:             test-calc.hs
+  other-modules:       Calc
+  build-depends:       base,
+                       HUnit == 1.2.*,
+                       unbound-generics
+  hs-source-dirs:      test
+  default-language:    Haskell2010
+  ghc-options:         -Wall
+
+Test-Suite test-parallelreduction
+  type:                exitcode-stdio-1.0
+  main-is:             test-parallelreduction.hs
+  other-modules:       ParallelReduction
+  build-depends:       base,
+                       HUnit == 1.2.*,
+                       mtl >= 2.1,
+                       unbound-generics
+  hs-source-dirs:      test
+  default-language:    Haskell2010
+  ghc-options:         -Wall
+
+source-repository head
+  type:                git
+  location:            git://github.com/lambdageek/unbound-generics.git