diff --git a/Language/ImProve.hs b/Language/ImProve.hs
--- a/Language/ImProve.hs
+++ b/Language/ImProve.hs
@@ -11,6 +11,7 @@
   , true
   , false
   , constant
+  , zero
   -- ** Variable Reference
   , ref
   -- ** Logical Operations
@@ -29,7 +30,7 @@
   , (<=.)
   , (>.)
   , (>=.)
-  -- ** Min, max, and limiting.
+  -- ** Min, Max, and Limiting
   , min_
   , minimum_
   , max_
@@ -46,7 +47,9 @@
   , linear
   -- * Hierarchical Scope
   , scope
-  -- * Variable Declarations
+  -- * Statements
+  , Stmt
+  -- ** Variable Declarations
   , bool
   , bool'
   , int
@@ -54,8 +57,6 @@
   , float
   , float'
   , input
-  -- * Statements
-  , Stmt
   -- ** Variable Assignment
   , (<==)
   -- ** Conditional Execution
@@ -67,91 +68,24 @@
   -- ** Assertions and  Assumptions
   , assert
   , assume
-  -- * Compilation
-  , compile
+  -- * Verification
+  , verify
+  -- * Code Generation
+  , code
   ) where
 
 import Control.Monad
-import Data.List
-import Data.Ratio
 
+import Language.ImProve.Core
+import qualified Language.ImProve.Verify as V
+import qualified Language.ImProve.Code   as C
+
 infixl 7 *., /., `div_`, `mod_`
 infix  4 ==., /=., <., <=., >., >=.
 infixl 3 &&.
 infixl 2 ||.
 infixr 1 <==
 
-type Name = String
-
--- | Variables.
-data V a
-  = V   [Name] a
-  | VIn [Name]
-
--- | All types.
-class AllE a where
-  showConst :: a -> String
-  showType  :: a -> String
-  zero      :: (Name -> a -> Stmt (V a)) -> a
-
-instance AllE Bool where
-  showConst a = case a of
-    True  -> "1"
-    False -> "0"
-  showType _ = "int"
-  zero = const False
-
-instance AllE Int where
-  showConst = show
-  showType _ = "int"
-  zero = const 0
-  
-instance AllE Float where
-  showConst = show
-  showType _ = "float"
-  zero = const 0
-
--- | Number types.
-class    AllE a => NumE a
-instance NumE Int
-instance NumE Float
-
--- | Core expressions.
-data E a where
-  Ref   :: AllE a => V a -> E a
-  Const :: AllE a => a -> E a
-  Add   :: NumE a => E a -> E a -> E a
-  Sub   :: NumE a => E a -> E a -> E a
-  Mul   :: NumE a => E a -> a -> E a
-  Div   :: NumE a => E a -> a -> E a
-  Mod   :: E Int -> Int -> E Int
-  Not   :: E Bool -> E Bool
-  And   :: E Bool -> E Bool -> E Bool
-  Or    :: E Bool -> E Bool -> E Bool
-  Eq    :: AllE a => E a -> E a -> E Bool
-  Lt    :: NumE a => E a -> E a -> E Bool
-  Gt    :: NumE a => E a -> E a -> E Bool
-  Le    :: NumE a => E a -> E a -> E Bool
-  Ge    :: NumE a => E a -> E a -> E Bool
-  Mux   :: AllE a => E Bool -> E a -> E a -> E a
-
-instance Show (E a) where show = undefined 
-instance Eq   (E a) where (==) = undefined
-
-instance (Num a, AllE a, NumE a) => Num (E a) where
-  (+) = Add
-  (-) = Sub
-  (*) = error "general multiplication not supported, use (*.)"
-  negate a = 0 - a
-  abs a = mux (a <. 0) (negate a) a
-  signum a = mux (a ==. 0) 0 $ mux (a <. 0) (-1) 1
-  fromInteger = Const . fromInteger
-
-instance Fractional (E Float) where
-  (/) = error "general division not supported, use (/.)"
-  recip a = 1 / a
-  fromRational r = Const $ fromInteger (numerator r) / fromInteger (denominator r)
-
 -- | True term.
 true :: E Bool
 true = Const True
