diff --git a/Language/ImProve.hs b/Language/ImProve.hs
--- a/Language/ImProve.hs
+++ b/Language/ImProve.hs
@@ -57,13 +57,13 @@
 /Assertion Statements/
 
 @
-assert(condition);        'assert' condition
+assert(condition);        'theorem' name k lemmas condition
 @
 
 /Statement Labels/
 
 @
-label: {                  \"label\" '|' do
+label: {                  \"label\" '-|' do
     a();                      a
     b();                      b
 }
@@ -78,7 +78,7 @@
 false                     'false'
 0                         0
 100                       100
-1.0                       1     -- float
+1.0                       1
 3.14                      3.14
 
 /Variable Reference/
@@ -225,6 +225,7 @@
 import qualified Language.ImProve.Verify as V
 import qualified Language.ImProve.Code   as C
 
+--infixl 9 !, !.
 infixl 7 *., /., `div_`, `mod_`
 infix  4 ==., /=., <., <=., >., >=.
 infixl 3 &&.
@@ -342,7 +343,7 @@
 mod_ _ 0 = error "divide by zero (mod_)"
 mod_ a b = Mod a b
 
--- | Linear interpolation and extrapolation between two points.
+-- | Linear interpolation and extrapolation of two points.
 linear :: (Float, Float) -> (Float, Float) -> E Float -> E Float
 linear (x1, y1) (x2, y2) a = a *. slope + constant inter
   where
@@ -359,6 +360,14 @@
 mux :: AllE a => E Bool -> E a -> E a -> E a
 mux = Mux
 
+-- | Array index to a variable.
+--(!) :: AllE a => A a -> E Int -> V a
+--(!) a i = VArray a i
+
+-- | Array index to an expression.
+--(!.) :: AllE a => A a -> E Int -> E a
+--(!.) a i = ref $ a ! i
+
 -- | Labels a statement and creates a variable scope.
 --   Labels are used in counter examples to trace the program execution.
 --   And assertion names, and hence counter example trace file names, are produce from labels.
@@ -464,8 +473,8 @@
 -- | Declare an assumption condition is true.
 --   Assumptions expressions must contain variables directly or indirectly related
 --   to the assertion under verification, otherwise they will be ignored.
-assume :: E Bool -> Stmt ()
-assume a = statement $ Assume a
+assume :: Name -> E Bool -> Stmt ()
+assume name a = statement $ Label name $ Assume a
 
 -- | Theorem to be proven or used as lemmas to assist proofs of other theorems.
 data Theorem = Theorem' Int
diff --git a/Language/ImProve/Code.hs b/Language/ImProve/Code.hs
--- a/Language/ImProve/Code.hs
+++ b/Language/ImProve/Code.hs
@@ -1,13 +1,17 @@
 module Language.ImProve.Code (code) where
 
+import Control.Monad.State
 import Data.List
+import Data.Maybe
 import Text.Printf
 
 import Language.ImProve.Core
 import Language.ImProve.Tree hiding (Branch)
 import qualified Language.ImProve.Tree as T
 
--- | Generate C code.
+infixr 0 :-, :=
+
+-- | Generate C and Simulink code.
 code :: Name -> Statement -> IO ()
 code name stmt = do
   writeFile (name ++ ".c") $
@@ -21,8 +25,9 @@
        "/* Generated by ImProve. */\n\n"
     ++ codeVariables False scope ++ "\n"
     ++ "void " ++ name ++ "(void);\n\n"
+  codeMdl name stmt
   where
-  scope = case tree (\ (_, path, _) -> path) $ map varInfo $ stmtVars stmt of
+  scope = case tree (\ (_, path, _) -> path) $ stmtVars stmt of
     [] -> error "program contains no useful statements"
     a  -> T.Branch (name ++ "_variables") a
 
@@ -34,8 +39,8 @@
   Branch a b Null -> "if (" ++ codeExpr a ++ ") {\n" ++ indent (codeStmt name path b) ++ "}\n"
   Branch a b c    -> "if (" ++ codeExpr a ++ ") {\n" ++ indent (codeStmt name path b) ++ "}\nelse {\n" ++ indent (codeStmt name path c) ++ "}\n"
   Sequence a b -> codeStmt name path a ++ codeStmt name path b
-  Theorem _ _ _ a -> "assert((" ++ show (intercalate "." path) ++ ", " ++ codeExpr a ++ "));\n"
-  Assume a -> "assert((" ++ show (intercalate "." path) ++ ", " ++ codeExpr a ++ "));\n"
+  Theorem _ _ _ a -> "assert((" ++ show (pathName path) ++ ", " ++ codeExpr a ++ "));\n"
+  Assume a -> "assert((" ++ show (pathName path) ++ ", " ++ codeExpr a ++ "));\n"
   Label name' a -> "/*" ++ name' ++ "*/\n" ++ indent (codeStmt name (path ++ [name']) a)
   Null -> ""
   where
@@ -93,4 +98,326 @@
   Bool  _ -> "int"
   Int   _ -> "int"
   Float _ -> "float"
+
+
+type Net = StateT Netlist IO
+
+data Block
+  = Inport  Const
+  | Outport Const
+  | UnitDelay Const
+  | Cast String
+  | Assertion
+  | Const' Const
+  | Add'
+  | Sub'
+  | Mul'
+  | Div'
+  | Mod'
+  | Not'
+  | And'
+  | Or'
+  | Eq'
+  | Lt'
+  | Gt'
+  | Le'
+  | Ge'
+  | Mux'
+
+data Netlist = Netlist
+  { nextId :: Int
+  , path   :: Path
+  , vars   :: [Path]
+  , env    :: [Name]
+  , blocks :: [(Name, Block)]
+  , nets   :: [(Name, (Name, Int))]
+  }
+
+-- Simulink generation.
+codeMdl :: Name -> Statement -> IO ()
+codeMdl name stmt = do
+  net <- execStateT all (Netlist 0 [] paths env [] [])
+  writeFile (name ++ ".mdl") $ show $ mdl name $ (mdlBlocks $ blocks net) ++ (mdlLines $ nets net)
+  where
+  vars = stmtVars stmt
+  paths = [ path | (_, path, _) <- vars ]
+  env = [ error $ "variable " ++ pathName a ++ " does not have a source" | a <- vars ]
+
+  all :: Net ()
+  all = do
+    inputs <- mapM input vars
+    elaborate stmt
+    mapM_ output $ zip vars inputs
+
+  input :: VarInfo -> Net Name
+  input (input, path, const) = if input
+    then do
+      a <- block' (pathName path) (Inport const)
+      updateEnv path a
+      return a
+    else do
+      a <- block $ UnitDelay const
+      b <- block $ Cast $ constType const
+      net a (b, 0)
+      updateEnv path b
+      return a
+  
+  output :: (VarInfo, Name) -> Net ()
+  output ((True, _, _), _) = return ()
+  output ((False, path, const), delay) = do
+    a <- block' (pathName path) $ Outport const
+    src <- getNet path
+    net src (a, 0)
+    net src (delay, 0)
+
+newName :: Net Name
+newName = do
+  net <- get
+  put net { nextId = nextId net + 1 }
+  return $ "b" ++ show (nextId net)
+
+-- New unnamed block.
+block :: Block -> Net Name
+block a = do
+  name <- newName
+  modify $ \ net -> net { blocks = (name, a) : blocks net }
+  return name
+
+-- New named block.
+block' :: Name -> Block -> Net Name
+block' name a = do
+  modify $ \ net -> net { blocks = (name, a) : blocks net }
+  return name
+
+-- New net.
+net :: Name -> (Name, Int) -> Net ()
+net src (dest, port) = modify $ \ net -> net { nets = (src, (dest, port)) : nets net }
+
+updateEnv :: Path -> Name -> Net ()
+updateEnv path name = do
+  net <- get
+  let i = fromJust $ elemIndex path $ vars net
+      pre = take i $ env net
+      post = drop (i + 1) $ env net
+  put net { env = pre ++ [name] ++ post }
+
+getNet :: Path -> Net Name
+getNet path = do
+  net <- get
+  return $ env net !! (fromJust $ elemIndex path $ vars net)
+
+getPathName :: Net Name
+getPathName = do
+  net <- get
+  return $ pathName $ path net
+
+-- Elaborate netlist.
+elaborate :: Statement -> Net ()
+elaborate a = case a of 
+
+  Assign (V _ path _) b -> do
+    b <- evalExpr b
+    updateEnv path b
+
+  Branch a b c -> do
+    cond <- evalExpr a
+    net0 <- get
+
+    elaborate b
+    net1 <- get
+    modify $ \ net -> net { env = env net0 }
+
+    elaborate c
+    net2 <- get
+    modify $ \ net -> net { env = env net0 }
+
+    names <- mergeEnvs cond (env net1) (env net2)
+    modify $ \ net -> net { env = names }
+
+    where
+
+    mergeEnvs :: Name -> [Name] -> [Name] -> Net [Name]
+    mergeEnvs _ [] [] = return []
+    mergeEnvs cond (a : as) (b : bs) = do
+      names <- mergeEnvs cond as bs
+      name <- if a == b then return a else do
+        switch <- block Mux'
+        net a    (switch, 0)
+        net cond (switch, 1)
+        net b    (switch, 2)
+        return switch
+      return $ name : names
+    mergeEnvs _ _ _ = error "unbalanced environments"
+
+  Sequence a b    -> elaborate a >> elaborate b
+
+  Theorem _ _ _ a -> do
+    a <- evalExpr a
+    name <- getPathName
+    assert <- block' name Assertion
+    net a (assert, 0)
+
+  Assume a -> do
+    a <- evalExpr a
+    name <- getPathName
+    assert <- block' name Assertion
+    net a (assert, 0)
+
+  Label name a -> do
+    modify $ \ net -> net { path = path net ++ [name] }
+    elaborate a
+    modify $ \ net -> net { path = init $ path net }
+
+  Null            -> return ()
+
+evalExpr :: E a -> Net Name
+evalExpr a = case a of
+  Ref (V _ path _) -> getNet path
+  Const a   -> block $ Const' $ const' a
+  Add a b   -> f2 Add' a b
+  Sub a b   -> f2 Sub' a b
+  Mul a b   -> do
+    b <- block $ Const' $ const' b
+    f2' Mul' a b
+  Div a b   -> do
+    b <- block $ Const' $ const' b
+    f2' Div' a b
+  Mod a b   -> do
+    b <- block $ Const' $ const' b
+    f2' Mod' a b
+  Not a     -> f1 Not' a
+  And a b   -> f2 And' a b
+  Or  a b   -> f2 Or'  a b
+  Eq  a b   -> f2 Eq'  a b
+  Lt  a b   -> f2 Lt'  a b
+  Gt  a b   -> f2 Gt'  a b
+  Le  a b   -> f2 Le'  a b
+  Ge  a b   -> f2 Ge'  a b
+  Mux a b c -> f3 Mux' b a c
+  where
+  f1 :: Block -> E a -> Net Name
+  f1 b a1 = do
+    a1 <- evalExpr a1
+    b  <- block b
+    net a1 (b, 0)
+    return b
+
+  f2 :: Block -> E a -> E b -> Net Name
+  f2 b a1 a2 = do
+    a1 <- evalExpr a1
+    a2 <- evalExpr a2
+    b  <- block b
+    net a1 (b, 0)
+    net a2 (b, 1)
+    return b
+
+  f2' :: Block -> E a -> Name -> Net Name
+  f2' b a1 a2 = do
+    a1 <- evalExpr a1
+    b  <- block b
+    net a1 (b, 0)
+    net a2 (b, 1)
+    return b
+
+  f3 :: Block -> E a -> E b -> E c -> Net Name
+  f3 b a1 a2 a3 = do
+    a1 <- evalExpr a1
+    a2 <- evalExpr a2
+    a3 <- evalExpr a3
+    b  <- block b
+    net a1 (b, 0)
+    net a2 (b, 1)
+    net a3 (b, 2)
+    return b
+
+data Mdl
+  = String :- String
+  | String := [Mdl]
+
+instance Show Mdl where
+  show a = case a of
+    name :- value -> name ++ "\t" ++ show value ++ "\n"
+    name := items -> name ++ " {\n" ++ indent (concatMap show items) ++ "}\n"
+    where
+    indent = unlines . map ('\t' :) . lines
+
+mdl :: Name -> [Mdl] -> Mdl
+mdl name blocks = "Library" :=
+  [ "Name" :- name
+  , "System" :=
+    [ "Name" :- name
+    , "Block" :=
+      [ "BlockType" :- "SubSystem"
+      , "Name" :- name
+      , "TreatAsAtomicUnit" :- "on"
+      , "System" := ("Name" :- name) : blocks
+      ]
+    ]
+  ]
+
+mdlLines :: [(Name, (Name, Int))] -> [Mdl]
+mdlLines nets = map branch branches
+  where
+  branches :: [(Name, [(Name, Int)])]
+  branches = [ (src, [ dest | (src', dest) <- nets, src == src' ]) | src <- nub $ fst $ unzip nets ]
+  branch :: (Name, [(Name, Int)]) -> Mdl
+  branch (src, dests) = "Line" :=
+    [ "SrcBlock" :- src
+    , "SrcPort"  :- "1"
+    ] ++ (if length dests == 1 then head dests' else map ("Branch" :=) dests')
+    where
+    dests' = [ ["DstBlock" :- dest, "DstPort" :- show $ port + 1] | (dest, port) <- dests ]
+
+mdlBlocks :: [(Name, Block)] -> [Mdl]
+mdlBlocks blocks = map (port "Inport") inputs ++ map blk others ++ map (port "Outport") outputs
+  where
+  inputs  = zip [1 ..] $ sortBy (\ (a, _) (b, _) -> compare a b) [ (name, constType init) | (name, Inport  init) <- blocks ]
+  outputs = zip [1 ..] $ sortBy (\ (a, _) (b, _) -> compare a b) [ (name, constType init) | (name, Outport init) <- blocks ]
+  others  = [ (name, block) | (name, block) <- blocks, not $ isPort block ]
+  port :: String -> (Int, (Name, String)) -> Mdl
+  port direction (port, (name, typ)) = mdlBlock direction name
+    [ "Port" :- show port
+    , "DataType" :- typ
+    ]
+  isPort :: Block -> Bool
+  isPort (Inport  _) = True
+  isPort (Outport _) = True
+  isPort _           = False
+
+mdlBlock :: String -> Name -> [Mdl] -> Mdl
+mdlBlock blockType name fields = "Block" :=
+  [ "BlockType" :- blockType
+  , "Name"      :- name
+  ] ++ fields
+
+constType :: Const -> String
+constType a = case a of
+  Bool  _ -> "boolean"
+  Int   _ -> "int32"
+  Float _ -> "single"
+
+blk :: (Name, Block) -> Mdl
+blk (name, a) = case a of
+  Inport  _ -> undefined
+  Outport _ -> undefined
+  UnitDelay init -> f "UnitDelay"          ["X0" :- showConst init, "SampleTime" :- "-1"]
+  Cast t         -> f "DataTypeConversion" ["OutDataTypeMode" :- t]
+  Assertion      -> f "Assertion"          ["StopWhenAssertionFail" :- "off", "SampleTime" :- "-1", "Enabled" :- "on"]
+  Const' c       -> f "Constant"           ["Value" :- showConst c, "OutDataTypeMode" :- constType c]
+  Add'           -> f "Sum"                ["Inputs" :- "++"]
+  Sub'           -> f "Sum"                ["Inputs" :- "+-"]
+  Mul'           -> f "Product"            ["Inputs" :- "**"]
+  Div'           -> f "Product"            ["Inputs" :- "*/"]
+  Mod'           -> f "Math"               ["Operator" :- "mod"]
+  Not'           -> f "Logic"              ["Operator" :- "NOT", "Inputs" :- "1"]
+  And'           -> f "Logic"              ["Operator" :- "AND", "Inputs" :- "2"]
+  Or'            -> f "Logic"              ["Operator" :- "OR",  "Inputs" :- "2"]
+  Eq'            -> f "RelationalOperator" ["Operator" :- "==", "LogicOutDataTypeMode" :- "boolean"]
+  Lt'            -> f "RelationalOperator" ["Operator" :- "<" , "LogicOutDataTypeMode" :- "boolean"]
+  Gt'            -> f "RelationalOperator" ["Operator" :- ">" , "LogicOutDataTypeMode" :- "boolean"]
+  Le'            -> f "RelationalOperator" ["Operator" :- "<=", "LogicOutDataTypeMode" :- "boolean"]
+  Ge'            -> f "RelationalOperator" ["Operator" :- ">=", "LogicOutDataTypeMode" :- "boolean"]
+  Mux'           -> f "Switch"             ["Criteria" :- "u2 ~= 0"]
+  where
+  f typ args = mdlBlock typ name args
 
diff --git a/Language/ImProve/Core.hs b/Language/ImProve/Core.hs
--- a/Language/ImProve/Core.hs
+++ b/Language/ImProve/Core.hs
@@ -1,7 +1,7 @@
 module Language.ImProve.Core
   ( E (..)
   , V (..)
-  , UV (..)
+  , A (..)
   , Name
   , Path
   , UID
@@ -13,7 +13,7 @@
   , VarInfo
   , varInfo
   , stmtVars
-  , exprVars
+  , arrayLength
   , theorems
   ) where
 
@@ -27,39 +27,41 @@
 type UID = Int
 
 -- | A mutable variable.
-data V a = V Bool [Name] a deriving (Eq, Ord)
+data V a
+  = V Bool Path a
+  deriving Eq
 
--- | An untyped variable.
-data UV
-  = UVBool  (V Bool)
-  | UVInt   (V Int)
-  | UVFloat (V Float)
-  deriving (Eq, Ord)
+-- | A mutable array.
+data A a = A Bool Path [a] deriving (Eq, Ord)
 
-class    PathName a         where pathName :: a -> String
-instance PathName Path      where pathName = intercalate "."
-instance PathName (V a)     where pathName (V _ path _) = pathName path
-instance PathName VarInfo   where pathName (_, path, _) = pathName path
+-- | Length of array.
+arrayLength :: A a -> Int
+arrayLength (A _ _ a) = length a
 
+class    PathName a       where pathName :: a -> String
+instance PathName Path    where pathName = intercalate "."
+instance PathName (V a)   where
+  pathName a = case a of
+    V _ path _ -> pathName path
+    -- VArray a _ -> pathName a
+instance PathName (A a)   where pathName (A _ a _) = pathName a
+instance PathName VarInfo where pathName (_, path, _) = pathName path
+
 class Eq a => AllE a where
   zero   :: (Name -> a -> m (V a)) -> a
   const' :: a -> Const
-  untype :: V a -> UV
 
 instance AllE Bool where
   zero = const False
   const' = Bool
-  untype = UVBool
 
 instance AllE Int where
   zero = const 0
   const' = Int
-  untype = UVInt
   
 instance AllE Float where
   zero = const 0
   const' = Float
-  untype = UVFloat
 
 class    AllE a => NumE a
 instance NumE Int
@@ -111,25 +113,21 @@
   Null     :: Statement
 
 data Const
-  = Bool  Bool
-  | Int   Int
-  | Float Float
+  = Bool   Bool
+  | Int    Int
+  | Float  Float
   deriving (Show, Eq, Ord)
 
 type VarInfo = (Bool, Path, Const)
 
-class VarInfo' a where varInfo :: a -> VarInfo
-instance AllE a => VarInfo' (V a) where varInfo (V input path init) = (input, path, const' init)
-instance VarInfo' UV where
-  varInfo a = case a of
-    UVBool a  -> varInfo a
-    UVInt  a  -> varInfo a
-    UVFloat a -> varInfo a
+varInfo :: AllE a => V a -> VarInfo
+varInfo a = case a of
+  V input path init -> (input, path, const' init)
 
 -- | Variables in a program.
-stmtVars :: Statement -> [UV]
+stmtVars :: Statement -> [VarInfo]
 stmtVars a = case a of
-  Assign a b   -> nub $ untype a : exprVars b
+  Assign a b   -> nub $ varInfo a : exprVars b
   Branch a b c -> nub $ exprVars a ++ stmtVars b ++ stmtVars c
   Sequence a b -> nub $ stmtVars a ++ stmtVars b
   Theorem _ _ _ a -> exprVars a
@@ -138,9 +136,9 @@
   Null         -> []
 
 -- | Variables in an expression.
-exprVars :: E a -> [UV]
+exprVars :: E a -> [VarInfo]
 exprVars a = case a of
-  Ref a     -> [untype a]
+  Ref a     -> [varInfo a]
   Const _   -> []
   Add a b   -> exprVars a ++ exprVars b
   Sub a b   -> exprVars a ++ exprVars b
diff --git a/Language/ImProve/Verify.hs b/Language/ImProve/Verify.hs
--- a/Language/ImProve/Verify.hs
+++ b/Language/ImProve/Verify.hs
@@ -69,8 +69,8 @@
   step :: Y ()
   step = do
       addTrace $ Step' 0
-      sequence_ [ getVar' a >>= addTrace . State' (pathName path) | a@(input, path, _) <- sortBy f $ map varInfo $ stmtVars program, not input ]
-      sequence_ [ addVar' a >>= addTrace . Input' (pathName path) | a@(input, path, _) <- sortBy f $ map varInfo $ stmtVars program,     input ]
+      sequence_ [ getVar' a >>= addTrace . State' (pathName path) | a@(input, path, _) <- sortBy f $ stmtVars program, not input ]
+      sequence_ [ addVar' a >>= addTrace . Input' (pathName path) | a@(input, path, _) <- sortBy f $ stmtVars program,     input ]
       evalStmt theorem lemmas (LitB True) program
   f (_, a, _) (_, b, _) = compare a b
 
@@ -92,7 +92,7 @@
   env <- get
   r <- liftIO $ quickCheckY' yices [] $ reverse (cmds env)
           ++ [ASSERT $ NOT $ AND $ asserts env]
-          ++ [ ASSERT $ VarE (var env0 a) := evalConst' c | a@(input, _, c) <- map varInfo $ stmtVars program, not input ]
+          ++ [ ASSERT $ VarE (var env0 a) := evalConst' c | a@(input, _, c) <- stmtVars program, not input ]
           ++ [CHECK]
   return $ result r
 
@@ -234,7 +234,7 @@
   }
  
 initEnv :: Statement -> IO Env
-initEnv program = execStateT (sequence_ [ addVar' a | a@(input, _, _) <- map varInfo $ stmtVars program, not input ]) Env
+initEnv program = execStateT (sequence_ [ addVar' a | a@(input, _, _) <- stmtVars program, not input ]) Env
   { nextId  = 0
   , var     = \ v -> error $ "variable not found in environment: " ++ pathName v
   , cmds    = []
diff --git a/improve.cabal b/improve.cabal
--- a/improve.cabal
+++ b/improve.cabal
@@ -1,5 +1,5 @@
 name:    improve
-version: 0.2.3
+version: 0.3.0
 
 category: Language, Formal Methods, Embedded
 
@@ -9,6 +9,7 @@
   ImProve is an imperative programming language for high assurance applications.
   ImProve uses infinite state, unbounded model checking to verify programs adhere
   to specifications.  Yices (required) is the backend SMT solver.
+  ImProve compiles to C and Simulink.
 
 author:     Tom Hawkins <tomahawkins@gmail.com>
 maintainer: Tom Hawkins <tomahawkins@gmail.com>