diff --git a/Language/Atom/Code.hs b/Language/Atom/Code.hs
--- a/Language/Atom/Code.hs
+++ b/Language/Atom/Code.hs
@@ -11,7 +11,9 @@
 import Data.Char
 import Data.List
 import Data.Maybe
+import Data.Word
 import System.IO
+import Unsafe.Coerce
 
 import Language.Atom.Elaboration
 import Language.Atom.Expressions
@@ -34,30 +36,19 @@
   , cPostCode = ""
   }
 
-declareMemory :: Config -> UV -> String
-declareMemory config (UV id name (Local init)) = cType config (constType init) ++ " " ++ e id ++ " = " ++ c ++ ";  /* " ++ name ++ " */\n"
-  where
-  c = case init of
-    CBool   c -> if c then "1" else "0" 
-    CInt8   c -> show c
-    CInt16  c -> show c
-    CInt32  c -> show c
-    CInt64  c -> show c
-    CWord8  c -> show c
-    CWord16 c -> show c
-    CWord32 c -> show c
-    CWord64 c -> show c
-    CFloat  c -> show c
-    CDouble c -> show c
-declareMemory _ (UV _ _ (External _)) = ""
-
-declareUE :: Config -> String -> (UE, String) -> String
-declareUE config d (ue, n) = case ue of
-  UVRef _              -> ""
-  UConst (CBool True ) -> d ++ "const " ++ cType config (ueType ue) ++ " " ++ n ++ " = 1;\n"
-  UConst (CBool False) -> d ++ "const " ++ cType config (ueType ue) ++ " " ++ n ++ " = 0;\n"
-  UConst c             -> d ++ "const " ++ cType config (ueType ue) ++ " " ++ n ++ " = " ++ show c ++ ";\n"
-  _                    -> d ++             cType config (ueType ue) ++ " " ++ n ++ ";\n"
+showConst :: Const -> String
+showConst c = case c of
+  CBool   c -> if c then "1" else "0" 
+  CInt8   c -> show c
+  CInt16  c -> show c
+  CInt32  c -> show c
+  CInt64  c -> show c
+  CWord8  c -> show c
+  CWord16 c -> show c
+  CWord32 c -> show c
+  CWord64 c -> show c
+  CFloat  c -> show c
+  CDouble c -> show c
 
 -- | ANSI C type naming rules.
 cTypes :: Type -> String
@@ -90,17 +81,15 @@
   Double -> "double"
 
 codeUE :: Config -> [(UE, String)] -> String -> (UE, String) -> String
-codeUE config ues d (ue, n) = case ue of
-  UConst _       -> ""
-  UVRef _        -> ""
-  _              -> d ++ n ++ " = " ++ basic operands ++ ";\n"
+codeUE config ues d (ue, n) = d ++ cType config (typeOf ue) ++ " " ++ n ++ " = " ++ basic operands ++ ";\n"
   where
   operands = map (fromJust . flip lookup ues) $ ueUpstream ue
   basic :: [String] -> String
   basic operands = case ue of
-    UVRef _              -> error "Code.ueStmt: should not get here."
-    UCast _ _            -> "(" ++ cType config (ueType ue) ++ ") (" ++ a ++ ")"
-    UConst _             -> error "Code.ueStmt: should not get here."
+    UVRef (UV (Array ua@(UA _ n _) _)) -> arrayIndex config ua a ++ " /* " ++ n ++ " */ "
+    UVRef (UV (External n _)) -> n
+    UCast _ _            -> "(" ++ cType config (typeOf ue) ++ ") " ++ a
+    UConst c             -> showConst c
     UAdd _ _             ->  a ++ " + " ++ b
     USub _ _             ->  a ++ " - " ++ b
     UMul _ _             ->  a ++ " * " ++ b
@@ -124,8 +113,8 @@
     b = operands !! 1
     c = operands !! 2
 
-writeC :: Name -> Config -> [[[Rule]]] -> [UV] -> IO ()
-writeC name config periods uvs = do
+writeC :: Name -> Config -> [[[Rule]]] -> ([Const], [Const], [Const], [Const]) -> IO ()
+writeC name config periods (init8, init16, init32, init64) = do
   putStrLn $ "Writing C code (" ++ name ++ ".c)..."
   writeFile (name ++ ".c") c
   putStrLn $ "Writing coverage data description (" ++ name' ++ "CoverageData.hs)..."