@@ -283,33 +217,28 @@
 scope :: Name -> Stmt a -> Stmt a
 scope name (Stmt f0) = Stmt f1
   where
-  f1 (path, items, statement) = (a, (path, Scope name items0 : items, statement1))
+  f1 (path, statement) = (a, (path, statement1))
     where
-    (a, (_, items0, statement1)) = f0 (path ++ [name], [], statement)
+    (a, (_, statement1)) = f0 (path ++ [name], statement)
   
-get :: Stmt ([Name], [Scope], Statement)
+get :: Stmt ([Name], Statement)
 get = Stmt $ \ a -> (a, a)
 
 getPath :: Stmt [Name]
 getPath = do
-  (path, _, _) <- get
+  (path, _) <- get
   return path
 
-put :: ([Name], [Scope], Statement) -> Stmt ()
-put a = Stmt $ \ _ -> ((), a)
-
 var :: AllE a => Name -> a -> Stmt (V a)
 var name init = do
-  (path, items, stmt) <- get
-  put (path, Variable name (showType init) (showConst init) : items, stmt)
-  return $ V (path ++ [name]) init
+  path <- getPath
+  return $ V False (path ++ [name]) init
 
 -- | Input variable declaration.  Input variables are initialized to 0.
 input  :: AllE a => (Name -> a -> Stmt (V a)) -> Name -> Stmt (E a)
 input f name = do
-  (path, items, stmt) <- get
-  put (path, Variable name (showType $ zero f) (showConst $ zero f) : items, stmt)
-  return $ ref $ VIn (path ++ [name])
+  path <- getPath
+  return $ ref $ V True (path ++ [name]) $ zero f
 
 -- | Boolean variable declaration.
 bool :: Name -> Bool -> Stmt (V Bool)
@@ -352,18 +281,8 @@
 decr :: V Int -> Stmt ()
 decr a = a <== ref a - 1
 
-data Statement
-  = AssignBool  (V Bool ) (E Bool )
-  | AssignInt   (V Int  ) (E Int  )
-  | AssignFloat (V Float) (E Float)
-  | Branch (E Bool) Statement Statement
-  | Sequence Statement Statement
-  | Assert [Name] (E Bool)
-  | Assume [Name] (E Bool)
-  | Null
-
 -- | The Stmt monad holds variable declarations and statements.
-data Stmt a = Stmt (([Name], [Scope], Statement) -> (a, ([Name], [Scope], Statement)))
+data Stmt a = Stmt (([Name], Statement) -> (a, ([Name], Statement)))
 
 instance Monad Stmt where
   return a = Stmt $ \ s -> (a, s)
@@ -375,10 +294,10 @@
       Stmt f4 = f2 a
 
 statement :: Statement -> Stmt ()
-statement a = Stmt $ \ (path, scope, statement) -> ((), (path, scope, Sequence statement a))
+statement a = Stmt $ \ (path, statement) -> ((), (path, Sequence statement a))
 
-evalStmt :: [Name] -> [Scope] -> Stmt () -> ([Name], [Scope], Statement)
-evalStmt path items (Stmt f) = snd $ f (path, items, Null)
+evalStmt :: [Name] -> Stmt () -> ([Name], Statement)
+evalStmt path (Stmt f) = snd $ f (path, Null)
 
 class    Assign a     where (<==) :: V a -> E a -> Stmt ()
 instance Assign Bool  where a <== b = statement $ AssignBool  a b
@@ -398,100 +317,22 @@
   statement $ Assume (path ++ [a]) b
 
 -- | Conditional if-else.
