diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c)2013, Galois, Inc
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Galois, Inc nor the names of its contributors
+      may be used to endorse or promote products derived from this software
+      without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
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/ivory-backend-c.cabal b/ivory-backend-c.cabal
new file mode 100644
--- /dev/null
+++ b/ivory-backend-c.cabal
@@ -0,0 +1,52 @@
+-- Initial ivory.cabal generated by cabal init.  For further documentation,
+--  see http://haskell.org/cabal/users-guide/
+
+name:                ivory-backend-c
+version:             0.1.0.0
+author:              Galois, Inc.
+maintainer:          leepike@galois.com
+category:            Language
+synopsis:            Ivory C backend.
+description:         Ivory compiler, to a subset of C99.
+homepage:            http://smaccmpilot.org/languages/ivory-introduction.html
+build-type:          Simple
+cabal-version:       >= 1.10
+data-files:             runtime/ivory.h,
+                        runtime/ivory_asserts.h
+license:             BSD3
+license-file:        LICENSE
+source-repository    this
+  type:     git
+  location: https://github.com/GaloisInc/ivory-backend-c
+  tag:      hackage-backend-0100
+
+library
+  exposed-modules:      Ivory.Compile.C,
+                        Ivory.Compile.C.Gen,
+                        Ivory.Compile.C.Modules,
+                        Ivory.Compile.C.Prop,
+                        Ivory.Compile.C.Types,
+                        Ivory.Compile.C.CmdlineFrontend,
+                        Ivory.Compile.C.CmdlineFrontend.Options,
+                        Ivory.Compile.C.SourceDeps
+  other-modules:        Paths_ivory_backend_c
+
+  build-depends:        base >= 4.6 && < 4.7,
+                        language-c-quote >= 0.7.1,
+                        -- XXX remove when inits quasi-quote escape is added
+                        srcloc,
+                        mainland-pretty >= 0.2.5,
+                        monadLib >= 3.7,
+                        template-haskell >= 2.8,
+                        bytestring >= 0.10,
+                        ivory,
+                        ivory-opts,
+                        directory,
+                        filepath,
+                        process,
+                        cmdlib >= 0.3.5,
+                        containers
+  hs-source-dirs:       src
+  default-language:     Haskell2010
+
+  ghc-options:          -Wall
diff --git a/runtime/ivory.h b/runtime/ivory.h
new file mode 100644
--- /dev/null
+++ b/runtime/ivory.h
@@ -0,0 +1,124 @@
+#ifndef IVORY_H
+#define IVORY_H
+
+#include<stdint.h>
+#include<math.h>
+#include<stdbool.h>
+#include<string.h>
+#include<limits.h>
+
+#include "ivory_asserts.h"
+
+#define FOREVER true
+#define FOREVER_INC
+
+/* abs implementations */
+
+#if (CHAR_MIN < 0)
+static inline char abs_char(char i) {
+  COMPILER_ASSERTS(i != CHAR_MIN);
+  return i >= 0 ? i : -i;
+}
+#else
+static inline char abs_char(char i) {
+  return i;
+}
+#endif
+
+static inline int8_t abs_i8(int8_t i) {
+  COMPILER_ASSERTS(i != INT8_MIN);
+  return i >= 0 ? i : -i;
+}
+
+static inline int16_t abs_i16(int16_t i) {
+  COMPILER_ASSERTS(i != INT16_MIN);
+  return i >= 0 ? i : -i;
+}
+
+static inline int32_t abs_i32(int32_t i) {
+  COMPILER_ASSERTS(i != INT32_MIN);
+  return i >= 0 ? i : -i;
+}
+
+static inline int64_t abs_i64(int64_t i) {
+  COMPILER_ASSERTS(i != INT64_MIN);
+  return i >= 0 ? i : -i;
+}
+
+/* signum implementations */
+
+#if (CHAR_MIN < 0)
+static inline char signum_char(char i) {
+  if (i > 0) return 1;
+  if (i < 0) return (-1);
+  return 0;
+}
+#else
+static inline char signum_char(char i) {
+  if (i > 0) return 1;
+  return 0;
+}
+#endif
+
+static inline int8_t signum_i8(int8_t i) {
+  if (i > 0) return 1;
+  if (i < 0) return (-1);
+  return 0;
+}
+
+static inline int16_t signum_i16(int16_t i) {
+  if (i > 0) return 1;
+  if (i < 0) return (-1);
+  return 0;
+}
+
+static inline int32_t signum_i32(int32_t i) {
+  if (i > 0) return 1;
+  if (i < 0) return (-1);
+  return 0;
+}
+
+static inline int64_t signum_i64(int64_t i) {
+  if (i > 0) return 1;
+  if (i < 0) return (-1);
+  return 0;
+}
+
+static inline float signum_float(float i) {
+  if (i > 0) return 1;
+  if (i < 0) return (-1);
+  return 0;
+}
+
+static inline double signum_double(double i) {
+  if (i > 0) return 1;
+  if (i < 0) return (-1);
+  return 0;
+}
+
+static inline uint8_t signum_u8(uint8_t i) {
+  if (i > 0) return 1;
+  return 0;
+}
+
+static inline uint16_t signum_u16(uint16_t i) {
+  if (i > 0) return 1;
+  return 0;
+}
+
+static inline uint32_t signum_u32(uint32_t i) {
+  if (i > 0) return 1;
+  return 0;
+}
+
+static inline uint64_t signum_u64(uint64_t i) {
+  if (i > 0) return 1;
+  return 0;
+}
+
+/* index type */
+
+/* machine-depdentent size */
+typedef int idx;
+
+#endif // IVORY_H
diff --git a/runtime/ivory_asserts.h b/runtime/ivory_asserts.h
new file mode 100644
--- /dev/null
+++ b/runtime/ivory_asserts.h
@@ -0,0 +1,50 @@
+#ifndef IVORY_ASSERTS_H
+#define IVORY_ASSERTS_H
+
+/* Requires and Provides statements */
+
+#ifdef IVORY_TEST
+
+#ifdef __arm__
+
+/* TODO: We could write a better "assert" that suspends all RTOS
+ * tasks and tries to write a debug string somewhere, but this is at
+ * least somewhat useful while running under GDB. */
+#define ivory_assert(arg)         \
+  do {                            \
+    if (!(arg)) {                 \
+      asm volatile("bkpt");       \
+    }                             \
+  } while (0)
+
+#define REQUIRES(arg)         ivory_assert(arg)
+#define ENSURES(arg)          ivory_assert(arg)
+#define ASSUMES(arg)          ivory_assert(arg)
+#define ASSERTS(arg)          ivory_assert(arg)
+#define COMPILER_ASSERTS(arg) ivory_assert(arg)
+
+#else /* ! __arm__ */
+
+#include <assert.h>
+
+#define REQUIRES(arg)         assert(arg)
+#define ENSURES(arg)          assert(arg)
+#define ASSUMES(arg)          assert(arg)
+#define ASSERTS(arg)          assert(arg)
+#define COMPILER_ASSERTS(arg) assert(arg)
+
+#endif /* __arm__ */
+
+#endif /* IVORY_TEST */
+
+#ifdef IVORY_DEPLOY
+
+#define REQUIRES(arg)
+#define ENSURES(arg)
+#define ASSUMES(arg)
+#define ASSERTS(arg)
+#define COMPILER_ASSERTS(arg)
+
+#endif /* IVORY_DEPLOY */
+
+#endif /* IVORY_ASSERTS_H */
diff --git a/src/Ivory/Compile/C.hs b/src/Ivory/Compile/C.hs
new file mode 100644
--- /dev/null
+++ b/src/Ivory/Compile/C.hs
@@ -0,0 +1,18 @@
+module Ivory.Compile.C
+  ( compile
+  , compileModule
+  , runOpt
+  , showModule
+  , writeHdr
+  , writeSrc
+  , renderHdr
+  , renderSrc
+  , CompileUnits(..)
+  , outputProcSyms
+  ) where
+
+-- Umbrella module
+
+import Ivory.Compile.C.Gen
+import Ivory.Compile.C.Modules
+import Ivory.Compile.C.Types
diff --git a/src/Ivory/Compile/C/CmdlineFrontend.hs b/src/Ivory/Compile/C/CmdlineFrontend.hs
new file mode 100644
--- /dev/null
+++ b/src/Ivory/Compile/C/CmdlineFrontend.hs
@@ -0,0 +1,201 @@
+
+module Ivory.Compile.C.CmdlineFrontend
+  ( compile
+  , compileWith
+  , runCompiler
+  , runCompilerWith
+  , Opts(..), parseOpts, printUsage
+  , initialOpts
+  ) where
+
+import qualified Paths_ivory_backend_c
+import qualified Ivory.Compile.C as C
+import qualified Ivory.Compile.C.SourceDeps as C
+
+import           Ivory.Compile.C.CmdlineFrontend.Options
+
+import           Ivory.Language
+import qualified Ivory.Opts.ConstFold as O
+import qualified Ivory.Opts.Overflow as O
+import qualified Ivory.Opts.DivZero as O
+import qualified Ivory.Opts.Index as O
+import qualified Ivory.Opts.FP as O
+import qualified Ivory.Opts.CFG as G
+
+import qualified Data.ByteString.Char8 as B
+
+import Control.Monad (when)
+import Data.List (foldl')
+import System.Directory (doesFileExist,createDirectoryIfMissing)
+import System.Environment (getArgs)
+import System.FilePath (takeDirectory,takeExtension,addExtension,(</>))
+import Text.PrettyPrint.Mainland
+    ((<+>),(<>),line,text,stack,punctuate,render,empty,indent,displayS)
+import qualified System.FilePath.Posix as PFP
+
+
+-- Code Generation Front End ---------------------------------------------------
+
+compile :: [Module] -> IO ()
+compile = compileWith Nothing Nothing
+
+compileWith :: Maybe G.SizeMap -> Maybe [IO FilePath] -> [Module] -> IO ()
+compileWith sm sp ms = runCompilerWith sm sp ms =<< parseOpts =<< getArgs
+
+runCompilerWith :: Maybe G.SizeMap -> Maybe [IO FilePath] -> [Module] -> Opts -> IO ()
+runCompilerWith sm sp =
+  rc (maybe G.defaultSizeMap id sm) (maybe [] id sp)
+
+runCompiler :: [Module] -> Opts -> IO ()
+runCompiler = runCompilerWith Nothing Nothing
+
+rc :: G.SizeMap -> [IO FilePath] -> [Module] -> Opts -> IO ()
+rc sm userSearchPath modules opts
+  | outProcSyms opts = C.outputProcSyms modules
+  | printDeps        = runDeps
+  | otherwise        = do
+    if stdOut opts then mapM_ showM_ cmodules else run
+    -- CFG stuff
+    when (cfg opts) $ do
+      cfs <- mapM (\p -> G.callGraphDot p (cfgDotDir opts) optModules) cfgps
+      let maxstacks = map ms (zip cfgps cfs)
+      mapM_ maxStackMsg (zip cfgps maxstacks)
+  where
+  ivoryHeaders = ["ivory.h", "ivory_asserts.h"]
+
+  run = do
+    searchPath <- mkSearchPath opts userSearchPath
+    createDirectoryIfMissing True (includeDir opts)
+    createDirectoryIfMissing True (srcDir opts)
+    outputHeaders (includeDir opts) cmodules
+    outputSources (srcDir opts) cmodules
+    C.outputSourceDeps (includeDir opts) (srcDir opts)
+       (map ("runtime/" ++) ivoryHeaders ++ (C.collectSourceDeps modules)) searchPath
+
+  runDeps =
+    outputDeps (deps opts) (depPrefix opts) (genHs ++ cpyHs) (genSs ++ cpySs)
+    where
+    sdeps = C.collectSourceDeps modules
+    genHs = map (mkDep (includeDir opts) ".h") cmodules
+    genSs = map (mkDep (srcDir opts) ".c")     cmodules
+    cpyHs = map (mkDepSourceDep (includeDir opts)) $
+              filter (\p -> takeExtension p == ".h") sdeps
+    cpySs = map (mkDepSourceDep (srcDir opts)) $
+              filter (\p -> takeExtension p == ".c") sdeps
+
+  optModules = map (C.runOpt passes) modules
+
+  cfgps = cfgProc opts
+
+  ms (p, cf) = G.maxStack p cf sm
+  maxStackMsg :: (String, G.WithTop Integer) -> IO ()
+  maxStackMsg (p,res) =
+    putStrLn $ "Maximum stack usage from function " ++ p ++ ": " ++ show res
+
+  cmodules   = map C.compileModule optModules
+
+  printDeps = not (null (deps opts))
+
+  showM_ mods = do
+    mapM_ (mapM_ putStrLn) (C.showModule mods)
+
+  cfPass = mkPass constFold O.constFold
+
+  -- Put new assertion passes here and add them to passes below.
+  ofPass = mkPass overflow O.overflowFold
+  dzPass = mkPass divZero O.divZeroFold
+  fpPass = mkPass fpCheck O.fpFold
+  ixPass = mkPass ixCheck O.ixFold
+
+  mkPass passOpt pass = if passOpt opts then pass else id
+
+  -- Constant folding before and after all other passes.
+  passes e = foldl' (flip ($)) e
+    [ cfPass
+    , ofPass, dzPass, fpPass, ixPass
+    , cfPass
+    ]
+
+  -- Output headers in a directory
+  outputHeaders :: FilePath -> [C.CompileUnits] -> IO ()
+  outputHeaders fp cus = mapM_ (process outputHeader fp) cus
+  -- Output sources in a directory
+  outputSources :: FilePath -> [C.CompileUnits] -> IO ()
+  outputSources fp cus = mapM_ (process outputSrc fp) cus
+
+  process outputter dir m = outputter (dir </> (C.unitName m)) m
+
+  -- Transform a compiled unit into a header, and write to a .h file
+  outputHeader :: FilePath -> C.CompileUnits -> IO ()
+  outputHeader basename cm = do
+    let headerfname = addExtension basename ".h"
+        header = C.renderHdr (C.headers cm) (C.unitName cm)
+    outputHelper headerfname header
+
+  -- Transform a compiled unit into a c src, and write to a .c file
+  outputSrc :: FilePath -> C.CompileUnits -> IO ()
+  outputSrc basename cm = do
+    let srcfname = addExtension basename ".c"
+        src = C.renderSrc (C.sources cm)
+    outputHelper srcfname src
+
+  outputHelper :: FilePath -> String -> IO ()
+  outputHelper fname contents = case verbose opts of
+    False -> out
+    True -> do
+      putStr ("Writing to file " ++ fname ++ "...")
+      out
+      putStrLn " Done"
+    where
+    out = writeFile fname contents
+
+--------------------------------------------------------------------------------
+
+mkDep :: FilePath -> String -> C.CompileUnits -> String
+mkDep basepath extension unit = basepath PFP.</> (C.unitName unit) PFP.<.> extension
+
+mkDepSourceDep :: FilePath -> FilePath -> String
+mkDepSourceDep basepath sdep = basepath PFP.</> sdep
+
+outputDeps :: FilePath -> String -> [String] -> [String] -> IO ()
+outputDeps path prefix headers sources = do
+  createDirectoryIfMissing True (takeDirectory path)
+  outputIfChanged path docstring
+  where
+  docstring = displayS (render w d) ""
+  w = 10000000 -- don't ever wrap lines - invalid make syntax
+  d = stack $
+    [ text "# dep file autogenerated by ivory compiler"
+    , empty
+    , listof (prefix ++ "_HEADERS") headers
+    , empty
+    , listof (prefix ++ "_SOURCES") sources
+    ]
+  declaration n = text n <+> text ":= \\" <> line
+  listof name values = declaration name <>
+    (indent 4 $ stack $ punctuate (text " \\") (map text values))
+
+outputIfChanged :: FilePath -> String -> IO ()
+outputIfChanged path string_contents = do
+  let contents = B.pack string_contents
+  exists <- doesFileExist path
+  case exists of
+    False -> B.writeFile path contents
+    True -> do
+      existing <- B.readFile path
+      case existing == contents of
+          True -> return ()
+          False -> B.writeFile path contents
+
+
+mkSearchPath :: Opts -> [IO FilePath] -> IO [FilePath]
+mkSearchPath opts userSearchPaths = do
+  rtPath <- getRtPath
+  users <- sequence userSearchPaths
+  return $ rtPath:users
+  where
+  getRtPath :: IO FilePath
+  getRtPath  = case rtIncludeDir opts of
+    Just path -> return path
+    Nothing   -> Paths_ivory_backend_c.getDataDir
+
diff --git a/src/Ivory/Compile/C/CmdlineFrontend/Options.hs b/src/Ivory/Compile/C/CmdlineFrontend/Options.hs
new file mode 100644
--- /dev/null
+++ b/src/Ivory/Compile/C/CmdlineFrontend/Options.hs
@@ -0,0 +1,221 @@
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE GADTs #-}
+
+module Ivory.Compile.C.CmdlineFrontend.Options where
+
+import Data.Monoid (Monoid(..),mconcat)
+import System.Console.GetOpt
+    (ArgOrder(Permute),OptDescr(..),ArgDescr(..),getOpt,usageInfo)
+
+import System.Environment (getProgName)
+import System.Exit (exitFailure,exitSuccess)
+
+-- Option Parsing --------------------------------------------------------------
+
+data OptParser opt
+  = Success (opt -> opt)
+  | Error [String]
+
+instance Monoid (OptParser opt) where
+  mempty                        = Success id
+
+  -- left-to-right composition makes the last option parsed take precedence
+  Success f `mappend` Success g = Success (f . g)
+  Error as  `mappend` Error bs  = Error (as ++ bs)
+  Error as  `mappend` _         = Error as
+  _         `mappend` Error bs  = Error bs
+
+-- | Option parser succeeded, use this function to transform the default
+-- options.
+success :: (opt -> opt) -> OptParser opt
+success  = Success
+
+-- | Option parser failed, emit this message.
+--
+-- XXX currently not used.
+--invalid :: String -> OptParser opt
+--invalid msg = Error [msg]
+
+
+-- | Yield either a list of errors, or a function to produce an options
+-- structure, given a set of default options.  Discard any non-options.
+parseOptions :: [OptDescr (OptParser opt)] -> [String]
+             -> (Either [String] (opt -> opt))
+parseOptions opts args = case getOpt Permute opts args of
+  (fs,[],[]) -> case mconcat fs of
+    Success f -> Right f
+    Error es  -> Left es
+  (_,_,es)  -> Left es
+
+
+
+-- Command Line Options --------------------------------------------------------
+
+data Opts = Opts
+  { stdOut      :: Bool
+  , includeDir  :: FilePath
+  , srcDir      :: FilePath
+  -- dependencies
+  , deps        :: FilePath
+  , depPrefix   :: String
+  , rtIncludeDir:: Maybe FilePath
+  -- optimization passes
+  , constFold   :: Bool
+  , overflow    :: Bool
+  , divZero     :: Bool
+  , ixCheck     :: Bool
+  , fpCheck     :: Bool
+  , outProcSyms :: Bool
+  -- CFG stuff
+  , cfg         :: Bool
+  , cfgDotDir   :: FilePath
+  , cfgProc     :: [String]
+  -- debugging
+  , verbose     :: Bool
+
+  , help        :: Bool
+  } deriving (Show)
+
+initialOpts :: Opts
+initialOpts  = Opts
+  { stdOut       = False
+  , includeDir   = ""
+  , srcDir       = ""
+
+  -- dependencies
+  , deps         = ""
+  , depPrefix    = ""
+  , rtIncludeDir = Nothing
+
+  -- optimization passes
+  , constFold    = False
+  , overflow     = False
+  , divZero      = False
+  , ixCheck      = False
+  , fpCheck      = False
+  , outProcSyms  = False
+
+  -- CFG stuff
+  , cfg          = False
+  , cfgDotDir    = ""
+  , cfgProc      = []
+  -- debugging
+  , verbose      = False
+
+  , help         = False
+  }
+
+setStdOut :: OptParser Opts
+setStdOut  = success (\opts -> opts { stdOut = True } )
+
+setIncludeDir :: String -> OptParser Opts
+setIncludeDir str = success (\opts -> opts { includeDir = str })
+
+setSrcDir :: String -> OptParser Opts
+setSrcDir str = success (\opts -> opts { srcDir = str })
+
+setDeps :: String -> OptParser Opts
+setDeps str = success (\opts -> opts { deps = str })
+
+setDepPrefix :: String -> OptParser Opts
+setDepPrefix str = success (\opts -> opts { depPrefix = str })
+
+setRtIncludeDir :: String -> OptParser Opts
+setRtIncludeDir str = success (\opts -> opts { rtIncludeDir = Just str })
+
+setConstFold :: OptParser Opts
+setConstFold  = success (\opts -> opts { constFold = True })
+
+setOverflow :: OptParser Opts
+setOverflow  = success (\opts -> opts { overflow = True })
+
+setDivZero :: OptParser Opts
+setDivZero  = success (\opts -> opts { divZero = True })
+
+setIxCheck :: OptParser Opts
+setIxCheck  = success (\opts -> opts { ixCheck = True })
+
+setFpCheck :: OptParser Opts
+setFpCheck  = success (\opts -> opts { fpCheck = True })
+
+setProcSyms :: OptParser Opts
+setProcSyms  = success (\opts -> opts { outProcSyms = True })
+
+setCfg :: OptParser Opts
+setCfg  = success (\opts -> opts { cfg = True })
+
+setCfgDotDir :: String -> OptParser Opts
+setCfgDotDir str = success (\opts -> opts { cfgDotDir = str })
+
+addCfgProc :: String -> OptParser Opts
+addCfgProc str = success (\opts -> opts { cfgProc = cfgProc opts ++ [str] })
+
+setVerbose :: OptParser Opts
+setVerbose  = success (\opts -> opts { verbose = True })
+
+setHelp :: OptParser Opts
+setHelp  = success (\opts -> opts { help = True })
+
+options :: [OptDescr (OptParser Opts)]
+options  =
+  [ Option "" ["std-out"] (NoArg setStdOut)
+    "print to stdout only"
+  , Option "" ["include-dir"] (ReqArg setIncludeDir "PATH")
+    "output directory for header files"
+  , Option "" ["src-dir"] (ReqArg setSrcDir "PATH")
+    "output directory for source files"
+
+  , Option "" ["dep-file"] (ReqArg setDeps "FILE")
+    "makefile dependency output"
+  , Option "" ["dep-prefix"] (ReqArg setDepPrefix "STRING")
+    "makefile dependency prefix"
+  , Option "" ["rt-include-dir"] (ReqArg setRtIncludeDir "PATH")
+    "path to ivory runtime includes"
+
+  , Option "" ["const-fold"] (NoArg setConstFold)
+    "enable the constant folding pass"
+  , Option "" ["overflow"] (NoArg setOverflow)
+    "enable overflow checking annotations"
+  , Option "" ["div-zero"] (NoArg setDivZero)
+    "generate assertions checking for division by zero."
+  , Option "" ["ix-check"] (NoArg setIxCheck)
+    "generate assertions checking for back indexes (e.g., negative)"
+  , Option "" ["fp-check"] (NoArg setFpCheck)
+    "generate assertions checking for NaN and Infinitiy."
+
+  , Option "" ["out-proc-syms"] (NoArg setProcSyms)
+    "dump out the modules' function symbols"
+
+  , Option "" ["cfg"] (NoArg setCfg)
+    "Output control-flow graph and max stack usage."
+
+  , Option "" ["cfg-dot-dir"] (ReqArg setCfgDotDir "PATH")
+    "output directory for CFG Graphviz file"
+  , Option "" ["cfg-proc"] (ReqArg addCfgProc "NAME")
+    "entry function(s) for CFG computation."
+
+  , Option "" ["verbose"] (NoArg setVerbose)
+    "verbose debugging output"
+
+  , Option "h" ["help"] (NoArg setHelp)
+    "display this message"
+  ]
+
+-- | Parse an @Opts@ structure from a list of strings.
+parseOpts :: [String] -> IO Opts
+parseOpts args = case parseOptions options args of
+  Right f   ->
+    let opts = f initialOpts
+     in if help opts
+           then printUsage [] >> exitSuccess
+           else return opts
+  Left errs -> printUsage errs >> exitFailure
+
+printUsage :: [String] -> IO ()
+printUsage errs = do
+  prog <- getProgName
+  let banner = unlines
+        (errs ++ ["", "Usage: " ++ prog ++ " [OPTIONS]"])
+  putStrLn (usageInfo banner options)
+
+
diff --git a/src/Ivory/Compile/C/Gen.hs b/src/Ivory/Compile/C/Gen.hs
new file mode 100644
--- /dev/null
+++ b/src/Ivory/Compile/C/Gen.hs
@@ -0,0 +1,633 @@
+{-# LANGUAGE PackageImports #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE CPP#-}
+
+-- | Ivory backend targeting language-c-quote.
+
+module Ivory.Compile.C.Gen where
+
+import qualified "language-c-quote" Language.C.Syntax as C
+import Language.C.Quote.GCC
+
+import qualified Ivory.Language.Syntax as I
+import qualified Ivory.Language.Proc as P
+
+import Ivory.Compile.C.Types
+import Ivory.Compile.C.Prop
+
+import Prelude hiding (exp, abs, signum)
+import qualified Prelude as P
+import Data.List (foldl')
+
+import Data.Loc (noLoc)
+
+data Visibility = Public | Private deriving (Show, Eq)
+
+--------------------------------------------------------------------------------
+-- | Compile a top-level element.
+compile :: P.Def a -> Compile
+compile (P.DefProc fun) = compileUnit fun
+compile (P.DefExtern e) = compileExtern e
+compile (P.DefImport _) = error "Can't compile an import!"
+
+--------------------------------------------------------------------------------
+-- | Compile an extern declaration
+compileExtern :: I.Extern -> Compile
+compileExtern I.Extern
+  { I.externSym     = sym
+  , I.externRetType = ret
+  , I.externArgs    = args
+  }
+  = putExt [cedecl| extern $ty:(toType ret) $id:(sym)
+                      ($params:(map mkParam args)) ; |]
+  where
+  mkParam ty = [cparam| $ty:(toType ty) |]
+
+--------------------------------------------------------------------------------
+-- | Compile a struct.
+compileStruct :: Visibility -> I.Struct -> Compile
+compileStruct visibility def = case def of
+  I.Struct n fs    ->
+    (if visibility == Public then putHdrSrc else putSrc)
+    [cedecl| struct $id:n { $sdecls:(map mkFieldGroup fs)
+                          } __attribute__ ((__packed__)) ;
+           |]
+  I.Abstract _ file ->
+    putHdrInc (SysInclude file)
+
+mkFieldGroup :: I.Typed String -> C.FieldGroup
+mkFieldGroup field =
+  [csdecl| $ty:(toType (I.tType field)) $id:(I.tValue field) ; |]
+
+--------------------------------------------------------------------------------
+-- | Compile an external memory area reference.
+compileAreaImport :: I.AreaImport -> Compile
+compileAreaImport ai = putSrcInc (SysInclude (I.aiFile ai))
+
+--------------------------------------------------------------------------------
+-- | Get prototypes for memory areas.
+extractAreaProto :: Visibility -> I.Area -> Compile
+extractAreaProto visibility area = do
+  let aty                   = toType (I.areaType area)
+      ty | I.areaConst area = [cty| const $ty:aty |]
+         | otherwise        = aty
+  if visibility == Public
+    then putHdrSrc [cedecl| extern $ty:ty $id:(I.areaSym area); |]
+    else putSrc    [cedecl| static $ty:ty $id:(I.areaSym area); |]
+
+-- | Compile a memory area definition into an extern in the header, and a
+-- structure in the source.
+compileArea :: Visibility -> I.Area -> Compile
+compileArea visibility area = do
+  let aty                   = toType (I.areaType area)
+      i                     = I.areaInit area
+      ty | I.areaConst area = [cty| const $ty:aty |]
+         | otherwise        = aty
+  case i of
+    I.InitZero -> putSrc [cedecl| $ty:(type' visibility ty) $id:(I.areaSym area) ; |]
+    _          -> putSrc [cedecl| $ty:(type' visibility ty)
+                                 $id:(I.areaSym area) = $init:(toInit i) ; |]
+  where
+  type' Public ty' = [cty|$ty:ty'|]
+  type' Private ty' = [cty|static $ty:ty'|]
+
+--------------------------------------------------------------------------------
+-- | Compile a definition unit.
+compileUnit :: I.Proc -> Compile
+compileUnit I.Proc { I.procSym      = sym
+                   , I.procRetTy    = ret
+                   , I.procArgs     = args
+                   , I.procBody     = body
+                   , I.procRequires = requires
+                   , I.procEnsures  = ensures
+                   }
+  = do let ens  = map I.getEnsure ensures
+       let bd   = concatMap (toBody ens) body
+       let reqs = map (toRequire . I.getRequire) requires
+       putSrc [cedecl| $ty:(toType ret) ($id:sym) ($params:(toArgs args))
+                         { $items:reqs
+                           $items:bd
+                         } |]
+
+--------------------------------------------------------------------------------
+-- | Get the prototypes.
+extractProto :: Visibility -> I.Proc -> Compile
+extractProto visibility I.Proc { I.procSym   = sym
+                               , I.procRetTy = ret
+                               , I.procArgs  = args
+                               }
+  = if visibility == Public
+       then putHdrSrc
+         [cedecl| $ty:(toType ret) ($id:sym) ($params:(toArgs args)); |]
+       else putSrc
+         [cedecl| static $ty:(toType ret) ($id:sym) ($params:(toArgs args)); |]
+
+--------------------------------------------------------------------------------
+
+-- | Argument conversion.
+toArgs :: [I.Typed I.Var] -> [C.Param]
+toArgs = foldl' go [] . reverse
+  where
+  go acc I.Typed { I.tType  = t
+                 , I.tValue = v }
+    = [cparam| $ty:(toType t) $id:(toVar v) |] : acc
+
+toParam :: C.Type -> C.Param
+toParam ty = case ty of
+  C.Type spec decl loc -> C.Param Nothing spec decl loc
+  _                    -> error "toParam: unexpected anti-quote"
+
+-- | Type conversion outside of an assignment context.  This converts arrays to
+-- arrays, and carrays to pointers.
+toType :: I.Type -> C.Type
+toType  = toTypeCxt $ \ t -> case t of
+  I.TyCArray t'  -> [cty| $ty:(toType t') *          |]
+  I.TyArr len t' -> [cty| $ty:(toType t')[$uint:len] |]
+  _              -> [cty| $ty:(toType t) *           |]
+
+
+-- | Type conversion in the context of an assignment.
+-- This converts all arrays/carrays to pointers.
+toTypeAssign :: I.Type -> C.Type
+toTypeAssign  = toTypeCxt $ \ t -> case t of
+  I.TyCArray t'  -> [cty| $ty:(toTypeAssign t') * |]
+  I.TyArr _   t' -> [cty| $ty:(toTypeAssign t') * |]
+  _              -> [cty| $ty:(toTypeAssign t)  * |]
+
+--------------------------------------------------------------------------------
+-- | C type conversion, with a special case for references and pointers.
+toTypeCxt :: (I.Type -> C.Type) -> I.Type -> C.Type
+toTypeCxt arrCase = convert
+  where
+  convert ty = case ty of
+    I.TyVoid              -> [cty| void |]
+    I.TyChar              -> [cty| char |]
+    I.TyInt i             -> intSize i
+    I.TyWord w            -> wordSize w
+    I.TyBool              -> [cty| typename bool |]
+    I.TyFloat             -> [cty| float |]
+    I.TyDouble            -> [cty| double |]
+    I.TyStruct nm         -> [cty| struct $id:nm |]
+    I.TyConstRef t        -> [cty| const $ty:(arrCase t) |]
+    -- Reference is a guaranted non-NULL pointer.
+    I.TyRef t             -> arrCase t
+    I.TyPtr t             -> arrCase t
+    I.TyArr len t         -> [cty| $ty:(convert t)[$uint:len] |]
+    I.TyCArray t          -> [cty| $ty:(convert t) * |]
+    I.TyProc retTy argTys ->
+      [cty| $ty:(convert retTy) (*)
+            ($params:(map (toParam . convert) argTys)) |]
+    I.TyOpaque            -> error "Opaque type is not implementable."
+
+intSize :: I.IntSize -> C.Type
+intSize I.Int8  = [cty| typename int8_t  |]
+intSize I.Int16 = [cty| typename int16_t |]
+intSize I.Int32 = [cty| typename int32_t |]
+intSize I.Int64 = [cty| typename int64_t |]
+
+wordSize :: I.WordSize -> C.Type
+wordSize I.Word8  = [cty| typename uint8_t  |]
+wordSize I.Word16 = [cty| typename uint16_t |]
+wordSize I.Word32 = [cty| typename uint32_t |]
+wordSize I.Word64 = [cty| typename uint64_t |]
+
+--------------------------------------------------------------------------------
+-- | Call Symbols
+toName :: I.Name -> String
+toName name = case name of
+  I.NameSym s   -> s
+  I.NameVar var -> toVar var
+
+-- | Variable name mangling.
+toVar :: I.Var -> String
+toVar var = case var of
+  I.VarName n     -> "n_" ++ n
+  I.VarInternal n -> "i_" ++ n
+  I.VarLitName n  -> n
+
+--------------------------------------------------------------------------------
+
+-- | Translate statements.
+toBody :: [I.Cond] -> I.Stmt -> [C.BlockItem]
+toBody ens stmt =
+  let toBody' = toBody ens in
+  case stmt of
+    I.Assign t v exp       ->
+      [C.BlockDecl [cdecl| $ty:(toTypeAssign t) $id:(toVar v)
+                         = $exp:(toExpr t exp); |]]
+    I.IfTE exp blk0 blk1   ->
+      let ifBd   = concatMap toBody' blk0 in
+      let elseBd = concatMap toBody' blk1 in
+      if null elseBd
+        then [C.BlockStm [cstm| if($exp:(toExpr I.TyBool exp)) {
+                                  $items:ifBd } |]]
+        else [C.BlockStm [cstm| if($exp:(toExpr I.TyBool exp)) {
+                                  $items:ifBd }
+                                else { $items:elseBd } |]]
+    I.Return exp           ->
+           map (toEnsure $ I.tValue exp) ens
+        ++ [C.BlockStm [cstm| return $exp:(typedRet exp); |]]
+    I.ReturnVoid           -> [C.BlockStm [cstm| return; |]]
+
+    -- t is the referenced type.  Should only be able to deref a stored value.
+    -- We replicate some of the type deconstruction in parsing expressions to
+    -- optimize away *& constructions on dereferncing structs and indexes into
+    -- arrays.
+    I.Deref t var exp      -> [C.BlockDecl
+      [cdecl| $ty:(toType t) $id:(toVar var) = $exp:deref; |]]
+      where
+      deref = case t of
+                I.TyArr _ _  -> [cexp| * $exp:e |]
+                I.TyCArray _ -> [cexp| * $exp:e |]
+                _            -> [cexp|   $exp:e |]
+      e = case exp of
+            I.ExpLabel t' e' field ->
+              [cexp| $exp:(toExpr (I.TyRef t') e') -> $id:field |]
+            I.ExpIndex t' e' ti i  ->
+              [cexp| $exp:(toExpr (I.TyRef t') e') [$exp:(toExpr ti i)] |]
+            _                      -> [cexp| * $exp:(toExpr (I.TyRef t) exp) |]
+
+    I.Local t var inits    -> [C.BlockDecl
+      [cdecl| $ty:(toType t) $id:(toVar var) = $init:(toInit inits); |]]
+    -- Can't do a static check since we have local let bindings.
+    I.RefCopy t vto vfrom  ->
+      [C.BlockStm [cstm| if( $exp:toRef != $exp:fromRef) {
+         memcpy( $exp:toRef, $exp:fromRef, sizeof($ty:(toType t)) ); }
+                           else { COMPILER_ASSERTS(false); }
+      |]]
+      where
+      toRef   = toExpr (I.TyRef t) vto
+      fromRef = toExpr (I.TyRef t) vfrom
+
+    -- Should only be a reference (not a pointer).
+    I.AllocRef t l r       -> [C.BlockDecl
+        [cdecl| $ty:(toType (I.TyRef rty)) $id:(toVar l) = $exp:rhs; |]]
+      where
+      name      = toName r
+      (rhs,rty) = case t of
+        I.TyArr _ t'  -> ([cexp| $id:name    |], t')
+        I.TyCArray t' -> ([cexp| $id:name    |], t')
+        _             -> ([cexp| &($id:name) |], t)
+    I.Assert exp           -> [C.BlockStm
+      [cstm| ASSERTS($exp:(toExpr I.TyBool exp)); |]]
+    I.CompilerAssert exp   -> [C.BlockStm
+      [cstm| COMPILER_ASSERTS($exp:(toExpr I.TyBool exp)); |]]
+    I.Assume exp           -> [C.BlockStm
+      [cstm| ASSUMES($exp:(toExpr I.TyBool exp)); |]]
+    I.Call t mVar sym args ->
+      case mVar of
+        Nothing  -> -- Just call the fuction.
+          [C.BlockStm [cstm| $id:(toName sym)($args:(map go args)); |]]
+        Just var -> -- Call it and assign it a value.
+          [C.BlockDecl [cdecl| $ty:(toType t) $id:(toVar var) =
+                                 $id:(toName sym)($args:(map go args));
+                      |]]
+        where
+        go I.Typed { I.tType = t'
+                   , I.tValue = v }
+          = toExpr t' v
+    -- Assume that ty is a signed and sufficiently big (int).
+    I.Loop var start incr blk ->
+      let loopBd =  concatMap toBody' blk in
+      [C.BlockStm [cstm| for( $ty:(toType ty) $id:(toVar var)
+                                = $exp:(toExpr ty start);
+                              $exp:test;
+                              $exp:incExp ) {
+                       $items:loopBd } |]]
+      where
+      ty = I.TyInt I.Int32
+      (test,incExp)  = toIncr incr
+      ix = toVar var
+      toIncr (I.IncrTo to) =
+        ( [cexp| $id:ix <= $exp:(toExpr ty to) |]
+        , [cexp| $id:ix++ |] )
+      toIncr (I.DecrTo to) =
+        ( [cexp| $id:ix >= $exp:(toExpr ty to) |]
+        , [cexp| $id:ix-- |] )
+
+    I.Forever blk ->
+      let foreverBd =  concatMap toBody' blk
+          foreverDecl = C.BlockDecl
+            [cdecl| int forever_loop __attribute__((unused)); |]
+          loop = C.BlockStm [cstm| for( forever_loop = 0
+                                      ; FOREVER
+                                      ; FOREVER_INC ) { $items:foreverBd } |]
+          decAndLoop = [ foreverDecl, loop ]
+      in  [ C.BlockStm [cstm| { $items:decAndLoop } |] ]
+
+    I.Break                       -> [C.BlockStm [cstm| break; |]]
+    I.Store t ptr exp             -> [C.BlockStm
+      [cstm| * $exp:(toExpr (I.TyRef t) ptr) = $exp:(toExpr t exp); |]]
+
+-- | Return statement.
+typedRet :: I.Typed I.Expr -> C.Exp
+typedRet I.Typed { I.tType  = t
+                 , I.tValue = exp }
+    = [cexp| $exp:(toExpr t exp) |]
+
+--------------------------------------------------------------------------------
+
+toInit :: I.Init -> C.Initializer
+toInit i = case i of
+  I.InitZero      -> [cinit|{$inits:([])}|] -- {}
+  I.InitExpr ty e -> [cinit|$exp:(toExpr ty e)|]
+  I.InitArray is  -> [cinit|{$inits:([ toInit j | j <- is ])}|]
+  I.InitStruct fs ->
+    C.CompoundInitializer [ (Just (fieldDes f), toInit j) | (f,j) <- fs ] noLoc
+
+fieldDes :: String -> C.Designation
+fieldDes n = C.Designation [ C.MemberDesignator (C.Id n noLoc) noLoc ] noLoc
+
+--------------------------------------------------------------------------------
+
+-- | Translate an expression.
+toExpr :: I.Type -> I.Expr -> C.Exp
+----------------------------------------
+toExpr _ (I.ExpVar var)  = [cexp| $id:(toVar var) |]
+----------------------------------------
+toExpr t (I.ExpLit lit)  =
+  case lit of
+    -- XXX hack: should make type-correct literals.
+    I.LitInteger i -> [cexp| ($ty:(toType t))$id:fromInt |]
+      where fromInt = case t of
+                        I.TyWord _  -> show i ++ "U"
+                        I.TyInt  _  -> show i
+                        I.TyFloat   -> show (fromIntegral i :: Float) ++ "F"
+                        I.TyDouble  -> show (fromIntegral i :: Double)
+                        _           -> error ("Nonint type " ++ (show t) ++
+                                              " of literal " ++ (show i) )
+    I.LitChar c    -> [cexp| $char:c |]
+    I.LitBool b    -> [cexp| $id:(if b then "true" else "false") |]
+    I.LitNull      -> [cexp| NULL |]
+    I.LitString s  -> [cexp| $string:s |]
+    I.LitFloat f   -> [cexp| $id:(show f ++ "f") |]
+    I.LitDouble d  -> [cexp| $id:(show d) |]
+----------------------------------------
+toExpr t (I.ExpOp op args) = [cexp| ($ty:(toType t)) $exp:(toExpOp t op args) |]
+----------------------------------------
+toExpr _ (I.ExpSym sym) = [cexp| $id:sym |]
+----------------------------------------
+toExpr t (I.ExpLabel t' e field) = case t of
+  I.TyRef (I.TyArr _ _)       -> getField
+  I.TyRef (I.TyCArray _)      -> getField
+  I.TyConstRef (I.TyArr _ _)  -> getField
+  I.TyConstRef (I.TyCArray _) -> getField
+  _                           ->
+    [cexp| &($exp:(toExpr (I.TyRef t') e) -> $id:field) |]
+  where getField = [cexp| ($exp:(toExpr  t' e) -> $id:field) |]
+----------------------------------------
+toExpr t (I.ExpIndex at a ti i) = case t of
+  I.TyRef (I.TyArr _ _)       -> expIdx I.TyRef
+  I.TyRef (I.TyCArray _)      -> expIdx I.TyRef
+  I.TyConstRef (I.TyArr _ _)  -> expIdx I.TyConstRef
+  I.TyConstRef (I.TyCArray _) -> expIdx I.TyConstRef
+  _                           ->
+    [cexp| &($exp:(toExpr (I.TyRef at) a) [$exp:(toExpr ti i)]) |]
+  where
+  expIdx constr =
+    [cexp| ($exp:(toExpr (constr at) a) [$exp:(toExpr ti i)]) |]
+----------------------------------------
+toExpr tTo (I.ExpSafeCast tFrom e) =
+  [cexp| ($ty:(toType tTo))$exp:(toExpr tFrom e) |]
+----------------------------------------
+toExpr tTo (I.ExpToIx e maxSz) =
+  [cexp| $exp:(toExpr tTo e ) % $exp:maxSz |]
+----------------------------------------
+toExpr tTo (I.ExpAddrOfGlobal sym) = case tTo of
+  I.TyRef (I.TyArr _ _)       -> [cexp| $id:sym |]
+  I.TyRef (I.TyCArray _)      -> [cexp| $id:sym |]
+  I.TyConstRef (I.TyArr _ _)  -> [cexp| $id:sym |]
+  I.TyConstRef (I.TyCArray _) -> [cexp| $id:sym |]
+  _                           -> [cexp| & $id:sym |]
+----------------------------------------
+toExpr ty (I.ExpMaxMin b) = [cexp| $id:macro |]
+  where
+  macro = case b of
+    True  -> case ty of
+      I.TyInt sz -> case sz of
+        I.Int8     -> "INT8_MAX"
+        I.Int16    -> "INT16_MAX"
+        I.Int32    -> "INT32_MAX"
+        I.Int64    -> "INT64_MAX"
+      I.TyWord sz -> case sz of
+        I.Word8     -> "UINT8_MAX"
+        I.Word16    -> "UINT16_MAX"
+        I.Word32    -> "UINT32_MAX"
+        I.Word64    -> "UINT64_MAX"
+      _           -> err
+    False -> case ty of
+      I.TyInt sz -> case sz of
+        I.Int8     -> "INT8_MIN"
+        I.Int16    -> "INT16_MIN"
+        I.Int32    -> "INT32_MIN"
+        I.Int64    -> "INT64_MIN"
+      _          -> err
+  err = error $ "unexpected type " ++ show ty ++ " in ExpMaxMin."
+----------------------------------------
+
+
+exp0 :: [C.Exp] -> C.Exp
+exp0 = flip (!!) 0
+
+exp1 :: [C.Exp] -> C.Exp
+exp1 = flip (!!) 1
+
+exp2 :: [C.Exp] -> C.Exp
+exp2 = flip (!!) 2
+
+mkArgs :: I.Type -> [I.Expr] -> [C.Exp]
+mkArgs ty = map (toExpr ty)
+
+toExpOp :: I.Type -> I.ExpOp -> [I.Expr] -> C.Exp
+toExpOp ty op args = case op of
+  -- eq instance
+  I.ExpEq ety  -> let xs = mkArgs ety args in
+                  [cexp| $exp:(exp0 xs) == $exp:(exp1 xs) |]
+  I.ExpNeq ety -> let xs = mkArgs ety args in
+                  [cexp| $exp:(exp0 xs) != $exp:(exp1 xs) |]
+  -- conditional expressions
+  I.ExpCond    -> let b  = toExpr I.TyBool (head args) in
+                  let xs = mkArgs ty (tail args) in
+                  [cexp| $exp:b ? $exp:(exp0 xs) : $exp:(exp1 xs) |]
+  -- ord instance
+  I.ExpGt orEq ety
+    | orEq      -> let xs = mkArgs ety args in
+                   [cexp| $exp:(exp0 xs) >= $exp:(exp1 xs) |]
+    | otherwise -> let xs = mkArgs ety args in
+                   [cexp| $exp:(exp0 xs) > $exp:(exp1 xs) |]
+  I.ExpLt orEq ety
+    | orEq      -> let xs = mkArgs ety args in
+                   [cexp| $exp:(exp0 xs) <= $exp:(exp1 xs) |]
+    | otherwise -> let xs = mkArgs ety args in
+                   [cexp| $exp:(exp0 xs) < $exp:(exp1 xs) |]
+  -- boolean operations
+  I.ExpNot      -> let xs = mkArgs ty args in
+                   [cexp| !($exp:(exp0 xs)) |]
+  I.ExpAnd      -> let xs = mkArgs ty args in
+                   [cexp| $exp:(exp0 xs) && $exp:(exp1 xs) |]
+  I.ExpOr       -> let xs = mkArgs ty args in
+                   [cexp| $exp:(exp0 xs) || $exp:(exp1 xs) |]
+  -- num instance
+  I.ExpMul      -> let xs = mkArgs ty args in
+                   [cexp| $exp:(exp0 xs) * $exp:(exp1 xs) |]
+  I.ExpAdd      -> let xs = mkArgs ty args in
+                   [cexp| $exp:(exp0 xs) + $exp:(exp1 xs) |]
+  I.ExpSub      -> let xs = mkArgs ty args in
+                   [cexp| $exp:(exp0 xs) - $exp:(exp1 xs) |]
+  I.ExpNegate   -> let xs = mkArgs ty args in
+                   [cexp| - ($exp:(exp0 xs)) |]
+  I.ExpAbs      -> let xs = mkArgs ty args in
+                   [cexp| $id:(absSym ty)($exp:(exp0 xs)) |]
+  I.ExpSignum   -> let xs = mkArgs ty args in
+                   [cexp| $id:(signumSym ty)($exp:(exp0 xs)) |]
+
+  -- integral/fractional instance
+  I.ExpDiv      -> let xs = mkArgs ty args in
+                   [cexp| $exp:(exp0 xs) / $exp:(exp1 xs) |]
+  I.ExpMod      -> toMod ty args
+  I.ExpRecip    -> let xs = mkArgs ty args in
+                   [cexp| 1 / $exp:(exp0 xs) |]
+
+  -- floating instance
+  I.ExpFExp       -> floatingUnary ty "exp"  args
+  I.ExpFSqrt      -> floatingUnary ty "sqrt" args
+  I.ExpFLog       -> floatingUnary ty "log"  args
+  I.ExpFPow       -> floatingBinary ty "pow" args
+  I.ExpFLogBase   -> toLogBase ty args
+  I.ExpFSin       -> floatingUnary ty "sin"   args
+  I.ExpFCos       -> floatingUnary ty "cos"   args
+  I.ExpFTan       -> floatingUnary ty "tan"   args
+  I.ExpFAsin      -> floatingUnary ty "asin"  args
+  I.ExpFAcos      -> floatingUnary ty "acos"  args
+  I.ExpFAtan      -> floatingUnary ty "atan"  args
+  I.ExpFSinh      -> floatingUnary ty "sinh"  args
+  I.ExpFCosh      -> floatingUnary ty "cosh"  args
+  I.ExpFTanh      -> floatingUnary ty "tanh"  args
+  I.ExpFAsinh     -> floatingUnary ty "asinh" args
+  I.ExpFAcosh     -> floatingUnary ty "acosh" args
+  I.ExpFAtanh     -> floatingUnary ty "atanh" args
+
+  -- float operations
+  -- XXX this needs to add a dependency on <math.h>
+  I.ExpIsNan ety -> let xs = mkArgs ety args in
+                    [cexp| ($ty:(toType I.TyBool)) (isnan($exp:(exp0 xs))) |]
+  -- isinf returns -1 for negative infinity and 1 for positive infinity.
+  I.ExpIsInf ety -> let xs = mkArgs ety args in
+                    [cexp| ($ty:(toType I.TyBool)) (isinf($exp:(exp0 xs))) |]
+  I.ExpRoundF    -> floatingBinary ty "round" args
+  I.ExpCeilF     -> floatingBinary ty "ceil" args
+  I.ExpFloorF    -> floatingBinary ty "floor" args
+
+  -- float casting
+  I.ExpToFloat ety   -> let xs = mkArgs ety args in
+                        [cexp| ($ty:(toType ty))($exp:(exp0 xs)) |]
+  I.ExpFromFloat ety ->
+    [cexp| ($ty:(toType ty))($exp:(floatingUnary ety "trunc" args)) |]
+
+  -- bit operations
+  I.ExpBitAnd        -> let xs = mkArgs ty args in
+                        [cexp| $exp:(exp0 xs) & $exp:(exp1 xs) |]
+  I.ExpBitOr         -> let xs = mkArgs ty args in
+                        [cexp| $exp:(exp0 xs) | $exp:(exp1 xs) |]
+  I.ExpBitXor        -> let xs = mkArgs ty args in
+                        [cexp| $exp:(exp0 xs) ^ $exp:(exp1 xs) |]
+  I.ExpBitComplement -> let xs = mkArgs ty args in
+                        [cexp| ~($exp:(exp0 xs)) |]
+  I.ExpBitShiftL     -> let xs = mkArgs ty args in
+                        [cexp| $exp:(exp0 xs) << $exp:(exp1 xs) |]
+  I.ExpBitShiftR     -> let xs = mkArgs ty args in
+                        [cexp| $exp:(exp0 xs) >> $exp:(exp1 xs) |]
+
+floatingSym :: I.Type -> String ->  String
+floatingSym t sym = case t of
+  I.TyFloat -> sym ++ "f"
+  I.TyDouble -> sym
+  _ -> error "Can't make floatingSym out of non-float"
+
+floatingBinary :: I.Type -> String -> [I.Expr] -> C.Exp
+floatingBinary ty name args =
+  let xs = mkArgs ty args in
+  [cexp| $id:(floatingSym ty name)($exp:(exp0 xs), $exp:(exp1 xs)) |]
+
+floatingUnary :: I.Type -> String -> [I.Expr] -> C.Exp
+floatingUnary ty name args =
+  let xs = mkArgs ty args in
+  [cexp| $id:(floatingSym ty name)($exp:(exp0 xs)) |]
+
+toLogBase :: I.Type -> [I.Expr] -> C.Exp
+toLogBase ty args = [cexp| $exp:(logC $ exp0 xs) / $exp:(logC $ exp1 xs) |]
+  where
+  xs = mkArgs ty args
+  logC e = [cexp| $id:(floatingSym ty "log")($exp:e) |]
+
+-- XXX Not sure aobut this, as there's currently no way to perform mod on
+-- float/double in the frontend.
+toMod :: I.Type -> [I.Expr] -> C.Exp
+toMod ty args = case ty of
+  I.TyFloat  -> [cexp| fmodf($exp:x', $exp:y') |]
+  I.TyDouble -> [cexp| fmod ($exp:x', $exp:y') |]
+  _          -> [cexp| $exp:x' % $exp:y' |]
+  where
+  args' = mkArgs ty args
+  x' = exp0 args'
+  y' = exp1 args'
+
+-- | Emit the function name for a call to abs.  This doesn't include any symbol
+-- for unsigned things, as they should be optimized out by the front end.
+absSym :: I.Type -> String
+absSym ty = case ty of
+  I.TyFloat  -> "fabsf"
+  I.TyDouble -> "fabs"
+  I.TyInt i  -> "abs_i" ++ iType i
+  I.TyChar   -> "abs_char"
+  _          -> error ("abs " ++ "unimplemented for type " ++ show ty)
+  where
+  iType i = case i of
+    I.Int8  -> "8"
+    I.Int16 -> "16"
+    I.Int32 -> "32"
+    I.Int64 -> "64"
+
+-- | Emit the function name for a call to signum.
+signumSym :: I.Type -> String
+signumSym ty = case ty of
+  I.TyFloat  -> "signum_float"
+  I.TyDouble -> "signum_double"
+  I.TyInt i  -> "signum_i" ++ showInt i
+  I.TyWord w -> "signum_w" ++ showWord w
+  I.TyChar   -> "signum_char"
+  _          -> error ("signum " ++ "unimplemented for type " ++ show ty)
+----------------------------------------
+
+showInt :: I.IntSize -> String
+showInt I.Int8  = show (8 :: Int)
+showInt I.Int16 = show (16 :: Int)
+showInt I.Int32 = show (32 :: Int)
+showInt I.Int64 = show (64 :: Int)
+
+showWord :: I.WordSize -> String
+showWord I.Word8  = show (8 :: Int)
+showWord I.Word16 = show (16 :: Int)
+showWord I.Word32 = show (16 :: Int)
+showWord I.Word64 = show (32 :: Int)
+
+--------------------------------------------------------------------------------
+
+toRequire :: I.Cond -> C.BlockItem
+toRequire = toAssertion id "REQUIRES"
+
+-- | Takes the return expression, the condition, and returns a 'BlockItem'.
+toEnsure :: I.Expr -> I.Cond -> C.BlockItem
+toEnsure retE = toAssertion (ensTrans retE) "ENSURES"
+
+toAssertion :: (I.Expr -> I.Expr) -> String -> I.Cond -> C.BlockItem
+toAssertion trans call cond = C.BlockStm $
+  case cond of
+    I.CondBool e          ->
+      [cstm| $id:call($exp:(toExpr I.TyBool (trans e))); |]
+    I.CondDeref t e var c ->
+      let res = (toBody []) (I.Deref t var (trans e)) in
+      let c1  = toAssertion trans call c in
+      [cstm| { $items:res $item:c1 } |]
+
+--------------------------------------------------------------------------------
diff --git a/src/Ivory/Compile/C/Modules.hs b/src/Ivory/Compile/C/Modules.hs
new file mode 100644
--- /dev/null
+++ b/src/Ivory/Compile/C/Modules.hs
@@ -0,0 +1,182 @@
+{-# LANGUAGE QuasiQuotes #-}
+
+module Ivory.Compile.C.Modules where
+
+import Paths_ivory_backend_c (version)
+
+import qualified Text.PrettyPrint.Mainland as PP
+import Text.PrettyPrint.Mainland
+
+import qualified Ivory.Language.Syntax.AST as I
+
+import Ivory.Compile.C.Gen
+import Ivory.Compile.C.Types
+
+import Data.Char (toUpper)
+import Data.Version (showVersion)
+import Control.Applicative ((<$>))
+import qualified Data.Set as S
+import Control.Monad
+import System.FilePath.Posix ((<.>)) -- Always use posix convention in C code
+import MonadLib (put,runM)
+
+--------------------------------------------------------------------------------
+
+showModule :: CompileUnits -> [[String]]
+showModule m =
+  [ mk "// Sources:\n" (sources m)
+  , mk "// Header:\n"  (headers m)
+  , mk "// Externs:\n" (S.empty, externs m)
+  ]
+  where
+  mk _   (_,[])         = []
+  mk str (incls,units)  = str : pp (map includeDef (S.toList incls) ++ units)
+  pp = map (show . ppr)
+
+--------------------------------------------------------------------------------
+
+compilerVersion :: String
+compilerVersion = showVersion version
+
+---
+topComments :: Doc
+topComments  = text "/* This file has been autogenerated by Ivory" </>
+               text " * Compiler version " <+> text compilerVersion </>
+               text " */"
+
+-- | Output header file for a module.
+writeHdr :: Bool                -- ^ Verbosity
+         -> FilePath            -- ^ Output file name
+         -> (Includes, Sources) -- ^ Source to translate
+         -> String              -- ^ Unit name
+         -> IO ()
+writeHdr True  f s unitname = toFile f $ renderHdr s unitname
+writeHdr False f s unitname = toFileQuiet f $ renderHdr s unitname
+
+renderHdr :: (Includes, Sources) -> String -> String
+renderHdr s unitname = PP.displayS (PP.render width guardedHeader) ""
+  where
+  width = 80
+  guardedHeader = stack [ topComments
+                        , topGuard
+                        , topExternC
+                        , ppr (defs s)
+                        , botExternC
+                        , botGuard
+                        ]
+  topGuard        = text "#ifndef" <+> guardName PP.</> text "#define"
+                      <+> guardName
+  botGuard        = text "#endif" <+> text "/*" <+> guardName <+> text "*/"
+  unitname'       = map (\c -> if c == '-' then '_' else c) unitname
+  guardName       = text "__" <> text (toUpper <$> unitname') <> text "_H__"
+  topExternC      = stack $ text <$> [ "#ifdef __cplusplus"
+                                     , "extern \"C\" {"
+                                     , "#endif"]
+  botExternC      = stack $ text <$> [ "#ifdef __cplusplus"
+                                     , "}"
+                                     , "#endif"]
+  defs (incls,us) = map includeDef (S.toList incls) ++ us
+
+
+-- | Output source file for a module.
+writeSrc :: Bool                 -- ^ Be verbose
+         -> FilePath             -- ^ Output source name
+         -> (Includes, Sources)  -- ^ Module to translate
+         -> IO ()
+writeSrc verbose f s = vToFile f (renderSrc s)
+  where
+  vToFile = if verbose then toFile else toFileQuiet
+
+renderSrc :: (Includes, Sources) -> String
+renderSrc s = PP.displayS (PP.render width srcdoc) ""
+  where
+  width = 80
+  srcdoc = topComments </> out
+  defs (incls,us) = map includeDef (S.toList incls) ++ us
+  out = stack $ punctuate line $ map ppr $ defs s
+
+-- Utility
+toFileQuiet :: FilePath -> String -> IO ()
+toFileQuiet f v = writeFile f v
+
+toFile :: FilePath -> String -> IO ()
+toFile f v = do
+  putStr $ "Writing to file " ++ f ++ "..."
+  toFileQuiet f v
+  putStrLn " Done."
+
+--------------------------------------------------------------------------------
+
+runOpt :: (I.Proc -> I.Proc) -> I.Module -> I.Module
+runOpt opt m =
+  m { I.modProcs = procs' }
+  where
+  procs' = procs { I.public = map' I.public, I.private = map' I.private }
+  procs = I.modProcs m
+  map' acc = map opt (acc procs)
+
+--------------------------------------------------------------------------------
+
+-- | Compile a module.
+compileModule :: I.Module -> CompileUnits
+compileModule I.Module { I.modName        = nm
+                       , I.modDepends     = deps
+                       , I.modHeaders     = hdrs
+                       , I.modExterns     = exts
+                       , I.modImports     = imports
+                       , I.modProcs       = procs
+                       , I.modStructs     = structs
+                       , I.modAreas       = areas
+                       , I.modAreaImports = ais
+                       }
+  = CompileUnits
+  { unitName = nm
+  , sources  = sources res
+  , headers  = headers res
+  , externs  = externs res
+  }
+  where
+  res     = compRes comp
+  compRes = (snd . runM . unCompile)
+
+  unitHdr = LocalInclude (nm <.> "h")
+
+  comp = do
+    let c = compRes comp0
+    unless (null (snd (headers c))) (putSrcInc unitHdr)
+    Compile (put c)
+
+  comp0 :: Compile
+  comp0 = do
+    putHdrInc (LocalInclude "ivory.h")
+    -- module names don't have a .h on the end
+    mapM_ (putHdrInc . LocalInclude . ((<.> "h"))) (S.toList deps)
+    mapM_ (putHdrInc . SysInclude)   (S.toList hdrs)
+    mapM_ (compileStruct Public) (I.public structs)
+    mapM_ (compileStruct Private) (I.private structs)
+    mapM_ compileExtern exts
+    mapM_ fromImport imports
+    mapM_ (extractAreaProto Public) (I.public areas)
+    mapM_ (extractAreaProto Private) (I.private areas)
+    mapM_ (compileArea Public) (I.public areas)
+    mapM_ (compileArea Private) (I.private areas)
+    mapM_ compileAreaImport ais
+    mapM_ (extractProto Public) (I.public procs)
+    mapM_ (extractProto Private) (I.private procs)
+    mapM_ compileUnit (I.public procs ++ I.private procs)
+
+--------------------------------------------------------------------------------
+
+fromImport :: I.Import -> Compile
+fromImport p = putSrcInc (SysInclude (I.importFile p))
+
+--------------------------------------------------------------------------------
+
+outputProcSyms :: [I.Module] -> IO ()
+outputProcSyms mods = putStrLn $ unwords $ concatMap go mods
+  where
+  go :: I.Module -> [String]
+  go m = map I.procSym (pub ++ priv)
+    where I.Visible pub priv = I.modProcs m
+
+--------------------------------------------------------------------------------
diff --git a/src/Ivory/Compile/C/Prop.hs b/src/Ivory/Compile/C/Prop.hs
new file mode 100644
--- /dev/null
+++ b/src/Ivory/Compile/C/Prop.hs
@@ -0,0 +1,25 @@
+-- | Rewrite ensures variable with return expression.
+
+module Ivory.Compile.C.Prop where
+
+import qualified Ivory.Language.Syntax as I
+
+--------------------------------------------------------------------------------
+
+-- | Replace ensures variable with the return expression.
+ensTrans :: I.Expr -> I.Expr -> I.Expr
+ensTrans retE = loop
+  where
+  loop e = case e of
+    I.ExpSym{}             -> e
+    I.ExpVar v             -> if v == I.retval then retE else e
+    I.ExpLit{}             -> e
+    I.ExpOp op args        -> I.ExpOp op (map loop args)
+    I.ExpLabel t e0 s      -> I.ExpLabel t (loop e0) s
+    I.ExpIndex t e0 t1 e1  -> I.ExpIndex t (loop e0) t1 (loop e1)
+    I.ExpSafeCast t e0     -> I.ExpSafeCast t (loop e0)
+    I.ExpToIx e0 maxSz     -> I.ExpToIx (loop e0) maxSz
+    I.ExpAddrOfGlobal{}    -> e
+    I.ExpMaxMin{}          -> e
+
+--------------------------------------------------------------------------------
diff --git a/src/Ivory/Compile/C/SourceDeps.hs b/src/Ivory/Compile/C/SourceDeps.hs
new file mode 100644
--- /dev/null
+++ b/src/Ivory/Compile/C/SourceDeps.hs
@@ -0,0 +1,45 @@
+
+module Ivory.Compile.C.SourceDeps where
+
+import Control.Monad
+import System.FilePath
+import System.Directory
+
+import Data.Either
+import qualified Data.Set as Set
+
+import Ivory.Language
+import qualified Ivory.Language.Syntax.AST as AST
+
+-- At some point we may want to restrict this to .c and .h files only
+-- but for now we'll leave it alone.
+collectSourceDeps :: [Module] -> [FilePath]
+collectSourceDeps ms = Set.toList $ foldl aux Set.empty ms
+  where aux acc m = Set.union acc (AST.modSourceDeps m)
+
+outputSourceDeps :: FilePath -> FilePath -- Output dirs: include dir, source dir
+                 -> [FilePath]           -- SourceDeps: list if filenames to output
+                 -> [FilePath]           -- Search Path: list of directories
+                 -> IO ()                --  where SourceDeps may be
+outputSourceDeps inclDir srcDir srcDeps searchPath = do
+    validSearchPath <- filterM doesDirectoryExist searchPath
+    discovered <- mapM (findSource validSearchPath) srcDeps
+    mapM_ output (rights discovered)
+    case lefts discovered of
+      [] -> return ()
+      es -> error $ "failure to output source dependencies:\n" ++ (unlines es) ++
+                    "in search path:\n" ++ (unlines searchPath)
+  where
+  findSource :: [FilePath] -> FilePath -> IO (Either String FilePath)
+  findSource searchpath f = do
+    v <- filterM doesFileExist $ map (\p -> p </> f) searchpath
+    case v of
+      []   -> return $ Left ("not found: " ++ f)
+      a:_ -> return $ Right a
+  output :: FilePath -> IO ()
+  output fp = case takeExtension fp of
+    ".h" -> copyFile fp (inclDir </> (takeFileName fp))
+    _    -> copyFile fp (srcDir  </> (takeFileName fp))
+
+
+
diff --git a/src/Ivory/Compile/C/Types.hs b/src/Ivory/Compile/C/Types.hs
new file mode 100644
--- /dev/null
+++ b/src/Ivory/Compile/C/Types.hs
@@ -0,0 +1,69 @@
+{-# LANGUAGE PackageImports #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE QuasiQuotes #-}
+
+module Ivory.Compile.C.Types where
+
+import Language.C.Quote.GCC
+import qualified "language-c-quote" Language.C.Syntax as C
+
+import MonadLib (WriterT,Id,put)
+import Data.Monoid
+import qualified Data.Set as S
+
+--------------------------------------------------------------------------------
+
+data Include
+  = SysInclude   FilePath -- ^ @#include <foo.h>@
+  | LocalInclude FilePath -- ^ @#include "foo.h"@
+    deriving (Show,Eq,Ord)
+
+includeDef :: Include -> C.Definition
+includeDef incl = case incl of
+  SysInclude file   -> [cedecl| $esc:("#include <"  ++ file ++ ">")           |]
+  LocalInclude file -> [cedecl| $esc:("#include \"" ++ file ++ "\"")          |]
+
+type Includes = S.Set Include
+type Sources  = [C.Definition]
+
+data CompileUnits = CompileUnits
+  { unitName :: String
+  , sources  :: (Includes, Sources)
+  , headers  :: (Includes, Sources)
+  , externs  :: Sources
+  } deriving Show
+
+instance Monoid CompileUnits where
+  mempty = CompileUnits mempty mempty mempty mempty
+  (CompileUnits n0 s0 h0 e0) `mappend` (CompileUnits n1 s1 h1 e1) =
+    CompileUnits (n0 `mappend` n1)
+                 (s0 `mappend` s1)
+                 (h0 `mappend` h1)
+                 (e0 `mappend` e1)
+
+--------------------------------------------------------------------------------
+
+newtype CompileM a = Compile
+  { unCompile :: WriterT CompileUnits Id a }
+  deriving (Functor, Monad)
+
+type Compile = CompileM ()
+
+--------------------------------------------------------------------------------
+
+putSrc :: C.Definition -> Compile
+putSrc def = Compile (put mempty { sources = (S.empty,[def]) })
+
+putSrcInc :: Include -> Compile
+putSrcInc inc = Compile (put mempty { sources = (S.fromList [inc],[]) })
+
+putHdrSrc :: C.Definition -> Compile
+putHdrSrc hdr = Compile (put mempty { headers = (S.empty,[hdr]) })
+
+putHdrInc :: Include -> Compile
+putHdrInc inc = Compile (put mempty { headers = (S.fromList [inc],[]) })
+
+putExt :: C.Definition -> Compile
+putExt ext = Compile (put mempty { externs = [ext] })
+
+--------------------------------------------------------------------------------