diff --git a/Examples/LambdaLift/Common.hs b/Examples/LambdaLift/Common.hs
new file mode 100644
--- /dev/null
+++ b/Examples/LambdaLift/Common.hs
@@ -0,0 +1,3 @@
+module LambdaLift.Common where
+
+data Type = TyUnit | TyInt | TyFun Type Type deriving Show
diff --git a/Examples/LambdaLift/DeepSeq.hs b/Examples/LambdaLift/DeepSeq.hs
new file mode 100644
--- /dev/null
+++ b/Examples/LambdaLift/DeepSeq.hs
@@ -0,0 +1,34 @@
+{-# LANGUAGE TypeOperators, FlexibleInstances, FlexibleContexts,
+  UndecidableInstances #-}
+
+module LambdaLift.DeepSeq where
+
+import Data.Yoko
+
+
+
+class DeepSeq a where rnf :: a -> ()
+instance DeepSeq a => DeepSeq [a] where
+  rnf [] = ()
+  rnf (x : xs) = rnf x `seq` rnf xs
+instance DeepSeq a => DeepSeq (N a) where rnf = rnf . unN
+instance (DeepSeq a, DeepSeq b) => DeepSeq (a :+: b) where
+  rnf = foldPlus rnf rnf
+instance DeepSeq sum => DeepSeq (DCsOf a sum) where rnf = rnf . unDCsOf
+instance (DeepSeq a, DeepSeq b) => DeepSeq (a :*: b) where
+  rnf = foldTimes seq rnf rnf
+instance DeepSeq a => DeepSeq (Rec a) where rnf = rnf . unRec
+instance DeepSeq a => DeepSeq (Dep a) where rnf = rnf . unDep
+instance DeepSeq (f a) => DeepSeq (Par1 f a) where rnf = rnf . unPar1
+instance DeepSeq U where rnf U = ()
+
+instance DeepSeq Int where rnf = (`seq` ())
+instance (DeepSeq a, DeepSeq b) => DeepSeq (Either a b) where
+  rnf = either rnf rnf
+
+instance (DeepSeq a, DeepSeq b, DeepSeq c) =>
+  DeepSeq (a, b, c) where
+  rnf (a, b, c) = rnf a `seq` rnf b `seq` rnf c
+instance (DeepSeq a, DeepSeq b, DeepSeq c, DeepSeq d) =>
+  DeepSeq (a, b, c, d) where
+  rnf (a, b, c, d) = rnf a `seq` rnf b `seq` rnf c `seq` rnf d
diff --git a/Examples/LambdaLift/FreeVars.hs b/Examples/LambdaLift/FreeVars.hs
new file mode 100644
--- /dev/null
+++ b/Examples/LambdaLift/FreeVars.hs
@@ -0,0 +1,60 @@
+{-# LANGUAGE TypeOperators, FlexibleContexts, UndecidableInstances #-}
+
+module LambdaLift.FreeVars where
+
+import LambdaLift.ULC
+
+import qualified Data.IntSet as IS
+import Data.Foldable (Foldable, foldMap)
+
+import Data.Yoko
+
+
+
+
+
+type Frees = IS.IntSet
+
+bump :: Int -> Frees -> Frees
+bump k = IS.map (subtract k) . IS.filter (>= k)
+
+
+
+
+
+anonFVs :: ULC -> Frees
+anonFVs = freeVars
+
+
+
+class FreeVars a where freeVars :: a -> Frees
+
+instance FreeVars ULC where
+  freeVars = w where
+    w tm = case partition $ disband tm of
+      Left x -> ($ x) $
+        (\(Lam_ ty tm) -> bump 1 $ w tm) .||
+        (\(Var_ i) -> IS.singleton i) .|.
+        (\(Let_ ds tm) ->
+          foldr (\(Decl _ tm) -> IS.union (w tm) . bump 1) (w tm) ds)
+      Right x -> freeVars x
+
+-- through sums
+instance FreeVars sum => FreeVars (DCsOf t sum) where
+  freeVars = freeVars . unDCsOf
+instance (FreeVars a, FreeVars b) => FreeVars (a :+: b) where
+  freeVars = foldPlus freeVars freeVars
+instance (Generic a, FreeVars (Rep a)) => FreeVars (N a) where
+  freeVars = freeVars . rep . unN
+
+-- through products
+instance FreeVars U where freeVars = const IS.empty
+instance (FreeVars a, FreeVars b) => FreeVars (a :*: b) where
+  freeVars = foldTimes IS.union freeVars freeVars
+
+-- through fields
+instance FreeVars a => FreeVars (Rec a) where
+  freeVars = freeVars . unRec
+instance FreeVars (Dep a) where freeVars = const IS.empty
+instance (Foldable f, FreeVars a) => FreeVars (Par1 f a) where
+  freeVars = foldMap freeVars . unPar1
diff --git a/Examples/LambdaLift/LLBasics.hs b/Examples/LambdaLift/LLBasics.hs
new file mode 100644
--- /dev/null
+++ b/Examples/LambdaLift/LLBasics.hs
@@ -0,0 +1,61 @@
+{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, TypeFamilies,
+  UndecidableInstances #-}
+
+module LambdaLift.LLBasics where
+
+import LambdaLift.Common
+
+import LambdaLift.TLF
+
+import qualified Data.IntMap as IM; import Data.IntMap (IntMap)
+
+import Control.Monad (liftM, ap)
+import Control.Applicative (Applicative(pure, (<*>)))
+
+
+
+
+
+-- # of formal variables and the mapping for captives
+type Rename = (Int, IntMap Int)
+
+lookupRN :: Rename -> Int -> Occ
+lookupRN rn@(locals, m) i
+  | i < locals = Par i
+  | otherwise = maybe err Env $ IM.lookup (i - locals) m
+  where err = error $ "LLBasics.lookupRN: unresolved variable: " ++ show (i, rn)
+
+
+
+newtype M a =
+  M {runM :: ([Type], Rename, Int) -> (a, [FunDec])}
+
+instance Functor M where fmap = liftM
+instance Applicative M where pure = return; (<*>) = ap
+instance Monad M where
+  return a = M $ \_ -> (a, [])
+  m >>= k = M $ \(tys, rn, sh) ->
+    -- NB backwards state: a and w' are circular
+    let (a, w)  = runM m     (tys, rn, sh + length w')
+        (b, w') = runM (k a) (tys, rn, sh)
+    in (b, w ++ w')
+
+
+
+ask :: M ([Type], Rename)
+ask = M $ \ ~(x, y, _) -> ((x, y), [])
+
+local :: (([Type], Rename) -> ([Type], Rename)) -> M a -> M a
+local f (M g) = M $ \ ~(x, y, z) -> case f (x, y) of
+  ~(x', y') -> g (x', y', z)
+
+
+
+intermediates :: M Int
+intermediates = M $ \ ~(_, _, s) -> (s, [])
+
+emit :: FunDec -> M ()
+emit w = M $ \_ -> ((), [w])
+
+ignoreEmissions :: M a -> M a
+ignoreEmissions (M f) = M $ \(tys, rn, _) -> f (tys, rn, 0)
diff --git a/Examples/LambdaLift/LambdaLift.hs b/Examples/LambdaLift/LambdaLift.hs
new file mode 100644
--- /dev/null
+++ b/Examples/LambdaLift/LambdaLift.hs
@@ -0,0 +1,145 @@
+{-# LANGUAGE TypeFamilies, MultiParamTypeClasses #-}
+
+module LambdaLift.LambdaLift where
+
+import LambdaLift.Common
+import LambdaLift.ULC as A
+import LambdaLift.TLF
+
+import qualified Data.IntMap as IM
+import qualified Data.IntSet as IS
+
+import Data.Yoko
+import Data.Yoko.HCompos
+
+import LambdaLift.LLBasics
+import LambdaLift.FreeVars (freeVars)
+import LambdaLift.DeepSeq (DeepSeq(..))
+
+
+
+
+
+lambdaLift :: [Type] -> ULC -> Prog
+lambdaLift e x = Prog ds tm where
+  (tm, ds) = runM (ll x) (e, (length e, IM.empty), 0)
+
+
+
+data Cnv = Cnv
+type instance Idiom Cnv = M
+instance HCompos Cnv ULC TLF where hcompos Cnv = ll
+
+
+
+ll :: ULC -> M TLF
+ll tm = exact_case (hcompos Cnv) tm $ llLam .|| llVar .|. llLet
+
+llLam lams@(Lam_ tyTop tmTop) = do
+  -- get the body; count formals; determine captives
+  let ((tys, ty), ulc) = peel ([], tyTop) tmTop where
+        peel (acc, ty') (Lam ty tm) = peel (ty' : acc, ty) tm
+        peel acc tm = (acc, tm)
+  let nLocals = 1 + length tys -- NB "1 +" is for ty
+  let captives = freeVars $ rejoin lams
+      captives' = IS.toAscList captives
+      captives'' = reverse captives'
+
+  (rho, rn) <- ask
+
+  -- generate a top-level function from the body
+  do let m = IM.fromDistinctAscList $ zip captives' [0..]
+     tlf <- ignoreEmissions $
+            local (const (ty : tys ++ rho, (nLocals, m))) $ ll ulc
+     emit (map (rho !!) captives'', reverse tys, ty, tlf)
+
+  -- replace lambdas with an invocation of tlf
+  sh <- intermediates
+
+  return $ Top (sh - 1) $ map (lookupRN rn) $ captives''
+llVar (Var_ i) = ask >>= \(_, rn) -> return $ Occ $ lookupRN rn i
+llLet (Let_ ds tm) = ll $ foldr (\(Decl ty tm) x -> A.App (Lam ty tm) x) tm ds
+
+
+
+
+
+infixl 1 @@
+(@@) = A.App
+
+s_comb a b c = Lam (TyFun a (TyFun b c)) . Lam (TyFun a b) . Lam a $
+               Var 2 @@ Var 0 @@ (Var 1 @@ Var 0)
+
+ex0 = Lam TyInt (Var 0)
+ex0' = lambdaLift [] ex0
+
+ex1 = s_comb TyInt TyInt TyInt @@ (Lam TyInt $ Lam TyInt (Var 0))
+                               @@ Lam TyUnit (Var 2 @@ Var 1)
+ex1' = lambdaLift [TyInt, TyFun TyInt TyInt] ex1
+
+ex2 = Lam (TyFun (TyFun TyInt TyInt) TyUnit) $
+      Lam (TyFun TyInt TyInt)
+            (Var 1 @@ Lam TyInt (Var 1 @@ Var 0))
+ex2' = lambdaLift [] ex2
+
+ex3 = Lam TyUnit . Lam TyUnit . Lam TyUnit .
+      (Var 1 @@) . Lam TyUnit .
+       (Var 3 @@) . Lam TyInt $
+        Var 1
+ex3' = lambdaLift [] ex3
+
+ex4 = Lam (TyFun TyInt TyInt) (Var 0) @@ Lam TyInt (Var 0)
+ex4' = lambdaLift [] ex4
+
+ex5 = Lam (TyFun (TyFun TyInt TyInt) (TyFun TyInt TyInt)) (Var 0) @@
+      Lam (TyFun TyInt TyInt)
+          (Lam TyUnit (Var 1) @@ Var 1)
+ex5' = lambdaLift [TyUnit] ex5
+
+-- TODO can I make the Tops use scoped instead of global indices?
+
+{-
+ex0' ==
+Prog [([],[],TyInt,Var 0)
+     ] (Top 0 [])
+
+ex1' ==
+Prog [([],[TyFun TyInt (TyFun TyInt TyInt),TyFun TyInt TyInt],TyInt,
+         App (App (Var 2) (Var 0)) (App (Var 1) (Var 0))),
+      ([],[TyInt],TyInt,Var 0),
+      ([TyFun TyInt TyInt,TyInt],[],TyUnit,App (Var ^1) (Var ^0))
+     ] (App (App (Top 0 []) (Top 1 [])) (Top 2 [1,0]))
+
+ex2' ==
+Prog [([TyFun TyInt TyInt],[],TyInt,App (Var ^0) (Var 0)),
+      ([],[TyFun (TyFun TyInt TyInt) TyUnit],TyFun TyInt TyInt,
+         App (Var 1) (Top 0 [0]))
+     ] (Top 1 [])
+
+ex3' ==
+Prog [([TyUnit],[],TyInt,Var ^0),
+      ([TyUnit],[],TyUnit,App (Var ^0) (Top 0 [0])),
+      ([],[TyUnit,TyUnit],TyUnit,App (Var 1) (Top 1 [2]))
+     ] (Top 2 [])
+
+ex4' ==
+Prog [([],[],TyFun TyInt TyInt,Var 0),
+      ([],[],TyInt,Var 0)
+     ] (App (Top 0 []) (Top 1 []))
+
+ex5' ==
+Prog [([],[],TyFun (TyFun TyInt TyInt) (TyFun TyInt TyInt),Var 0),
+      ([TyFun TyInt TyInt],[],TyUnit,Var ^0),
+      ([TyUnit],[],TyFun TyInt TyInt,App (Top 1 [0]) (Var ^0))
+     ] (App (Top 0 []) (Top 2 [0]))
+
+-}
+
+instance DeepSeq Type where rnf = (`seq` ())
+instance DeepSeq Occ  where
+  rnf (Par x) = rnf x
+  rnf (Env x) = rnf x
+instance DeepSeq Prog where rnf (Prog decs tm) = rnf decs `seq` rnf tm
+instance DeepSeq TLF  where rnf = rnf . reps . disband
+
+all_exs = rnf [ex0', ex1', ex2', ex3', ex4', ex5']
diff --git a/Examples/LambdaLift/TLF.hs b/Examples/LambdaLift/TLF.hs
new file mode 100644
--- /dev/null
+++ b/Examples/LambdaLift/TLF.hs
@@ -0,0 +1,66 @@
+{-# LANGUAGE TypeFamilies, TemplateHaskell, TypeOperators #-}
+
+module LambdaLift.TLF where
+
+import Data.Yoko.TypeBasics (encode, derive)
+import Data.Yoko
+
+import LambdaLift.Common
+
+
+data Occ = Par Int | Env Int
+instance Show Occ where
+  show (Par i) = show i
+  show (Env i) = '^' : show i
+
+data TLF = Top Int [Occ] | Occ Occ
+         | App TLF TLF deriving Show
+
+type FunDec = ([Type], [Type], Type, TLF)
+data Prog = Prog [FunDec] TLF deriving Show
+
+
+
+
+
+data Top_ = Top_ Int [Occ]
+data Occ_ = Occ_ Occ
+data App_  = App_ TLF TLF
+
+
+
+type instance Range Top_ = TLF
+type instance Range Occ_  = TLF
+type instance Range App_  = TLF
+
+type instance Tag Top_ = $(return $ encode "Top")
+type instance Tag Occ_ = $(return $ encode "Occ")
+type instance Tag App_  = $(return $ encode "App")
+
+concat `fmap` mapM derive [''TLF, ''Top_, ''Occ_, ''App_]
+
+
+
+type instance Rep Top_ = Dep Int :*: Dep [Occ]
+instance Generic Top_ where
+  rep (Top_ i os) = Dep i :*: Dep os
+  obj (Dep i :*: Dep os) = Top_ i os
+type instance Rep Occ_ = Dep Occ
+instance Generic Occ_ where
+  rep (Occ_ o) = Dep o
+  obj (Dep o) = Occ_ o
+type instance Rep App_ = Rec TLF :*: Rec TLF
+instance Generic App_ where
+  rep (App_ tm1 tm2) = Rec tm1 :*: Rec tm2
+  obj (Rec tm1 :*: Rec tm2) = App_ tm1 tm2
+
+
+
+type instance DCs TLF = (N Top_ :+: N Occ_) :+: N App_
+instance DT TLF where
+  disband (Top i os )   = DCsOf . inject $ Top_ i os
+  disband (Occ o)       = DCsOf . inject $ Occ_ o
+  disband (App tm1 tm2) = DCsOf . inject $ App_ tm1 tm2
+instance DC Top_ where rejoin (Top_ i os)    = Top i os
+instance DC Occ_ where rejoin (Occ_  o)      = Occ o
+instance DC App_ where rejoin (App_ tm1 tm2) = App tm1 tm2
diff --git a/Examples/LambdaLift/ULC.hs b/Examples/LambdaLift/ULC.hs
new file mode 100644
--- /dev/null
+++ b/Examples/LambdaLift/ULC.hs
@@ -0,0 +1,84 @@
+{-# LANGUAGE TypeFamilies, TemplateHaskell, TypeOperators #-}
+
+module LambdaLift.ULC where
+
+import Data.Yoko
+import Data.Yoko.TypeBasics (encode, derive)
+import LambdaLift.Common
+
+
+
+data ULC = Lam Type ULC | Var Int
+         | Let [Decl] ULC
+         | App ULC ULC deriving Show
+
+data Decl = Decl Type ULC deriving Show
+
+
+data Lam_ = Lam_ Type ULC
+data Var_ = Var_ Int
+data Let_ = Let_ [Decl] ULC
+data App_ = App_ ULC ULC
+
+data Decl_ = Decl_ Type ULC
+
+
+
+type instance Range Lam_ = ULC
+type instance Range Var_ = ULC
+type instance Range Let_ = ULC
+type instance Range App_ = ULC
+
+type instance Range Decl_ = Decl
+
+type instance Tag Lam_ = $(return $ encode "Lam")
+type instance Tag Var_ = $(return $ encode "Var")
+type instance Tag Let_ = $(return $ encode "Let")
+type instance Tag App_ = $(return $ encode "App")
+
+type instance Tag Decl_ = $(return $ encode "Decl")
+
+concat `fmap` mapM derive [''ULC, ''Decl, ''Lam_, ''Var_, ''Let_, ''App_, ''Decl_]
+
+
+
+type instance Rep Lam_ = Dep Type :*: Rec ULC
+instance Generic Lam_ where
+  rep (Lam_ ty tm) = Dep ty :*: Rec tm
+  obj (Dep ty :*: Rec tm) = Lam_ ty tm
+type instance Rep Var_ = Dep Int
+instance Generic Var_ where
+  rep (Var_ i) = Dep i
+  obj (Dep i) = Var_ i
+type instance Rep Let_ = Par1 [] (Rec Decl) :*: Rec ULC
+instance Generic Let_ where
+  rep (Let_ ds tm) = Par1 (map Rec ds) :*: Rec tm
+  obj (Par1 ds :*: Rec tm) = Let_ (fmap unRec ds) tm
+type instance Rep App_ = Rec ULC :*: Rec ULC
+instance Generic App_ where
+  rep (App_ tm1 tm2) = Rec tm1 :*: Rec tm2
+  obj (Rec tm1 :*: Rec tm2) = App_ tm1 tm2
+
+type instance Rep Decl_ = Dep Type :*: Rec ULC
+instance Generic Decl_ where
+  rep (Decl_ ty tm) = Dep ty :*: Rec tm
+  obj (Dep ty :*: Rec tm) = Decl_ ty tm
+
+
+
+type instance DCs ULC =
+  (N Lam_ :+: N Var_) :+: (N Let_ :+: N App_)
+instance DT ULC where
+  disband (Lam ty tm)   = DCsOf . inject $ Lam_ ty tm
+  disband (Var i)       = DCsOf . inject $ Var_ i
+  disband (Let ds tm)   = DCsOf . inject $ Let_ ds tm
+  disband (App tm1 tm2) = DCsOf . inject $ App_ tm1 tm2
+instance DC Lam_ where rejoin (Lam_ ty tm)   = Lam ty tm
+instance DC Var_ where rejoin (Var_ i)       = Var i
+instance DC Let_ where rejoin (Let_ ds tm)   = Let ds tm
+instance DC App_ where rejoin (App_ tm1 tm2) = App tm1 tm2
+
+type instance DCs Decl = N Decl_
+instance DT Decl where
+  disband (Decl ty tm) = DCsOf . N $ Decl_ ty tm
+instance DC Decl_ where rejoin (Decl_ ty tm) = Decl ty tm
diff --git a/yoko.cabal b/yoko.cabal
--- a/yoko.cabal
+++ b/yoko.cabal
@@ -1,5 +1,5 @@
 name: yoko
-version: 0.3.1.1
+version: 0.3.1.2
 synopsis: Generic Programming with Disbanded Data Types
 
 description:
@@ -76,7 +76,7 @@
 build-type: Simple
 cabal-version: >= 1.6
 
-extra-source-files: README, CHANGES, Examples/*.hs
+extra-source-files: README, CHANGES, Examples/*.hs, Examples/LambdaLift/*.hs