-ifelse :: E Bool -> Stmt () -> Stmt () -> Stmt ()
-ifelse cond onTrue onFalse = do
-  (path, items, stmt) <- get
-  let (_, items1, stmt1) = evalStmt path items  onTrue
-      (_, items2, stmt2) = evalStmt path items1 onFalse
-  put (path, items2, stmt)
-  statement $ Branch cond stmt1 stmt2
-
--- | Conditional without the else.
-if_ :: E Bool -> Stmt () -> Stmt()
-if_ cond stmt = ifelse cond stmt $ return ()
-
--- | Generate C code.
-compile :: Name -> Stmt () -> IO ()
-compile name program = do
-  writeFile (name ++ ".c") $
-       "// Generated by ImProve.\n\n"
-    ++ "#include <assert.h>\n\n"
-    ++ codeVariables True scope ++ "\n"
-    ++ "void " ++ name ++ "() {\n"
-    ++ indent (codeStmt stmt)
-    ++ "}\n\n"
-  writeFile (name ++ ".h") $
-       "// Generated by ImProve.\n\n"
-    ++ codeVariables False scope ++ "\n"
-    ++ "void " ++ name ++ "(void);\n\n"
-  where
-  (_, items, stmt) = evalStmt [name ++ "Variables"] [] program
-  scope = Scope (name ++ "Variables") items
-
-varName :: V a -> String
-varName a = intercalate "." names
-  where
-  names = case a of
-    V   names _ -> names
-    VIn names   -> names
-
-codeStmt :: Statement -> String
-codeStmt a = case a of
-  AssignBool  a b -> varName a ++ " = " ++ codeExpr b ++ ";\n"
-  AssignInt   a b -> varName a ++ " = " ++ codeExpr b ++ ";\n"
-  AssignFloat a b -> varName a ++ " = " ++ codeExpr b ++ ";\n"
-  Branch a b Null -> "if (" ++ codeExpr a ++ ") {\n" ++ indent (codeStmt b) ++ "}\n"
-  Branch a b c    -> "if (" ++ codeExpr a ++ ") {\n" ++ indent (codeStmt b) ++ "}\nelse {\n" ++ indent (codeStmt c) ++ "}\n"
-  Sequence a b -> codeStmt a ++ codeStmt b
-  Assert names a -> "// assert " ++ intercalate "." names ++ "\nassert(" ++ codeExpr a ++ ");\n"
-  Assume names a -> "// assume " ++ intercalate "." names ++ "\nassert(" ++ codeExpr a ++ ");\n"
-  Null -> ""
-
-codeExpr :: E a -> String
-codeExpr a = case a of
-  Ref a -> varName a
-  Const a -> showConst a
-  Add a b -> group [codeExpr a, "+", codeExpr b]
-  Sub a b -> group [codeExpr a, "-", codeExpr b]
-  Mul a b -> group [codeExpr a, "*", showConst b]
-  Div a b -> group [codeExpr a, "/", showConst b]
-  Mod a b -> group [codeExpr a, "%", showConst b]
-  Not a   -> group ["!", codeExpr a]
-  And a b -> group [codeExpr a, "&&",  codeExpr b]
-  Or  a b -> group [codeExpr a, "||",  codeExpr b]
-  Eq  a b -> group [codeExpr a, "==",  codeExpr b]
-  Lt  a b -> group [codeExpr a, "<",   codeExpr b]
-  Gt  a b -> group [codeExpr a, ">",   codeExpr b]
-  Le  a b -> group [codeExpr a, "<=",  codeExpr b]
-  Ge  a b -> group [codeExpr a, ">=",  codeExpr b]
-  Mux a b c -> group [codeExpr a, "?", codeExpr b, ":", codeExpr c] 
-  where
-  group :: [String] -> String
-  group a = "(" ++ intercalate " " a ++ ")"
-
-indent :: String -> String
-indent = unlines . map ("  " ++) . lines
-
-data Scope
-  = Scope Name [Scope]
-  | Variable Name String String  -- name type init
-  deriving Eq
+ifelse :: Name -> E Bool -> Stmt () -> Stmt () -> Stmt ()
+ifelse name cond onTrue onFalse = do
+  path <- getPath
+  let (_, stmt1) = evalStmt path onTrue
+      (_, stmt2) = evalStmt path onFalse
+  statement $ Branch (path ++ [name]) cond stmt1 stmt2
 
-instance Ord Scope where
-  compare a b = case (a, b) of
-    (Scope a _, Scope b _) -> compare a b
-    (Variable a _ _, Variable b _ _) -> compare a b
-    (Variable _ _ _, Scope _ _) -> LT
-    (Scope _ _, Variable _ _ _) -> GT
+-- | Conditional if without the else.
+if_ :: Name -> E Bool -> Stmt () -> Stmt()
+if_ name cond stmt = ifelse name cond stmt $ return ()
 
-codeVariables :: Bool -> Scope -> String
-codeVariables define a = (if define then "" else "extern ") ++ init (init (f1 a)) ++ (if define then " =\n" ++ f2 a else "") ++ ";\n"
-  where
-  f1 a = case a of
-    Scope     name items -> "struct {  // " ++ name ++ "\n" ++ indent (concatMap f1 $ sort items) ++ "} " ++ name ++ ";\n"
-    Variable  name typ _ -> typ ++ " " ++ name ++ ";\n"
+-- | Verify a program.
+verify :: Stmt () -> IO (Maybe Bool)
+verify program = V.verify $ snd $ evalStmt [] program
 
-  f2 a = case a of
-    Scope    name items  -> "{  // " ++ name ++ "\n" ++ indent (intercalate ",\n" (map f2 $ sort items)) ++ "\n}"
-    Variable name _ init -> "/* " ++ name ++ " */  " ++ init
+-- | Generate C code.
+code :: Name -> Stmt () -> IO ()
+code name program = C.code name $ snd $ evalStmt [name ++ "Variables"] program
 
diff --git a/Language/ImProve/Code.hs b/Language/ImProve/Code.hs
new file mode 100644
--- /dev/null
+++ b/Language/ImProve/Code.hs
@@ -0,0 +1,118 @@
+module Language.ImProve.Code (code) where
+
+import Data.List
+import Text.Printf
+
+import Language.ImProve.Core
+import Language.ImProve.Tree hiding (Branch)
+import qualified Language.ImProve.Tree as T
+
+-- | Generate C code.
+code :: Name -> Statement -> IO ()
+code name stmt = do
+  writeFile (name ++ ".c") $
+       "// Generated by ImProve.\n\n"
+    ++ "#include <assert.h>\n\n"
+    ++ codeVariables True scope ++ "\n"
+    ++ "void " ++ name ++ "() {\n"
+    ++ indent (codeStmt stmt)
+    ++ "}\n\n"
+  writeFile (name ++ ".h") $
+       "// Generated by ImProve.\n\n"
+    ++ codeVariables False scope ++ "\n"
+    ++ "void " ++ name ++ "(void);\n\n"
+  where
+  [scope] = tree (\ (path, _, _, _) -> path) $ varsInStmt stmt
+
+varName :: V a -> String
+varName a = intercalate "." names
+  where
+  names = case a of
+    V _ names _ -> names
+
+codeStmt :: Statement -> String
+codeStmt a = case a of
+  AssignBool  a b -> varName a ++ " = " ++ codeExpr b ++ ";\n"
+  AssignInt   a b -> varName a ++ " = " ++ codeExpr b ++ ";\n"
+  AssignFloat a b -> varName a ++ " = " ++ codeExpr b ++ ";\n"
+  Branch path a b Null -> "// if_ "    ++ intercalate "." path ++ "\nif (" ++ codeExpr a ++ ") {\n" ++ indent (codeStmt b) ++ "}\n"
+  Branch path a b c    -> "// ifelse " ++ intercalate "." path ++ "\nif (" ++ codeExpr a ++ ") {\n" ++ indent (codeStmt b) ++ "}\nelse {\n" ++ indent (codeStmt c) ++ "}\n"
+  Sequence a b -> codeStmt a ++ codeStmt b
+  Assert path a -> "// assert " ++ intercalate "." path ++ "\nassert(" ++ codeExpr a ++ ");\n"
+  Assume path a -> "// assume " ++ intercalate "." path ++ "\nassert(" ++ codeExpr a ++ ");\n"
+  Null -> ""
+
+codeExpr :: E a -> String
+codeExpr a = case a of
+  Ref a -> varName a
+  Const a -> showConst a
+  Add a b -> group [codeExpr a, "+", codeExpr b]
+  Sub a b -> group [codeExpr a, "-", codeExpr b]
+  Mul a b -> group [codeExpr a, "*", showConst b]
+  Div a b -> group [codeExpr a, "/", showConst b]
+  Mod a b -> group [codeExpr a, "%", showConst b]
+  Not a   -> group ["!", codeExpr a]
+  And a b -> group [codeExpr a, "&&",  codeExpr b]
+  Or  a b -> group [codeExpr a, "||",  codeExpr b]
+  Eq  a b -> group [codeExpr a, "==",  codeExpr b]
+  Lt  a b -> group [codeExpr a, "<",   codeExpr b]
+  Gt  a b -> group [codeExpr a, ">",   codeExpr b]
+  Le  a b -> group [codeExpr a, "<=",  codeExpr b]
+  Ge  a b -> group [codeExpr a, ">=",  codeExpr b]
+  Mux a b c -> group [codeExpr a, "?", codeExpr b, ":", codeExpr c] 
+  where
+  group :: [String] -> String
+  group a = "(" ++ intercalate " " a ++ ")"
+
+indent :: String -> String
+indent = unlines . map ("  " ++) . lines
+
+indent' :: String -> String
+indent' a = case lines a of
+  [] -> []
+  (a:b) -> a ++ "\n" ++ indent (unlines b)
+
+codeVariables :: Bool -> (Tree Name ([Name], Bool, String, String)) -> String
+codeVariables define a = (if define then "" else "extern ") ++ init (init (f1 a)) ++ (if define then " =\n  " ++ f2 a else "") ++ ";\n"
+  where
+  f1 a = case a of
+    T.Branch name items -> "struct {  // " ++ name ++ "\n" ++ indent (concatMap f1 items) ++ "} " ++ name ++ ";\n"
+    Leaf name (_, input, typ, _) -> printf "%-5s %-25s;%s\n" typ name (if input then "  // input" else "")
+
+  f2 a = case a of
+    T.Branch name items -> indent' $ "{ " ++ (intercalate ", " $ map f2 items) ++ "}  // " ++ name ++ "\n"
+    Leaf name (_, _, _, init) -> printf "%-15s  // %s\n" init name
+
+varInfo :: AllE a => V a -> ([Name], Bool, String, String)
+varInfo (V input path a) = (path, input, showType a, showConst a)
+
+varsInStmt :: Statement -> [([Name], Bool, String, String)] -- (path, isInput, type, init)
+varsInStmt a = case a of
+  AssignBool  a b -> nub $ varInfo a : varsInExpr b
+  AssignInt   a b -> nub $ varInfo a : varsInExpr b
+  AssignFloat a b -> nub $ varInfo a : varsInExpr b
+  Branch _ a b c  -> nub $ varsInExpr a ++ varsInStmt b ++ varsInStmt c
+  Sequence a b    -> nub $ varsInStmt a ++ varsInStmt b
+  Assert _ a      -> varsInExpr a
+  Assume _ a      -> varsInExpr a
+  Null            -> []
+
+varsInExpr :: E a -> [([Name], Bool, String, String)] -- (path, isInput, type, init)
+varsInExpr a = case a of
+  Ref a     -> [varInfo a]
+  Const _   -> []
+  Add a b   -> varsInExpr a ++ varsInExpr b
+  Sub a b   -> varsInExpr a ++ varsInExpr b
+  Mul a _   -> varsInExpr a
+  Div a _   -> varsInExpr a
+  Mod a _   -> varsInExpr a
+  Not a     -> varsInExpr a
+  And a b   -> varsInExpr a ++ varsInExpr b
+  Or  a b   -> varsInExpr a ++ varsInExpr b
+  Eq  a b   -> varsInExpr a ++ varsInExpr b
+  Lt  a b   -> varsInExpr a ++ varsInExpr b
+  Gt  a b   -> varsInExpr a ++ varsInExpr b
+  Le  a b   -> varsInExpr a ++ varsInExpr b
+  Ge  a b   -> varsInExpr a ++ varsInExpr b
+  Mux a b c -> varsInExpr a ++ varsInExpr b ++ varsInExpr c
+
diff --git a/Language/ImProve/Core.hs b/Language/ImProve/Core.hs
new file mode 100644
--- /dev/null
+++ b/Language/ImProve/Core.hs
@@ -0,0 +1,86 @@
+module Language.ImProve.Core
+  ( E (..)
+  , V (..)
+  , Name
+  , AllE (..)
+  , NumE
+  , Statement (..)
+  ) where
+
+import Data.Ratio
+
+type Name = String
+
+data V a = V Bool [Name] a
+
+class AllE a where
+  showConst :: a -> String
+  showType  :: a -> String
+  zero      :: (Name -> a -> m (V a)) -> a
+
+instance AllE Bool where
+  showConst a = case a of
+    True  -> "1"
+    False -> "0"
+  showType _ = "int"
+  zero = const False
+
+instance AllE Int where
+  showConst = show
+  showType _ = "int"
+  zero = const 0
+  
+instance AllE Float where
+  showConst = show
+  showType _ = "float"
+  zero = const 0
+
+class    AllE a => NumE a
+instance NumE Int
+instance NumE Float
+
+data E a where
+  Ref   :: AllE a => V a -> E a
+  Const :: AllE a => a -> E a
+  Add   :: NumE a => E a -> E a -> E a
+  Sub   :: NumE a => E a -> E a -> E a
+  Mul   :: NumE a => E a -> a -> E a
+  Div   :: NumE a => E a -> a -> E a
+  Mod   :: E Int -> Int -> E Int
+  Not   :: E Bool -> E Bool
+  And   :: E Bool -> E Bool -> E Bool
+  Or    :: E Bool -> E Bool -> E Bool
+  Eq    :: AllE a => E a -> E a -> E Bool
+  Lt    :: NumE a => E a -> E a -> E Bool
+  Gt    :: NumE a => E a -> E a -> E Bool
+  Le    :: NumE a => E a -> E a -> E Bool
+  Ge    :: NumE a => E a -> E a -> E Bool
+  Mux   :: AllE a => E Bool -> E a -> E a -> E a
+
+instance Show (E a) where show = undefined 
+instance Eq   (E a) where (==) = undefined
+
+instance (Num a, AllE a, NumE a) => Num (E a) where
+  (+) = Add
+  (-) = Sub
+  (*) = error "general multiplication not supported, use (*.)"
+  negate a = 0 - a
+  abs a = Mux (Lt a 0) (negate a) a
+  signum a = Mux (Eq a 0) 0 $ Mux (Lt a 0) (-1) 1
+  fromInteger = Const . fromInteger
+
+instance Fractional (E Float) where
+  (/) = error "general division not supported, use (/.)"
+  recip a = 1 / a
+  fromRational r = Const $ fromInteger (numerator r) / fromInteger (denominator r)
+
+data Statement
+  = AssignBool  (V Bool ) (E Bool )
+  | AssignInt   (V Int  ) (E Int  )
+  | AssignFloat (V Float) (E Float)
+  | Branch      [Name] (E Bool) Statement Statement
+  | Sequence    Statement Statement
+  | Assert      [Name] (E Bool)
+  | Assume      [Name] (E Bool)
+  | Null
+
diff --git a/Language/ImProve/Examples.hs b/Language/ImProve/Examples.hs
new file mode 100644
--- /dev/null
+++ b/Language/ImProve/Examples.hs
@@ -0,0 +1,57 @@
+-- | ImProve examples.
+module Language.ImProve.Examples
+  ( gcd'
+  , gcdMain
+  , gcdBuild
+  ) where
+
+import Language.ImProve
+
+-- | Computes the greatest common divison of two integers.
+--   Returns true if the computation is done, and the result.
+gcd' :: E Int -> E Int -> Stmt (E Bool, E Int)
+gcd' a b = do
+  a0 <- int "a0" 0  -- Copy of input 'a'.
+  b0 <- int "b0" 0  -- Copy of input 'b'.
+  a1 <- int "a1" 0  -- Working copy of 'a'.
+  b1 <- int "b1" 0  -- Working copy of 'b'.
+
+  -- A new input to process.
+  if_ "startNew" (a /=. ref a0 ||. b /=. ref b0) $ do
+    a0 <== a
+    b0 <== b
+    a1 <== a
+    b1 <== b
+
+  -- Reduce a1.
+  if_ "reduceA" (ref a1 >. ref b1) $ do
+    a1 <== ref a1 - ref b1
+
+  -- Reduce b1.
+  if_ "reduceB" (ref b1 >. ref a1) $ do
+    b1 <== ref b1 - ref a1
+
+  -- Done if a1 == b1.
+  return (ref a1 ==. ref b1, ref a1)
+
+
+-- | A top level wrapper for gcd'.
+gcdMain :: Stmt ()
+gcdMain = do
+  a <- input int "a"  -- Input variable 'a'.
+  b <- input int "b"  -- Input variable 'b'.
+  done   <- bool "done"   False  -- Variable signalling completion.
+  result <- int  "result" 0      -- Result of GCD.
+
+  -- Call gcd' in its own scope.  (Scopes prevent variable name collisions.)
+  (done', result') <- scope "gcd" $ gcd' a b
+
+  -- Bind the results to the output variables.
+  done   <== done'
+  result <== result'
+
+
+-- | Build the gcdMain code (i.e. gcd.c, gcd.h).
+gcdBuild :: IO ()
+gcdBuild = code "gcd" gcdMain
+
diff --git a/Language/ImProve/Tree.hs b/Language/ImProve/Tree.hs
new file mode 100644
--- /dev/null
+++ b/Language/ImProve/Tree.hs
@@ -0,0 +1,46 @@
+-- | Building hierarchy from unstructured hierarchical paths.
+module Language.ImProve.Tree
+  ( Tree (..)
+  , tree
+  ) where
+
+import Data.Function
+import Data.List
+
+data Tree a b
+  = Branch a [Tree a b]
+  | Leaf   a b
+
+tree :: (Eq a, Ord a) => (b -> [a]) -> [b] -> [Tree a b]
+tree path leaves = foldl mergeTrees [] [ singleTree (path leaf) leaf | leaf <- leaves ]
+
+label :: Tree a b -> a
+label (Branch a _) = a
+label (Leaf   a _) = a
+
+isBranch :: Tree a b -> Bool
+isBranch (Branch _ _) = True
+isBranch _ = False
+
+singleTree :: [a] -> b -> Tree a b
+singleTree [] _ = undefined
+singleTree [a] b = Leaf a b
+singleTree (a:b) c = Branch a [singleTree b c]
+
+mergeTrees :: (Eq a, Ord a) => [Tree a b] -> Tree a b -> [Tree a b]
+mergeTrees trees t@(Leaf _ _) = insertTree t trees
+mergeTrees trees t@(Branch n branches) = case find' (\ t -> isBranch t && label t == n) trees of
+    Nothing -> insertTree t trees
+    Just (Branch n trees1, trees2) -> insertTree (Branch n (foldl mergeTrees trees1 branches)) trees2
+    Just (Leaf _ _, _) -> undefined
+
+insertTree :: Ord a => Tree a b -> [Tree a b] -> [Tree a b]
+insertTree a b = insertBy (compare `on` label) a b
+
+find' :: (a -> Bool) -> [a] -> Maybe (a, [a])
+find' _ [] = Nothing
+find' f (a:b) | f a = Just (a, b)
+              | otherwise = do
+  (found, rest) <- find' f b
+  return (found, a : rest)
+
diff --git a/Language/ImProve/Verify.hs b/Language/ImProve/Verify.hs
new file mode 100644
--- /dev/null
+++ b/Language/ImProve/Verify.hs
@@ -0,0 +1,7 @@
+module Language.ImProve.Verify (verify) where
+
+import Language.ImProve.Core
+
+verify :: Statement -> IO (Maybe Bool)
+verify _ = putStrLn "verification not implemented yet" >> return Nothing
+
diff --git a/improve.cabal b/improve.cabal
--- a/improve.cabal
+++ b/improve.cabal
@@ -1,9 +1,9 @@
 name:    improve
-version: 0.0.1
+version: 0.0.2
 
 category: Language
 
-synopsis: A simple imperative programming language for embedded applications.
+synopsis: An imperative, verifiable programming language for embedded applications.
 
 description:
     TODO
@@ -26,6 +26,11 @@
 
     exposed-modules:
         Language.ImProve
+        Language.ImProve.Code
+        Language.ImProve.Core
+        Language.ImProve.Examples
+        Language.ImProve.Tree
+        Language.ImProve.Verify
 
     extensions: GADTs, FlexibleInstances