diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,20 @@
+Copyright (c) 2014 Jonathan Sterling
+
+Permission is hereby granted, free of charge, to any person obtaining
+a copy of this software and associated documentation files (the
+"Software"), to deal in the Software without restriction, including
+without limitation the rights to use, copy, modify, merge, publish,
+distribute, sublicense, and/or sell copies of the Software, and to
+permit persons to whom the Software is furnished to do so, subject to
+the following conditions:
+
+The above copyright notice and this permission notice shall be included
+in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
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/abt.cabal b/abt.cabal
new file mode 100644
--- /dev/null
+++ b/abt.cabal
@@ -0,0 +1,33 @@
+name:                abt
+version:             0.1.0.0
+synopsis:            Abstract binding trees for Haskell
+description:         A Haskell port of the Carnegie Mellon ABT library (SML), with some improvements.
+license:             MIT
+license-file:        LICENSE
+author:              Jonathan Sterling
+maintainer:          jon@jonmsterling.com
+-- copyright:
+category:            Language
+build-type:          Simple
+-- extra-source-files:
+cabal-version:       >=1.10
+
+library
+  exposed-modules:     Abt.Class,
+                       Abt.Class.Show1,
+                       Abt.Class.HEq1,
+                       Abt.Class.Monad,
+                       Abt.Class.Abt,
+                       Abt.Types,
+                       Abt.Types.Nat,
+                       Abt.Types.HList,
+                       Abt.Types.View,
+                       Abt.Concrete.LocallyNameless
+                       Abt.Tutorial
+  -- other-modules:
+  -- other-extensions:
+  build-depends:       base >=4.7 && <4.8,
+                       transformers,
+                       mtl
+  hs-source-dirs:      src
+  default-language:    Haskell2010
diff --git a/src/Abt/Class.hs b/src/Abt/Class.hs
new file mode 100644
--- /dev/null
+++ b/src/Abt/Class.hs
@@ -0,0 +1,15 @@
+-- | The core signatures used to define abstract binding trees.
+--
+module Abt.Class
+( module Abt.Class.Abt
+, module Abt.Class.Monad
+, module Abt.Class.Show1
+, module Abt.Class.HEq1
+) where
+
+import Abt.Class.Abt
+import Abt.Class.Monad
+import Abt.Class.Show1
+import Abt.Class.HEq1
+
+
diff --git a/src/Abt/Class/Abt.hs b/src/Abt/Class/Abt.hs
new file mode 100644
--- /dev/null
+++ b/src/Abt/Class/Abt.hs
@@ -0,0 +1,128 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE UnicodeSyntax #-}
+
+module Abt.Class.Abt
+( Abt(..)
+) where
+
+import Abt.Types.Nat
+import Abt.Types.HList
+import Abt.Types.View
+import Abt.Class.Monad
+import Abt.Class.Show1
+
+import Control.Applicative
+import qualified Data.List as L
+
+-- | The 'Abt' signature represents mediation between an arbitrary (possibly
+-- nameless) term representaion, and a first-order one (the 'View'). Based on
+-- the (effectful) ismorphism @'into' / 'out'@ between representations, many
+-- operations can be defined generically for arbitrary operator sets, including
+-- substitution and aggregation of free variables.
+--
+class (Show1 o, Show v) ⇒ Abt (v ∷ *) (o ∷ [Nat] → *) (t ∷ Nat → *) | t → v o, o → t where
+  -- | Convert a 'View' into a term.
+  --
+  into
+    ∷ View v o n t
+    → t n
+
+  -- | Convert a term into a first-order 'View'.
+  --
+  out
+    ∷ MonadVar v m
+    ⇒ t n
+    → m (View v o n t)
+
+  -- | The injection from variables to terms.
+  --
+  var
+    ∷ v
+    → t Z
+  var = into . V
+
+  -- | Construct an abstraction.
+  --
+  (\\)
+    ∷ v
+    → t n
+    → t (S n)
+  v \\ e = into $ (v :\ e)
+
+  -- | Construct an operator term.
+  --
+  ($$)
+    ∷ o ns
+    → HList t ns
+    → t Z
+  o $$ es = into $ o :$ es
+  infixl 1 $$
+
+  -- | Substitute a term for a variable.
+  --
+  subst
+    ∷ MonadVar v m
+    ⇒ t Z
+    → v
+    → t n
+    → m (t n)
+  subst e v e' = do
+    oe' ← out e'
+    case oe' of
+      V v' → return $ if v == v' then e else e'
+      v' :\ e'' → do
+        e''' ← subst e v e''
+        return $ v' \\ e'''
+      o :$ es → do
+        es' ← htraverse (subst e v) es
+        return $ o $$ es'
+
+  -- | Instantiate the bound variable of an abstraction.
+  --
+  (//)
+    ∷ MonadVar v m
+    ⇒ t (S n)
+    → t Z
+    → m (t n)
+  xe // e' = do
+    v :\ e ← out xe
+    subst e' v e
+
+  -- | Compute the free variables of a term.
+  --
+  freeVars
+    ∷ MonadVar v m
+    ⇒ t n
+    → m [v]
+  freeVars e = do
+    oe ← out e
+    case oe of
+      V v → return [v]
+      v :\ e' → do
+        L.delete v <$>
+          freeVars e'
+      o :$ es → do
+        concat <$>
+          homogenizeA freeVars es
+
+  -- | Render a term into a human-readable string.
+  --
+  toString
+    ∷ MonadVar v m
+    ⇒ t n
+    → m String
+  toString e = do
+    vu ← out e
+    case vu of
+      V v → return $ show v
+      v :\ e → do
+        e' ← toString e
+        return $ show v ++ "." ++ e'
+      o :$ es → do
+        es' ← homogenizeA toString es
+        return $ show1 o ++ "[" ++ L.intercalate ";" es' ++ "]"
+
diff --git a/src/Abt/Class/HEq1.hs b/src/Abt/Class/HEq1.hs
new file mode 100644
--- /dev/null
+++ b/src/Abt/Class/HEq1.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE UnicodeSyntax #-}
+
+module Abt.Class.HEq1 where
+
+-- | Uniform variant of 'Eq' for indexed types. This is different from
+-- 'Data.Functor.Eq1' in that it is properly kind polymorphic and crucially
+-- heterogeneous, and it places no constraint on the index.
+--
+class HEq1 f where
+  (===) ∷ f i → f j → Bool
diff --git a/src/Abt/Class/Monad.hs b/src/Abt/Class/Monad.hs
new file mode 100644
--- /dev/null
+++ b/src/Abt/Class/Monad.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE UnicodeSyntax #-}
+
+module Abt.Class.Monad where
+
+import Control.Applicative
+
+class (Ord v, Eq v, Show v, Monad m, Applicative m) ⇒ MonadVar v m | m → v where
+  -- | Generates a fresh variable
+  fresh ∷ m v
+
+  -- | Generates a fresh variable tagged with a name
+  named ∷ String → m v
diff --git a/src/Abt/Class/Show1.hs b/src/Abt/Class/Show1.hs
new file mode 100644
--- /dev/null
+++ b/src/Abt/Class/Show1.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE UnicodeSyntax #-}
+
+module Abt.Class.Show1 where
+
+-- | Uniform variant of 'Show' for indexed types. This is different from
+-- 'Data.Functor.Show1' in that it is properly kind polymorphic.
+--
+class Show1 f where
+  showsPrec1 ∷ Int → f i → ShowS
+  showsPrec1 i x = (show1 x ++)
+
+  show1 ∷ f i → String
+  show1 x = showsPrec1 0 x ""
+
diff --git a/src/Abt/Concrete/LocallyNameless.hs b/src/Abt/Concrete/LocallyNameless.hs
new file mode 100644
--- /dev/null
+++ b/src/Abt/Concrete/LocallyNameless.hs
@@ -0,0 +1,122 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE UnicodeSyntax #-}
+
+module Abt.Concrete.LocallyNameless
+( Tm(..)
+, Var(..)
+, varName
+, varIndex
+) where
+
+import Abt.Types.Nat
+import Abt.Types.HList
+import Abt.Types.View
+import Abt.Class.HEq1
+import Abt.Class.Show1
+import Abt.Class.Abt
+import Abt.Class.Monad
+
+import Control.Applicative
+
+-- | A variable is a De Bruijn index, optionally decorated with a display name.
+data Var
+  = Var
+  { _varName ∷ !(Maybe String)
+  , _varIndex ∷ !Int
+  }
+
+instance Show Var where
+  show (Var (Just v) _) = v
+  show (Var Nothing i) = "@" ++ show i
+
+instance Eq Var where
+  (Var _ i) == (Var _ j) = i == j
+
+instance Ord Var where
+  compare (Var _ i) (Var _ j) = compare i j
+
+-- | A lens for '_varName'.
+--
+-- @
+-- varName ∷ Lens' 'Var' ('Maybe' 'String')
+-- @
+--
+varName
+  ∷ Functor f
+  ⇒ (Maybe String → f (Maybe String))
+  → Var
+  → f Var
+varName i (Var n j) =
+  (\n' → Var n' j)
+    <$> i n
+
+-- | A lens for '_varIndex'.
+--
+-- @
+-- varIndex ∷ Lens' 'Var' 'Int'
+-- @
+--
+varIndex
+  ∷ Functor f
+  ⇒ (Int → f Int)
+  → Var
+  → f Var
+varIndex i (Var n j) =
+  (\j' → Var n j')
+    <$> i j
+
+-- | Locally nameless terms with operators in @o@ at arity @n@.
+--
+data Tm (o ∷ [Nat] → *) (n ∷ Nat) where
+  Free ∷ Var → Tm o Z
+  Bound ∷ Int → Tm o Z
+  Abs ∷ Tm o n → Tm o (S n)
+  App ∷ o ns → HList (Tm o) ns → Tm o Z
+
+instance HEq1 o ⇒ HEq1 (Tm o) where
+  Free v1 === Free v2 = v1 == v2
+  Bound m === Bound n = m == n
+  Abs e1 === Abs e2 = e1 === e2
+  App o1 es1 === App o2 es2 = o1 === o2 && es1 === es2
+  _ === _ = False
+
+shiftVar
+  ∷ Var
+  → Int
+  → Tm o n
+  → Tm o n
+shiftVar v n = \case
+  Free v' → if v == v' then Bound n else Free v'
+  Bound m → Bound m
+  Abs e → Abs (shiftVar v (n + 1) e)
+  App p es → App p $ hmap (shiftVar v n) es
+
+addVar
+  ∷ Var
+  → Int
+  → Tm o n
+  → Tm o n
+addVar v n = \case
+  Free v' → Free v'
+  Bound m → if m == n then Free v else Bound m
+  Abs e → Abs (addVar v (n + 1) e)
+  App p es → App p $ hmap (addVar v n) es
+
+instance Show1 o ⇒ Abt Var o (Tm o) where
+  into = \case
+    V v → Free v
+    v :\ e → Abs (shiftVar v 0 e)
+    v :$ es → App v es
+
+  out = \case
+    Free v → return $ V v
+    Bound n → fail "bound variable occured in out"
+    Abs e → do
+      v ← fresh
+      return $ v :\ addVar v 0 e
+    App p es → return $ p :$ es
diff --git a/src/Abt/Tutorial.hs b/src/Abt/Tutorial.hs
new file mode 100644
--- /dev/null
+++ b/src/Abt/Tutorial.hs
@@ -0,0 +1,72 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE UnicodeSyntax #-}
+
+module Abt.Tutorial where
+
+import Abt.Class
+import Abt.Types
+import Abt.Concrete.LocallyNameless
+
+import Control.Applicative
+import Control.Monad.Trans
+import Control.Monad.Trans.State.Strict
+
+-- | We'll start off with a monad in which to manipulate ABTs; we'll need some
+-- state for fresh variable generation.
+--
+newtype M α
+  = M
+  { _M ∷ State Int α
+  } deriving (Functor, Applicative, Monad)
+
+-- | We'll run an ABT computation by starting the variable counter at @0@.
+--
+runM ∷ M α → α
+runM (M m) = evalState m 0
+
+-- | Check out the source to see fresh variable generation.
+--
+instance MonadVar Var M where
+  fresh = M $ do
+    n ← get
+    let n' = n + 1
+    put n'
+    return $ Var Nothing n'
+
+  named a = do
+    v ← fresh
+    return $ v { _varName = Just a }
+
+-- | Next, we'll define the operators for a tiny lambda calculus as a datatype
+-- indexed by arities.
+--
+data Lang ns where
+  Lam ∷ Lang '[S Z]
+  Ap ∷ Lang '[Z,Z]
+
+instance Show1 Lang where
+  show1 = \case
+    Lam → "lam"
+    Ap → "ap"
+
+instance HEq1 Lang where
+  Lam === Lam = True
+  Ap === Ap = True
+  _ === _ = False
+
+-- | Check out the source to see this example term: note that number of
+-- arguments and presence of abstractions is guaranteed by the types.  The
+-- representation is not scope-safe (i.e. free variables are permitted), but
+-- that's how we want it.
+--
+example ∷ M [Var]
+example = do
+  x ← fresh
+  y ← fresh
+  let tm = Lam $$ x \\ (Ap $$ var x :* var y :* Nil) :* Nil
+  freeVars tm
diff --git a/src/Abt/Types.hs b/src/Abt/Types.hs
new file mode 100644
--- /dev/null
+++ b/src/Abt/Types.hs
@@ -0,0 +1,11 @@
+-- | The core structures used to define the Abt signatures.
+--
+module Abt.Types
+( module Abt.Types.Nat
+, module Abt.Types.HList
+, module Abt.Types.View
+) where
+
+import Abt.Types.Nat
+import Abt.Types.HList
+import Abt.Types.View
diff --git a/src/Abt/Types/HList.hs b/src/Abt/Types/HList.hs
new file mode 100644
--- /dev/null
+++ b/src/Abt/Types/HList.hs
@@ -0,0 +1,43 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UnicodeSyntax #-}
+
+module Abt.Types.HList
+( HList(..)
+, hmap
+, htraverse
+, homogenizeA
+) where
+
+import Control.Applicative
+import Abt.Class.HEq1
+
+data HList ∷ (κ → *) → [κ] → * where
+  Nil ∷ HList el '[]
+  (:*) ∷ el x → HList el xs → HList el (x ': xs)
+infixr 8 :*
+
+hmap ∷ (∀ x. f x → g x) → HList f xs → HList g xs
+hmap η = \case
+  Nil → Nil
+  x :* xs → η x :* hmap η xs
+
+htraverse ∷ Applicative h ⇒ (∀ x. f x → h (g x)) → HList f xs → h (HList g xs)
+htraverse η = \case
+  Nil → pure Nil
+  x :* xs → (:*) <$> η x <*> htraverse η xs
+
+homogenizeA ∷ Applicative h ⇒ (∀ x. el x → h α) → HList el xs → h [α]
+homogenizeA η = \case
+  Nil → pure []
+  x :* xs → (:) <$> η x <*> homogenizeA η xs
+
+instance HEq1 el ⇒ HEq1 (HList el) where
+  Nil === Nil = True
+  (x :* xs) === (y :* ys) = x === y && xs === ys
+  _ === _ = False
+
diff --git a/src/Abt/Types/Nat.hs b/src/Abt/Types/Nat.hs
new file mode 100644
--- /dev/null
+++ b/src/Abt/Types/Nat.hs
@@ -0,0 +1,6 @@
+module Abt.Types.Nat where
+
+data Nat
+  = Z
+  | S !Nat
+
diff --git a/src/Abt/Types/View.hs b/src/Abt/Types/View.hs
new file mode 100644
--- /dev/null
+++ b/src/Abt/Types/View.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE UnicodeSyntax #-}
+
+module Abt.Types.View
+( View(..)
+, mapView
+) where
+
+import Abt.Types.Nat
+import Abt.Types.HList
+
+-- | @v@ is the type of variables; @o@ is the type of operators parameterized
+-- by arities; @n@ is the "higher type" of the term (i.e. a term has @n=0@, a
+-- single binding has @n=1@, etc.); @φ@ is the functor which interprets the
+-- inner structure of the view.
+--
+data View (v ∷ *) (o ∷ [Nat] → *) (n ∷ Nat) (φ ∷ Nat → *) where
+  V ∷ v → View v o Z φ
+  (:\) ∷ v → φ n → View v o (S n) φ
+  (:$) ∷ o ns → HList φ ns → View v o Z φ
+
+-- | Views are a (higher) functor.
+--
+mapView
+  ∷ (∀ j. φ j → ψ j) -- ^ a natural transformation @φ → ψ@
+  → View v o n φ -- ^ a view at @φ@
+  → View v o n ψ
+mapView eta = \case
+  V v → V v
+  v :\ e → v :\ eta e
+  o :$ es → o :$ hmap eta es