@@ -134,11 +123,11 @@
   name' = toUpper (head name) : tail name
   c = unlines
     [ cPreCode config
-    , cType config Word64 ++ " __clock = 0;"
-    , "const " ++ cType config Word32 ++ " __coverage_len = " ++ show covLen ++ ";"
-    , cType config Word32 ++ " __coverage[" ++ show covLen ++ "] = {" ++ drop 2 (concat $ replicate covLen ", 0") ++ "};"
-    , cType config Word32 ++ " __coverage_index = 0;"
-    , concatMap (declareMemory config) uvs
+    , "static " ++ cType config Word64 ++ " __clock = 0;"
+    , "static const " ++ cType config Word32 ++ " __coverage_len = " ++ show covLen ++ ";"
+    , "static " ++ cType config Word32 ++ " __coverage[" ++ show covLen ++ "] = {" ++ drop 2 (concat $ replicate covLen ", 0") ++ "};"
+    , "static " ++ cType config Word32 ++ " __coverage_index = 0;"
+    , memoryInit config Word8  init8 ++ memoryInit config Word16 init16 ++ memoryInit config Word32 init32 ++ memoryInit config Word64 init64
     , concatMap (codeRule config topo') $ concat $ concat periods
     , "void " ++ (if null (cFuncName config) then name else cFuncName config) ++ "(void) {"
     , concatMap codePeriod $ zip [1..] periods
@@ -157,29 +146,65 @@
     , "coverageData = " ++ show [ (ruleName r, (div (ruleId r) 32, mod (ruleId r) 32)) | r <- rules ]
     ]
 
-  topo' = topo $ maximum (map (\ (UV i _ _) -> i) uvs) + 1
+  topo' = topo 0
   covLen = 1 + div (maximum $ map ruleId rules) 32
 
+memoryInit :: Config -> Type -> [Const] -> String
+memoryInit _ _ [] = ""
+memoryInit config t init = "static " ++ cType config t ++ " " ++ memory t ++ "[" ++ show (length init) ++ "] = {" ++ drop 2 (concat [", " ++ format a | a <- init ]) ++ "};\n"
+  where
+  format :: Const -> String
+  format c = case c of
+    CBool True  -> "1"
+    CBool False -> "0"
+    CInt8   a   -> show a
+    CInt16  a   -> show a
+    CInt32  a   -> show a
+    CInt64  a   -> show a
+    CWord8  a   -> show a
+    CWord16 a   -> show a
+    CWord32 a   -> show a
+    CWord64 a   -> show a
+    CFloat  a   -> show $ floatBits  a
+    CDouble a   -> show $ doubleBits a
+
+floatBits :: Float -> Word32
+floatBits = unsafeCoerce
+
+doubleBits :: Double -> Word64
+doubleBits = unsafeCoerce
+
+memory :: Width a => a -> String
+memory a = "__memory" ++ show (if width a == 1 then 8 else width a)
+
 codeRule :: Config -> ([UE] -> [(UE, String)]) -> Rule -> String
 codeRule config topo rule = 
   "/* " ++ show rule ++ " */\n" ++
-  "void __r" ++ show (ruleId rule) ++ "(void) {\n" ++
-  concatMap (declareUE config     "  ") ues ++
+  "static void __r" ++ show (ruleId rule) ++ "(void) {\n" ++
   concatMap (codeUE    config ues "  ") ues ++
   "  if (" ++ id (ruleEnable rule) ++ ") {\n" ++
   concatMap codeAction (ruleActions rule) ++
   "    __coverage[" ++ covWord ++ "] = __coverage[" ++ covWord ++ "] | (1 << " ++ covBit ++ ");\n" ++
   "  }\n" ++
-  concatMap (\ (uv, ue) -> "  " ++ v uv ++ " = " ++ id ue ++ ";\n") (ruleAssigns rule) ++
+  concatMap codeAssign (ruleAssigns rule) ++
   "}\n\n"
   where
-  ues = topo $ ruleEnable rule : snd (unzip (ruleAssigns rule)) ++ concat (snd (unzip (ruleActions rule)))
+  ues = topo $ allUEs rule
   id ue = fromJust $ lookup ue ues
+
   codeAction :: (([String] -> String), [UE]) -> String
   codeAction (f, args) = "    " ++ f (map id args) ++ ";\n"
+
   covWord = show $ div (ruleId rule) 32
   covBit  = show $ mod (ruleId rule) 32
 
+  codeAssign :: (UV, UE) -> String
+  codeAssign (UV (Array ua@(UA _ n _) i), ue) = "  " ++ arrayIndex config ua (id i) ++ " = " ++ id ue ++ ";  /* " ++ n ++ " */\n"
+  codeAssign (UV (External n _), ue) = "  " ++ n ++ " = " ++ id ue ++ ";\n"
+
+arrayIndex :: Config -> UA -> String -> String
+arrayIndex config (UA addr _ c) i = "((" ++ cType config (typeOf (head c)) ++ " *) (" ++ memory (head c) ++ " + " ++ show addr ++ "))[" ++ i ++ "]"
+
 codePeriod :: (Int, [[Rule]]) -> String
 codePeriod (period, cycles) = concatMap (codeCycle period) $ zip [0..] cycles
 
@@ -194,9 +219,12 @@
 e :: Int -> String
 e i = "__" ++ show i
 
-v :: UV -> String
-v (UV i _ (Local _)) = e i
-v (UV _ n (External _)) = n
+allUEs :: Rule -> [UE]
+allUEs rule = ruleEnable rule : concat [ ue : index uv | (uv, ue) <- ruleAssigns rule ] ++ concat (snd (unzip (ruleActions rule)))
+  where
+  index :: UV -> [UE]
+  index (UV (Array _ ue)) = [ue]
+  index _ = []
 
 -- | Topologically sorts a list of expressions and subexpressions.
 topo :: Int -> [UE] -> [(UE, String)]
@@ -205,14 +233,9 @@
   (_, ues') = foldl collect (start, []) ues
   collect :: (Int, [(UE, String)]) -> UE -> (Int, [(UE, String)])
   collect (n, ues) ue | any ((== ue) . fst) ues = (n, ues)
-  collect (n, ues) ue = case ue of
-    UVRef (UV i _ (Local    _)) -> (n, (ue, e i) : ues)
-    UVRef (UV _ a (External _)) -> (n, (ue, a)   : ues)
-    _                -> (n' + 1, (ue, e n') : ues')
-      where
-      (n', ues') = foldl collect (n, ues) $ ueUpstream ue
+  collect (n, ues) ue = (n' + 1, (ue, e n') : ues') where (n', ues') = foldl collect (n, ues) $ ueUpstream ue
 
 -- | Number of UE's computed in rule.
 ruleComplexity :: Rule -> Int
-ruleComplexity rule = length $ topo 0 $ ruleEnable rule : snd (unzip (ruleAssigns rule)) ++ concat (snd (unzip (ruleActions rule)))
+ruleComplexity rule = length $ topo 0 $ allUEs rule
 
diff --git a/Language/Atom/Compile.hs b/Language/Atom/Compile.hs
--- a/Language/Atom/Compile.hs
+++ b/Language/Atom/Compile.hs
@@ -12,7 +12,6 @@
 import Language.Atom.Scheduling
 import Language.Atom.Elaboration
 import Language.Atom.Language hiding (Atom)
-import Language.Atom.Verify ()
 
 -- | Compiles an atom description to C.
 compile :: Name -> Config -> Atom () -> IO ()
@@ -20,18 +19,12 @@
   r <- elaborate name atom
   case r of
     Nothing -> putStrLn "ERROR: Design rule checks failed." >> exitWith (ExitFailure 1)
-    Just (rules, uvs, _) -> do
+    Just (rules, init) -> do
       r <- schedule name rules
       case r of
         Nothing -> putStrLn "ERROR: Rule scheduling failed." >> exitWith (ExitFailure 1)
         Just schedule -> do
-          {-
-          when (depth > 0) $ do
-            putStrLn $ "Starting bounded model checking with depth " ++ show depth ++ "..."
-            v <- mapM (verify depth schedule uvs) asserts 
-            when (not $ and v) $ putStrLn "ERROR: Verification failed." >> exitWith (ExitFailure 1)
-          -}
           putStrLn "Starting code generation..."
           hFlush stdout
-          writeC name config schedule uvs
+          writeC name config schedule init
 
diff --git a/Language/Atom/Elaboration.hs b/Language/Atom/Elaboration.hs
--- a/Language/Atom/Elaboration.hs
+++ b/Language/Atom/Elaboration.hs
@@ -13,6 +13,7 @@
   , elaborate
   , var
   , var'
+  , array
   , addName
   , get
   , put
@@ -36,9 +37,11 @@
 data Global = Global
   { gId      :: Int
   , gProbes  :: [(String, Type, E Word64)]
-  , gUVs     :: [UV]
+  , gInit8   :: [Const]
+  , gInit16  :: [Const]
+  , gInit32  :: [Const]
+  , gInit64  :: [Const]
   , gPeriod  :: Int
-  , gAsserts :: [(String, UE)]
   }
 
 data AtomDB = AtomDB
@@ -131,20 +134,17 @@
 -- data Relation = Higher UID | Lower UID deriving (Show, Eq)
 
 -- | Given a top level name and design, elabortes design and returns a design database.
-elaborate :: Name -> Atom () -> IO (Maybe ([Rule], [UV], [(String, UE)]))
+elaborate :: Name -> Atom () -> IO (Maybe ([Rule], ([Const], [Const], [Const], [Const])))
 elaborate name atom = do
   putStrLn "Starting atom elaboration..."
   hFlush stdout
-  (_, (g, atomDB)) <- buildAtom (Global { gId = 0, gProbes = [], gUVs = [], gPeriod = 1, gAsserts = [] }) name atom
+  (_, (g, atomDB)) <- buildAtom (Global { gId = 0, gInit8 = [], gInit16 = [], gInit32 = [], gInit64 = [], gProbes = [], gPeriod = 1 }) name atom
   let rules = reIdRules $ elaborateRules (ubool True) atomDB
   mapM_ checkEnable rules
   ok <- checkAssignConflicts atomDB
   if not ok
     then return Nothing
-    else do
-      let uvs = sort $ gUVs g
-      ruleGraph name rules uvs
-      return $ Just (rules, uvs, gAsserts g)
+    else return $ Just (rules, (gInit8 g, gInit16 g, gInit32 g, gInit64 g))
 
 checkEnable :: Rule -> IO ()
 checkEnable rule | ruleEnable rule == ubool False = putStrLn $ "WARNING: Rule will never execute: " ++ show rule
@@ -164,21 +164,32 @@
   vars' = nub vars
 
 -- | Generic local variable declaration.
-var :: Name -> Const -> Atom (V a)
-var name const = do
-  name <- addName name
-  (g, atom) <- get
-  let uv = UV (gId g) name $ Local const
-  put (g { gId = gId g  + 1, gUVs =  uv : gUVs g }, atom)
-  return $ V uv
+var :: Expr a => Name -> a -> Atom (V a)
+var name init = do
+  A a <- array name [init]
+  return $ V $ UV $ Array a $ UConst $ CWord8 0
 
 -- | Generic external variable declaration.
 var' :: Name -> Type -> Atom (V a)
-var' name t = do
+var' name t = return $ V $ UV $ External name t
+
+-- | Generic array declaration.
+array :: Expr a => Name -> [a] -> Atom (A a)
+array name [] = error $ "ERROR: arrays can not be empty: " ++ name
+array name init = do
+  name <- addName name
   (g, atom) <- get
-  let uv = UV (gId g) name $ External t
-  put (g { gId = gId g  + 1, gUVs =  uv : gUVs g }, atom)
-  return $ V uv
+  let constants = map constant init
+      (addr, g') = case width $ head constants of
+        1  -> (length $ gInit8  g, g { gInit8  = gInit8  g ++ constants })
+        8  -> (length $ gInit8  g, g { gInit8  = gInit8  g ++ constants })
+        16 -> (length $ gInit16 g, g { gInit16 = gInit16 g ++ constants })
+        32 -> (length $ gInit32 g, g { gInit32 = gInit32 g ++ constants })
+        64 -> (length $ gInit64 g, g { gInit64 = gInit64 g ++ constants })
+        _  -> error "Elaboration.array: unknown width"
+      ua = UA addr name constants
+  put (g', atom)
+  return $ A ua
 
 addName :: Name -> Atom Name
 addName name = do
@@ -189,6 +200,7 @@
       put (g, atom { atomNames = name : atomNames atom })
       return $ atomName atom ++ "." ++ name
 
+{-
 ruleGraph :: Name -> [Rule] -> [UV] -> IO ()
 ruleGraph name rules uvs = do
   putStrLn $ "Writing rule graph (" ++ name ++ ".dot)..."
@@ -214,4 +226,4 @@
   ruleUVRefs r = nub $ concatMap uvSet ues
     where
     ues = ruleEnable r : snd (unzip (ruleAssigns r)) ++ concat (snd (unzip (ruleActions r)))
-
+-}
diff --git a/Language/Atom/Example.hs b/Language/Atom/Example.hs
--- a/Language/Atom/Example.hs
+++ b/Language/Atom/Example.hs
@@ -16,6 +16,7 @@
   , "#include <stdio.h>"
   , "unsigned long int a;"
   , "unsigned long int b;"
+  , "unsigned long int x;"
   , "unsigned char running = 1;"
   ]
 
@@ -24,12 +25,12 @@
   [ "int main(int argc, char* argv[]) {"
   , "  a = atoi(argv[1]);"
   , "  b = atoi(argv[2]);"
-  , "  printf(\"Computing the GCD of %i and %i...\\n\", a, b);"
+  , "  printf(\"Computing the GCD of %lu and %lu...\\n\", a, b);"
   , "  while(running) {"
   , "    example();"
-  , "    printf(\"iteration:  a = %i  b = %i\\n\", a, b);"
+  , "    printf(\"iteration:  a = %lu  b = %lu\\n\", a, b);"
   , "  }"
-  , "  printf(\"GCD result: %i\\n\", a);"
+  , "  printf(\"GCD result: %lu\\n\", a);"
   , "  return 0;"
   , "}"
   ]
@@ -62,5 +63,4 @@
   atom "stop" $ do
     cond $ value a ==. value b
     running <== false
-
 
diff --git a/Language/Atom/Expressions.hs b/Language/Atom/Expressions.hs
--- a/Language/Atom/Expressions.hs
+++ b/Language/Atom/Expressions.hs
@@ -6,20 +6,21 @@
   , UE    (..)
   , UV    (..)
   , UVLocality (..)
+  , A     (..)
+  , UA    (..)
   , Expr  (..)
   , Expression (..)
   , Variable   (..)
   , Type  (..)
   , Const (..)
   , Width (..)
-  , constType
+  , TypeOf (..)
+  , bytes
   , ue
   , uv
-  , ueType
-  , uvType
   , ueUpstream
-  , uvSet
   , NumE
+  , IntegralE
   , FloatingE
   , EqE
   , OrdE
@@ -53,6 +54,9 @@
   , mod_
   -- * Conditional Operator
   , mux
+  -- * Array Indexing
+  , (!)
+  , (!.)
   -- * Smart constructors for untyped expressions.
   , ubool
   , unot
@@ -71,6 +75,7 @@
 --infixl 7 /., %.
 --infixl 6 +., -.
 --infixr 5 ++.
+infixl 9 !, !.
 infix  4 ==., /=., <., <=., >., >=.
 infixl 3 &&. --, ^. -- , &&&, $&, $&&
 infixl 2 ||. -- , |||, $$, $:, $|
@@ -120,20 +125,6 @@
     CFloat  c -> show c
     CDouble c -> show c
 
-constType :: Const -> Type
-constType c = case c of
-  CBool   _ -> Bool
-  CInt8   _ -> Int8
-  CInt16  _ -> Int16
-  CInt32  _ -> Int32
-  CInt64  _ -> Int64
-  CWord8  _ -> Word8
-  CWord16 _ -> Word16
-  CWord32 _ -> Word32
-  CWord64 _ -> Word64
-  CFloat  _ -> Float
-  CDouble _ -> Double
-
 data Expression
   = EBool   (E Bool)
   | EInt8   (E Int8)
@@ -164,14 +155,18 @@
 -- | Variables updated by state transition rules.
 data V a = V UV deriving Eq
 
--- | Unsigned variables.
-data UV = UV Int String UVLocality deriving Show
-instance Eq   UV where UV a _ _  == UV b _ _ = a == b
-instance Ord  UV where compare (UV a _ _) (UV b _ _) = compare a b
+-- | Untyped variables.
+data UV = UV UVLocality deriving (Show, Eq, Ord)
 
 -- | UV locality.
-data UVLocality = Local Const | External Type deriving Show
+data UVLocality = Array UA UE | External String Type deriving (Show, Eq, Ord)
 
+-- | A typed array.
+data A a = A UA deriving Eq
+
+-- | An untyped array.
+data UA = UA Int String [Const] deriving (Show, Eq, Ord)
+
 -- | A typed expression.
 data E a where
   VRef    :: V a -> E a
@@ -230,6 +225,9 @@
 class Width a where
   width :: a -> Int
 
+bytes :: Width a => a -> Int
+bytes a = div (width a) 8 + if mod (width a) 8 == 0 then 0 else 1
+
 instance Width Type where
   width t = case t of
     Bool   -> 1
@@ -244,11 +242,69 @@
     Float  -> 32
     Double -> 64
 
-instance Width Const           where width = width . constType
-instance Expr a => Width (E a) where width = width . eType
-instance Expr a => Width (V a) where width = width . eType . value
-instance Width UE              where width = width . ueType
+instance Width Const           where width = width . typeOf
+instance Expr a => Width (E a) where width = width . typeOf
+instance Expr a => Width (V a) where width = width . typeOf
+instance Width UE              where width = width . typeOf
 
+class TypeOf a where typeOf :: a -> Type
+
+instance TypeOf Const where
+  typeOf a = case a of
+    CBool   _ -> Bool
+    CInt8   _ -> Int8
+    CInt16  _ -> Int16
+    CInt32  _ -> Int32
+    CInt64  _ -> Int64
+    CWord8  _ -> Word8
+    CWord16 _ -> Word16
+    CWord32 _ -> Word32
+    CWord64 _ -> Word64
+    CFloat  _ -> Float
+    CDouble _ -> Double
+
+instance TypeOf UV where
+  typeOf a = case a of
+    UV (Array a _)  -> typeOf a
+    UV (External _ t) -> t
+
+instance TypeOf (V a) where
+  typeOf (V uv) = typeOf uv
+
+instance TypeOf UA where
+  typeOf (UA _ _ c) = typeOf $ head c
+
+instance TypeOf (A a) where
+  typeOf (A ua) = typeOf ua
+
+instance TypeOf UE where
+  typeOf t = case t of
+    UVRef uvar -> typeOf uvar
+    UCast t _  -> t
+    UConst c   -> typeOf c
+    UAdd a _   -> typeOf a
+    USub a _   -> typeOf a
+    UMul a _   -> typeOf a
+    UDiv a _   -> typeOf a
+    UMod a _   -> typeOf a
+    UNot _     -> Bool
+    UAnd _     -> Bool
+    UBWNot a   -> typeOf a
+    UBWAnd a _ -> typeOf a
+    UBWOr  a _ -> typeOf a
+    UShift a _ -> typeOf a
+    UEq  _ _   -> Bool
+    ULt  _ _   -> Bool
+    UMux _ a _ -> typeOf a
+    UF2B _     -> Word32
+    UD2B _     -> Word64
+    UB2F _     -> Float
+    UB2D _     -> Double
+
+instance Expr a => TypeOf (E a) where
+  typeOf = eType
+
+
 class Eq a => Expr a where
   eType      :: E a -> Type
   constant   :: a -> Const
@@ -545,67 +601,21 @@
 mux :: Expr a => E Bool -> E a -> E a -> E a
 mux = Mux
 
--- | A set of all variables referenced in a term.
-uvSet :: UE -> [UV]
-uvSet = nub . uvList
+-- | Array index to variable.
+(!) :: (Expr a, IntegralE b) => A a -> E b -> V a
+(A ua) ! e = V $ UV $ Array ua $ ue e
 
-uvList :: UE -> [UV]
-uvList t = case t of
-  UVRef v      -> [v]
-  UCast _ a    -> uvList a
-  UConst _     -> []
-  UAdd a b     -> uvList a ++ uvList b
-  USub a b     -> uvList a ++ uvList b
-  UMul a b     -> uvList a ++ uvList b
-  UDiv a b     -> uvList a ++ uvList b
-  UMod a b     -> uvList a ++ uvList b
-  UNot a       -> uvList a
-  UAnd a       -> concatMap uvList a
-  UBWNot a     -> uvList a
-  UBWAnd a b   -> uvList a ++ uvList b
-  UBWOr  a b   -> uvList a ++ uvList b
-  UShift a _   -> uvList a
-  UEq  a b     -> uvList a ++ uvList b
-  ULt  a b     -> uvList a ++ uvList b
-  UMux a b c   -> uvList a ++ uvList b ++ uvList c
-  UF2B a       -> uvList a
-  UD2B a       -> uvList a
-  UB2F a       -> uvList a
-  UB2D a       -> uvList a
+-- | Array index to expression.
+(!.) :: (Expr a, IntegralE b) => A a -> E b -> E a
+a !. i = value $ a ! i
 
-uvType :: UV -> Type
-uvType (UV _ _ (Local c))    = constType c
-uvType (UV _ _ (External t)) = t
 
--- | The type of an UE.
-ueType :: UE -> Type
-ueType t = case t of
-  UVRef uvar -> uvType uvar
-  UCast t _  -> t
-  UConst c   -> constType c
-  UAdd a _   -> ueType a
-  USub a _   -> ueType a
-  UMul a _   -> ueType a
-  UDiv a _   -> ueType a
-  UMod a _   -> ueType a
-  UNot _     -> Bool
-  UAnd _     -> Bool
-  UBWNot a   -> ueType a
-  UBWAnd a _ -> ueType a
-  UBWOr  a _ -> ueType a
-  UShift a _ -> ueType a
-  UEq  _ _   -> Bool
-  ULt  _ _   -> Bool
-  UMux _ a _ -> ueType a
-  UF2B _     -> Word32
-  UD2B _     -> Word64
-  UB2F _     -> Float
-  UB2D _     -> Double
 
 -- | The list of UEs adjacent upstream of a UE.
 ueUpstream :: UE -> [UE]
 ueUpstream t = case t of
-  UVRef _   -> []
+  UVRef (UV (Array _ ue))   -> [ue]
+  UVRef (UV (External _ _)) -> []
   UCast _ a   -> [a]
   UConst _    -> []
   UAdd a b    -> [a, b]
@@ -741,7 +751,7 @@
 
 umux :: UE -> UE -> UE -> UE
 umux _ t f | t == f = f
-umux b t f | ueType t == Bool = uor (uand b t) (uand (unot b) f)
+umux b t f | typeOf t == Bool = uor (uand b t) (uand (unot b) f)
 umux (UConst (CBool b)) t f = if b then t else f
 umux (UNot b) t f = umux b f t
 umux b1 (UMux b2 t _) f | b1 == b2 = umux b1 t f
diff --git a/Language/Atom/Language.hs b/Language/Atom/Language.hs
--- a/Language/Atom/Language.hs
+++ b/Language/Atom/Language.hs
@@ -13,12 +13,10 @@
   , Assign (..)
   , incr
   , decr
-  -- ** Performance Constraints
-  --, required
-  --, priority
   -- * Variable Declarations
   , var
   , var'
+  , array
   , bool
   , bool'
   , int8
@@ -43,8 +41,6 @@
   , double'
   -- * Custom Actions
   , action
-  -- * Assertions
-  , assert
   -- * Probing
   , probe
   , probes
@@ -108,7 +104,7 @@
 
 -- | Local boolean variable declaration.
 bool :: Name -> Bool -> Atom (V Bool)
-bool name init = var name $ CBool init
+bool = var
 
 -- | External boolean variable declaration.
 bool' :: Name -> Atom (V Bool)
@@ -116,7 +112,7 @@
 
 -- | Local int8 variable declaration.
 int8 :: Name -> Int8 -> Atom (V Int8)
-int8 name init = var name $ CInt8 init
+int8 = var
 
 -- | External int8 variable declaration.
 int8' :: Name -> Atom (V Int8)
@@ -124,7 +120,7 @@
 
 -- | Local int16 variable declaration.
 int16 :: Name -> Int16 -> Atom (V Int16)
-int16 name init = var name $ CInt16 init
+int16 = var
 
 -- | External int16 variable declaration.
 int16' :: Name -> Atom (V Int16)
@@ -132,7 +128,7 @@
 
 -- | Local int32 variable declaration.
 int32 :: Name -> Int32 -> Atom (V Int32)
-int32 name init = var name $ CInt32 init
+int32 = var
 
 -- | External int32 variable declaration.
 int32' :: Name -> Atom (V Int32)
@@ -140,7 +136,7 @@
 
 -- | Local int64 variable declaration.
 int64 :: Name -> Int64 -> Atom (V Int64)
-int64 name init = var name $ CInt64 init
+int64 = var
 
 -- | External int64 variable declaration.
 int64' :: Name -> Atom (V Int64)
@@ -148,7 +144,7 @@
 
 -- | Local word8 variable declaration.
 word8 :: Name -> Word8 -> Atom (V Word8)
-word8 name init = var name $ CWord8 init
+word8 = var
 
 -- | External word8 variable declaration.
 word8' :: Name -> Atom (V Word8)
@@ -156,7 +152,7 @@
 
 -- | Local word16 variable declaration.
 word16 :: Name -> Word16 -> Atom (V Word16)
-word16 name init = var name $ CWord16 init
+word16 = var
 
 -- | External word16 variable declaration.
 word16' :: Name -> Atom (V Word16)
@@ -164,7 +160,7 @@
 
 -- | Local word32 variable declaration.
 word32 :: Name -> Word32 -> Atom (V Word32)
-word32 name init = var name $ CWord32 init
+word32 = var
 
 -- | External word32 variable declaration.
 word32' :: Name -> Atom (V Word32)
@@ -172,7 +168,7 @@
 
 -- | Local word64 variable declaration.
 word64 :: Name -> Word64 -> Atom (V Word64)
-word64 name init = var name $ CWord64 init
+word64 = var
 
 -- | External word64 variable declaration.
 word64' :: Name -> Atom (V Word64)
@@ -180,7 +176,7 @@
 
 -- | Local float variable declaration.
 float :: Name -> Float -> Atom (V Float)
-float name init = var name $ CFloat init
+float = var
 
 -- | External float variable declaration.
 float' :: Name -> Atom (V Float)
@@ -188,7 +184,7 @@
 
 -- | Local double variable declaration.
 double :: Name -> Double -> Atom (V Double)
-double name init = var name $ CDouble init
+double = var
 
 -- | External double variable declaration.
 double' :: Name -> Atom (V Double)
@@ -200,18 +196,13 @@
   (g, a) <- get
   put (g, a { atomActions = atomActions a ++ [(f, ues)] })
 
--- | Asserts expression must always be true.
-assert :: Name -> E Bool -> Atom ()
-assert name a = do
-  name <- addName name
-  (g, atom) <- get
-  put (g { gAsserts = gAsserts g ++ [(name, ue a)] }, atom)
-
 -- | Declares a probe.
 probe :: Expr a => Name -> E a -> Atom ()
 probe name a = do
   (g, atom) <- get
-  put (g { gProbes = (name, eType a, rawBits a) : gProbes g }, atom)
+  if any (\ (n, _, _) -> name == n) $ gProbes g
+    then error $ "ERROR: Duplicated probe name: " ++ name
+    else put (g { gProbes = (name, eType a, rawBits a) : gProbes g }, atom)
 
 
 -- | Fetches all declared probes to current design point.
@@ -231,7 +222,7 @@
 
 
 class Expr a => Assign a where
-  -- | Assigns a 'E' to a 'V'.
+  -- | Assign an 'E' to a 'V'.
   (<==) :: V a -> E a -> Atom ()
   v <== e = do
     (g, atom) <- get
@@ -259,11 +250,11 @@
 
 -- | Reference to the 64-bit free running clock.
 clock :: E Word64
-clock = value (V (UV (-1) "__clock" (External Word64)))
+clock = value $ V $ UV $ External "__clock" Word64
 
 -- | Rule coverage information.  (current coverage index, coverage data)
 nextCoverage :: Atom (E Word32, E Word32)
 nextCoverage = do
   action (\_ -> "__coverage_index = (__coverage_index + 1) % __coverage_len") []
-  return (value (V (UV (-2) "__coverage_index" (External Word32))), value (V (UV (-3) "__coverage[__coverage_index]" (External Word32))))
+  return (value $ V $ UV $ External "__coverage_index" Word32, value $ V $ UV $ External "__coverage[__coverage_index]" Word32)
 
diff --git a/Language/Atom/Scheduling.hs b/Language/Atom/Scheduling.hs
--- a/Language/Atom/Scheduling.hs
+++ b/Language/Atom/Scheduling.hs
@@ -39,7 +39,12 @@
 reportSchedule :: [[[Rule]]] -> String
 reportSchedule s = "Rule Scheduling Report\n\n  Period  Cycle  Exprs  Rule\n  ------  -----  -----  ----\n" ++ (concatMap reportPeriod) (zip [1..] s) ++
                    "                 -----\n" ++
-                   printf "                 %5i\n" (sum $ map ruleComplexity (concat (concat s)))
+                   printf "                 %5i\n" (sum $ map ruleComplexity (concat (concat s))) ++ "\n" ++
+                   "Heirarchical Expression Count\n\n" ++
+                   "  Total   Local     Rule\n" ++
+                   "  ------  ------    ----\n" ++
+                   reportUsage "" (usage $ concat $ concat s) ++
+                   "\n"
 
 reportPeriod (period, p) = concatMap (reportCycle period) (zip [0..] p)
 
@@ -49,4 +54,33 @@
 reportRule period cycle rule = printf "  %6i  %5i  %5i  %s\n" period cycle (ruleComplexity rule) (show rule)
 
 
+data Usage = Usage String Int [Usage] deriving Eq
+
+instance Ord Usage where compare (Usage a _ _) (Usage b _ _) = compare a b
+
+reportUsage :: String -> Usage -> String
+reportUsage i node@(Usage name n subs) = printf "  %6i  %6i    %s\n" (totalComplexity node) n (i ++ name) ++ concatMap (reportUsage ("  " ++ i)) subs
+
+totalComplexity :: Usage -> Int
+totalComplexity (Usage _ n subs) = n + sum (map totalComplexity subs)
+
+usage :: [Rule] -> Usage
+usage rules = head $ foldl insertUsage [] $ map usage' rules
+
+usage' :: Rule -> Usage
+usage' rule = f $ split $ ruleName rule
+  where
+  f :: [String] -> Usage
+  f [] = undefined
+  f [name] = Usage name (ruleComplexity rule) []
+  f (name:names) = Usage name 0 [f names]
+
+split :: String -> [String]
+split "" = []
+split s = a : if null b then [] else split (tail b) where (a,b) = span (/= '.') s
+
+insertUsage :: [Usage] -> Usage -> [Usage]
+insertUsage [] u = [u]
+insertUsage (a@(Usage n1 i1 s1) : rest) b@(Usage n2 i2 s2) | n1 == n2  = Usage n1 (max i1 i2) (sort $ foldl insertUsage s1 s2) : rest
+                                                           | otherwise = a : insertUsage rest b
 
diff --git a/Language/Atom/Verify.hs b/Language/Atom/Verify.hs
deleted file mode 100644
--- a/Language/Atom/Verify.hs
+++ /dev/null
@@ -1,215 +0,0 @@
-module Language.Atom.Verify (verify) where
-
-import Data.Char
-import Data.Int
-import Data.List
-import Data.Ratio
-import Data.Word
-import System.Process
-
-import Language.Atom.Elaboration
-import Language.Atom.Expressions
-
-verify :: Int -> [[[Rule]]] -> [UV] -> (String, UE) -> IO Bool
-verify depth rules uvs (name, assert) = do
-  putStrLn $ "Checking assertion " ++ name ++ "..."
-  verify
-      
-  where
-  verify | assert == ubool True  = return True
-         | assert == ubool False = putStrLn ("Assertion failed trivially.") >> return False
-         | otherwise = do
-             --putStrLn yices
-             --putStrLn "***********************************************"
-             out <- readProcess "yices" ["-e"] yices
-             case parseYices out of
-               S "unsat" : _ -> return True
-               S "sat"   : vars' -> do
-                 let vars = map (parseVar uvs) vars'
-                 putStrLn ("Assertion failed.  See counter example: " ++ name ++ ".vcd")
-                 writeFile (name ++ ".vcd") $ vcd uvs vars
-                 return False
-               _         -> error "Unexpected results from yices."
-      
-  assertUE :: Int -> String
-  assertUE step = "(assert (not " ++ f ++ "))\n"
-    where
-    f = case assert of
-      UVRef uv -> uvName step uv
-      _        -> error "expressions not supported assertions yet"
-
-  asserts = concatMap assertUE [0..depth]
-  yices = initialize uvs ++ concatMap (transition rules uvs) [1..depth] ++ asserts ++ "(check)"
-
-yicesType :: Type -> String
-yicesType t = case t of
-  Bool   -> "bool"
-  Int8   -> "(bitvector  8)"
-  Int16  -> "(bitvector 16)"
-  Int32  -> "(bitvector 32)"
-  Int64  -> "(bitvector 64)"
-  Word8  -> "(bitvector  8)"
-  Word16 -> "(bitvector 16)"
-  Word32 -> "(bitvector 32)"
-  Word64 -> "(bitvector 64)"
-  Float  -> "real"
-  Double -> "real"
-
-vars :: [UV] -> Int -> String
-vars uvs step = concatMap (var step) uvs
-  where
-  var :: Int -> UV -> String
-  var step uv = "(define " ++ uvName step uv ++ "::" ++ yicesType (uvType uv) ++ ")\n"
-
-uvName :: Int -> UV -> String
-uvName step (UV i _ _) = "v" ++ show i ++ "_" ++ show step
-
-initialize :: [UV] -> String
-initialize uvs = vars uvs 0 ++ concatMap initialize uvs
-  where
-  initialize :: UV -> String
-  initialize uv@(UV _ _ (Local c)) = "(assert (= " ++ uvName 0 uv ++ " " ++ const c ++ "))\n"
-  initialize (UV _ _ (External _)) = ""
-  const :: Const -> String
-  const c = case c of
-    CBool   c -> if c then "true" else "false" 
-    CInt8   c -> "0b" ++ bits  8 (fromIntegral c)
-    CInt16  c -> "0b" ++ bits 16 (fromIntegral c)
-    CInt32  c -> "0b" ++ bits 32 (fromIntegral c)
-    CInt64  c -> "0b" ++ bits 64 (fromIntegral c)
-    CWord8  c -> "0b" ++ bits  8 (fromIntegral c)
-    CWord16 c -> "0b" ++ bits 16 (fromIntegral c)
-    CWord32 c -> "0b" ++ bits 32 (fromIntegral c)
-    CWord64 c -> "0b" ++ bits 64 (fromIntegral c)
-    CFloat  c -> "(/ " ++ show (numerator $ toRational c) ++ " " ++ show (denominator $ toRational c) ++ ")"
-    CDouble c -> "(/ " ++ show (numerator $ toRational c) ++ " " ++ show (denominator $ toRational c) ++ ")"
-
-  bits :: Int -> Word64 -> String
-  bits 0 _ = ""
-  bits n a = bits (n - 1) (div a 2) ++ show (mod a 2)
-
--- Time 0 to 1 is step 1.
-transition :: [[[Rule]]] -> [UV] -> Int -> String
-transition _ {-schedule-} uvs step = vars uvs step ++ transition
-  where
-  transition = "; transition " ++ show (step - 1) ++ " to " ++ show step ++ "\n"  --XXX
-
-getUV :: [UV] -> Int -> UV
-getUV [] _ = error "Verify.getUV"
-getUV (uv@(UV i _ _):_) j | i == j = uv
-getUV (_:a) i = getUV a i
-
-
-parseVar :: [UV] -> Group -> (Int, UV, String)
-parseVar uvs (G [S "=", S name, value]) = (t, getUV uvs i, parseValue value)
-  where
-  (i', t') = break (== '_') $ tail name
-  i = read i'
-  t = read $ tail t'
-parseVar _ g = error $ "Verify.parseVar: " ++ show g
-
-parseValue :: Group -> String
-parseValue (S ('0':'b':a)) = "b" ++ a ++ " "
-parseValue (S "true")      = "1"
-parseValue (S "false")     = "0"
-parseValue (S v)           = "r" ++ v ++ " "
-parseValue (G [S "/", S n, S d]) = "r" ++ show (fromRational (read n % read d)) ++ " "
-parseValue a               = error $ "Verify.parseValue: " ++ show a
-
-
-data Group = G [Group] | S String deriving Show
-
-parseYices :: String -> [Group]
-parseYices = groups . tokens
-
-groups :: [String] -> [Group]
-groups [] = []
-groups ("(":a) = G (groups x) : groups y where (x, y) = split 0 [] a
-groups (a:b) = S a : groups b
-
-split :: Int -> [String] -> [String] -> ([String], [String])
-split 0 a (")":b) = (reverse a, b)
-split n a ("(":b) = split (n + 1) ("(" : a) b
-split n a (")":b) = split (n - 1) (")" : a) b
-split n a (b:c)   = split n (b:a) c
-split _ _ []      = error "Verify.split"
-
-tokens :: String -> [String]
-tokens [] = []
-tokens (a:b) | isSpace a = tokens b
-tokens ('(':b) = "(" : tokens b
-tokens (')':b) = ")" : tokens b
-tokens a = tokens' "" a
-
-tokens' :: String -> String -> [String]
-tokens' a [] = [reverse a]
-tokens' a c@(b:_) | isSpace b || elem b "()" = reverse a : tokens c
-tokens' a (b:c) = tokens' (b:a) c
-
-data Heirarchy = Variable UV | Module String [Heirarchy]
-
-vcd :: [UV] -> [(Int, UV, String)] -> String
-vcd uvs signals' = header ++ samples ++ end
-  where
-  signals = sortBy (\ (a,_,_) (b,_,_) -> compare a b) signals' 
-
-  header = "$timescale\n  1 ms\n$end\n" ++ concatMap decl (heirarchy 0 uvs) ++ "$enddefinitions $end\n"
-  (lastTime, _, _) = last signals
-  end = "#" ++ show (lastTime + 1) ++ "\n"
-
-  decl :: Heirarchy -> String
-  decl (Module name subs) = "$scope module " ++ name ++ " $end\n" ++ concatMap decl subs ++ "$upscope $end\n"
-  decl (Variable uv)      = declVar uv
-
-  declVar :: UV -> String
-  declVar uv@(UV i n _) = case uvType uv of
-    Bool   -> "$var wire 1 "     ++ code ++ " " ++ name ++ " $end\n"
-    Int8   -> "$var integer 8 "  ++ code ++ " " ++ name ++ " $end\n"
-    Int16  -> "$var integer 16 " ++ code ++ " " ++ name ++ " $end\n"
-    Int32  -> "$var integer 32 " ++ code ++ " " ++ name ++ " $end\n"
-    Int64  -> "$var integer 64 " ++ code ++ " " ++ name ++ " $end\n"
-    Word8  -> "$var wire 8 "     ++ code ++ " " ++ name ++ " $end\n"
-    Word16 -> "$var wire 16 "    ++ code ++ " " ++ name ++ " $end\n"
-    Word32 -> "$var wire 32 "    ++ code ++ " " ++ name ++ " $end\n"
-    Word64 -> "$var wire 64 "    ++ code ++ " " ++ name ++ " $end\n"
-    Float  -> "$var real 32 "    ++ code ++ " " ++ name ++ " $end\n"
-    Double -> "$var real 64 "    ++ code ++ " " ++ name ++ " $end\n"
-    where
-    code = vcdCode i
-    name = reverse $ takeWhile (/= '.') $ reverse n
-
-  samples = concatMap sample signals
-
-  sample (t, (UV i _ _), v) = "#" ++ show t ++ "\n" ++ v ++ vcdCode i ++ "\n"
-
-heirarchy :: Int -> [UV] -> [Heirarchy]
-heirarchy _ [] = []
-heirarchy depth uvs = heirarchy' depth notvars ++ map Variable vars
-  where
-  isVar :: UV -> Bool
-  isVar uv = length (path depth uv) == 1
-  (vars, notvars) = partition isVar uvs
-
-heirarchy' :: Int -> [UV] -> [Heirarchy]
-heirarchy' _ [] = []
-heirarchy' depth uvs@(a:_) = Module n (heirarchy (depth + 1) yes) : heirarchy' depth no
-  where
-  n = head $ path depth a
-  isMod uv = n == head (path depth uv)
-  (yes, no) = partition isMod uvs
-
-path :: Int -> UV -> [String]
-path depth (UV _ n _) = drop depth $ words $ map (\ c -> if c == '.' then ' ' else c) n
- 
-vcdCode :: Int -> String
-vcdCode i | i < 94 =              [chr (33 + mod i 94)] 
-vcdCode i = vcdCode (div i 94) ++ [chr (33 + mod i 94)] 
-
-{-
-bitString :: Int -> String
-bitString n = if null bits then "0" else bits
-  where
-  bit :: Int -> Char
-  bit i = if testBit n i then '1' else '0'
-  bits = dropWhile (== '0') $ map bit $ reverse [0..31]
--}
diff --git a/RELEASE-NOTES b/RELEASE-NOTES
--- a/RELEASE-NOTES
+++ b/RELEASE-NOTES
@@ -1,3 +1,12 @@
+atom 0.0.4    05/19/2009
+
+- Made local variables static in generated C.
+- Added checking for duplicate probe names.
+- Added hierarchical expression count report.
+- Removed dot graph for rule-variable relationships.
+- Added support for arrays.  See array, (!), and (!.).
+  WARNING: No checks for index out of bounds or overlapping assignments.
+
 atom 0.0.3    05/05/2009
 
 - Set build-depends: process >= 1.0.1.1 for readProcess
diff --git a/atom.cabal b/atom.cabal
--- a/atom.cabal
+++ b/atom.cabal
@@ -1,5 +1,5 @@
 Name:           atom
-Version:        0.0.3
+Version:        0.0.4
 Synopsis:       A DSL for embedded hard realtime applications.
 Description:    Atom is a Haskell DSL for designing hard realtime embedded programs.
                 Based on conditional term rewriting, atom will compile
@@ -26,8 +26,7 @@
     Language.Atom.Example,
     Language.Atom.Expressions,
     Language.Atom.Language,
-    Language.Atom.Scheduling,
-    Language.Atom.Verify
+    Language.Atom.Scheduling
   extensions:      GADTs
   ghc-options:     -W
   Other-Modules: