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/examples/AddrOfRegression.hs b/examples/AddrOfRegression.hs
new file mode 100644
--- /dev/null
+++ b/examples/AddrOfRegression.hs
@@ -0,0 +1,86 @@
+{-# OPTIONS_GHC  -fno-warn-orphans #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module AddrOfRegression where
+
+import Ivory.Language
+
+[ivory|
+struct param_info
+  { param_requested :: Stored Uint8
+  ; other           :: Stored Uint16
+  }
+|]
+
+test1 :: ModuleDef
+test1 = do
+  defMemArea param_info_area
+  incl t1
+  where
+  param_info_area :: MemArea (Array 512 (Struct "param_info"))
+  param_info_area = area "g_param_info" Nothing
+
+  param_info_ref :: Ref Global (Array 512 (Struct "param_info"))
+  param_info_ref = addrOf param_info_area
+
+  t1 :: Def ('[]:->())
+  t1 = proc "t1" $ body $ do
+    arrayMap $ \ix ->
+      store ((param_info_ref ! ix) ~> param_requested) 1
+
+test1_noarray :: ModuleDef
+test1_noarray = do
+  defMemArea param_info_area
+  incl t1
+  where
+  param_info_area :: MemArea (Struct "param_info")
+  param_info_area = area "single_param_info" Nothing
+
+  param_info_ref :: Ref Global (Struct "param_info")
+  param_info_ref = addrOf param_info_area
+
+  t1 :: Def ('[]:->())
+  t1 = proc "t1_noarray" $ body $ do
+    store (param_info_ref ~> param_requested) 1
+
+test2 :: ModuleDef
+test2 = do
+  defMemArea atom_array_area
+  incl t2
+  where
+  atom_array_area :: MemArea (Array 512 (Stored IFloat))
+  atom_array_area = area "atom_array" Nothing
+
+  atom_array_ref :: Ref Global (Array 512 (Stored IFloat))
+  atom_array_ref = addrOf atom_array_area
+
+  t2 :: Def ('[]:->())
+  t2 = proc "t2" $ body $ do
+    arrayMap $ \ix ->
+      store (atom_array_ref ! ix) 1
+
+test3 :: ModuleDef
+test3 = do
+  incl t3
+  where
+  t3 :: Def ('[]:->())
+  t3 = proc "t3" $ body $ do
+    (stack_array :: Ref (Stack s) (Array 512 (Stored IFloat))) <- local izero
+    arrayMap $ \ix ->
+      store (stack_array ! ix) 1
+
+
+cmodule :: Module
+cmodule = package "AddrOfRegression" $ do
+  defStruct (Proxy :: Proxy "param_info")
+  test1
+  test1_noarray
+  test2
+  test3
+
+
+
diff --git a/examples/Area.hs b/examples/Area.hs
new file mode 100644
--- /dev/null
+++ b/examples/Area.hs
@@ -0,0 +1,41 @@
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE QuasiQuotes #-}
+
+module Area where
+
+import Ivory.Language
+
+
+[ivory|
+
+struct val {
+  field :: Stored Uint32
+}
+
+|]
+
+val :: MemArea (Struct "val")
+val  = area "val" (Just (istruct [field .= ival 0]))
+
+cval :: ConstMemArea (Struct "val")
+cval  = constArea "cval" (istruct [field .= ival 10])
+
+getVal :: Def ('[] :-> Uint32)
+getVal = proc "getVal" $ body $ do
+  ret =<< deref (addrOf val ~> field)
+
+setVal :: Def ('[Uint32] :-> ())
+setVal = proc "setVal" $ \ n -> body $ do
+  store (addrOf val ~> field) n
+  retVoid
+
+cmodule :: Module
+cmodule = package "Area" $ do
+  incl getVal
+  incl setVal
+  defMemArea val
+  defConstMemArea cval
+  defStruct (Proxy :: Proxy "val")
diff --git a/examples/Bits.hs b/examples/Bits.hs
new file mode 100644
--- /dev/null
+++ b/examples/Bits.hs
@@ -0,0 +1,78 @@
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE DataKinds #-}
+
+module Bits (runBits, cmodule) where
+
+import Ivory.Compile.C.CmdlineFrontend
+import Ivory.Language
+import MonadLib.Monads (runState, sets)
+
+runBits :: IO ()
+runBits = runCompiler [cmodule] initialOpts {stdOut = True}
+
+cmodule :: Module
+cmodule = package "Bits" $ do
+  incl test1
+  incl test2
+  incl test3
+  incl test4
+
+test1 :: Def ('[Uint8, Uint16, Uint32, Uint64] :-> Uint64)
+test1 = proc "test1" $ \u8 u16 u32 u64 -> body $ do
+  a <- assign $ u8  .& 0xFF
+  b <- assign $ u16 .& 0xFF00
+  c <- assign $ u32 .& 0xFF0000
+  d <- assign $ u64 .& 0xFF000000
+  ret $ (safeCast a) .| (safeCast b) .| (safeCast c) .| d
+
+-- | Convert an array of four 8-bit integers into a 32-bit integer.
+test2 :: Def ('[Ref s (Array 4 (Stored Uint8))] :-> Uint32)
+test2 = proc "test2" $ \arr -> body $ do
+  a <- deref (arr ! 0)
+  b <- deref (arr ! 1)
+  c <- deref (arr ! 2)
+  d <- deref (arr ! 3)
+  ret $ ((safeCast a) `iShiftL` 24) .|
+        ((safeCast b) `iShiftL` 16) .|
+        ((safeCast c) `iShiftL` 8)  .|
+        ((safeCast d) `iShiftL` 0)
+
+-- | Example of using "extractByte" with a state monad.
+extractUint32 :: Uint32 -> (Uint8, Uint8, Uint8, Uint8)
+extractUint32 x = fst $ runState x $ do
+  a <- sets extractByte
+  b <- sets extractByte
+  c <- sets extractByte
+  d <- sets extractByte
+  return (a, b, c, d)
+
+-- | Convert a 32-bit integer to an array of 8-bit integers.
+test3 :: Def ('[Uint32, Ref s (Array 4 (Stored Uint8))] :-> ())
+test3 = proc "test3" $ \n arr -> body $ do
+  let (a, b, c, d) = extractUint32 n
+  store (arr ! 0) d
+  store (arr ! 1) c
+  store (arr ! 2) b
+  store (arr ! 3) a
+
+setBit :: (IvoryBits a, IvoryStore a)
+       => (Ref s (Stored a)) -> Int -> Ivory eff ()
+setBit ref bit = do
+  val <- deref ref
+  store ref (val .| (1 `iShiftL` (fromIntegral bit)))
+
+clearBit :: (IvoryBits a, IvoryStore a)
+         => (Ref s (Stored a)) -> Int -> Ivory eff ()
+clearBit ref bit = do
+  val <- deref ref
+  store ref (val .& (iComplement (1 `iShiftL` (fromIntegral bit))))
+
+test4 :: Def ('[] :-> Uint32)
+test4 = proc "test4" $ body $ do
+  n <- local (ival 0)
+  setBit n 1
+  setBit n 3
+  setBit n 5
+  setBit n 8
+  clearBit n 3
+  ret =<< deref n
diff --git a/examples/Cond.hs b/examples/Cond.hs
new file mode 100644
--- /dev/null
+++ b/examples/Cond.hs
@@ -0,0 +1,34 @@
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE DataKinds #-}
+
+module Cond where
+
+import Ivory.Language
+import Ivory.Compile.C.CmdlineFrontend
+import Prelude hiding (exp)
+
+add :: Def ('[Uint32,Uint32] :-> Uint32)
+add  = proc "add"
+     $ \ x y -> ensures (\r -> r ==? x + y)
+              $ body
+              $ ret (x + y)
+
+cmodule :: Module
+cmodule = package "cond" $ incl add
+
+-- Testing assertions with choice expression
+
+foo :: Def ('[IFloat,IFloat,IFloat] :-> IFloat)
+foo = proc "foo" $ \x y z -> body $ do
+  let cond  = 2/x ==? 5
+  let tCond = 6/y ==? 7
+  let exp   = tCond ? (8/z, 9)
+  ret (cond ? (exp,4))
+
+fooMod :: Module
+fooMod  = package "fooM" $ incl foo
+
+runFoo :: IO ()
+runFoo = runCompiler [fooMod] initialOpts { stdOut = True
+                                          , divZero = True
+                                          }
diff --git a/examples/Factorial.hs b/examples/Factorial.hs
new file mode 100644
--- /dev/null
+++ b/examples/Factorial.hs
@@ -0,0 +1,25 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Factorial where
+
+import Ivory.Language
+import Ivory.Compile.C.CmdlineFrontend
+
+factorial :: Def ('[Sint32] :-> Sint32)
+factorial  = proc "factorial" $ \ n ->
+  -- These are made up requires/ensures for testing purposes.
+  ensures (\r -> n <? r) $
+  body $
+    ifte_ (n >? 1)
+      (do n' <- call factorial (n - 1)
+          ret (n' * n)
+      )
+      (do ret n
+      )
+
+cmodule :: Module
+cmodule = package "Factorial" $ incl factorial
+
+runFactorial :: IO ()
+runFactorial = runCompiler [cmodule] initialOpts { stdOut = True }
diff --git a/examples/FibLoop.hs b/examples/FibLoop.hs
new file mode 100644
--- /dev/null
+++ b/examples/FibLoop.hs
@@ -0,0 +1,71 @@
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeOperators #-}
+
+module FibLoop where
+
+import Ivory.Compile.C.CmdlineFrontend
+import Ivory.Language
+
+import Control.Applicative ((<$>),(<*>))
+
+-- Recursive implementation of fib
+fib_rec :: Def ('[Uint32] :-> Uint64)
+fib_rec  = proc "fib_rec" (\n -> body (ret =<< call fib_rec_aux 0 1 n))
+
+fib_rec_aux :: Def ('[Uint32,Uint32,Uint32] :-> Uint64)
+fib_rec_aux  = proc "fib_rec_aux" $ \ a b n -> body $ do
+  ifte_ (n ==? 0)
+    (ret (safeCast a))
+    (ret . safeCast =<< call fib_rec_aux b (a + b) (n - 1))
+
+-- Loop implementation of fib.
+
+fib_loop :: Def ('[Ix 1000] :-> Uint32)
+fib_loop  = proc "fib_loop" $ \ n -> body $ do
+  a <- local (ival 0)
+  b <- local (ival 0)
+
+  n `times` \ _ -> do
+    a' <- deref a
+    b' <- deref b
+    store a b'
+    store b (a' + b')
+
+  result <- deref a
+  ret result
+
+-- Loop implementation of fib, using a structure instead
+-- of two discrete variables.
+[ivory|
+struct Fibstate
+  { sa :: Stored Uint32
+  ; sb :: Stored Uint32
+  }
+|]
+
+fib_struct_loop :: Def ('[Ix 1000] :-> Uint32)
+fib_struct_loop  = proc "fib_struct_loop" $ \ n -> body $ do
+  state <- local (istruct [ sa .= ival 0 , sb .= ival 0 ])
+
+  let update = (+) <$> deref (state ~> sa) <*> deref (state ~> sb)
+
+  n `times` \ _ -> do
+    store (state ~> sa) =<< deref (state ~> sb)
+    store (state ~> sb) =<< update
+
+  ret =<< deref (state ~> sa)
+
+cmodule :: Module
+cmodule = package "FibLoop" $ do
+  incl fib_rec
+  incl fib_rec_aux
+  incl fib_loop
+
+  defStruct (Proxy :: Proxy "Fibstate")
+  incl fib_struct_loop
+
+runFibLoop :: IO ()
+runFibLoop  = runCompiler [cmodule] initialOpts { stdOut = True, constFold = True }
diff --git a/examples/FibTutorial.hs b/examples/FibTutorial.hs
new file mode 100644
--- /dev/null
+++ b/examples/FibTutorial.hs
@@ -0,0 +1,26 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeOperators #-}
+
+import Ivory.Language
+import qualified Ivory.Compile.C.CmdlineFrontend as C (compile)
+
+fib_loop :: Def ('[Ix 1000] :-> Uint32)
+fib_loop  = proc "fib_loop" $ \ n -> body $ do
+  a <- local (ival 0)
+  b <- local (ival 1)
+
+  n `times` \ _ -> do
+    a' <- deref a
+    b' <- deref b
+    store a b'
+    store b (a' + b')
+
+  result <- deref a
+  ret result
+
+fib_tutorial_module :: Module
+fib_tutorial_module = package "fib_tutorial" $ do
+  incl fib_loop
+
+main :: IO ()
+main = C.compile [ fib_tutorial_module ]
diff --git a/examples/Float.hs b/examples/Float.hs
new file mode 100644
--- /dev/null
+++ b/examples/Float.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE DataKinds #-}
+
+module Float (runFloat,cmodule) where
+
+import Ivory.Compile.C.CmdlineFrontend
+import Ivory.Language
+
+runFloat :: IO ()
+runFloat = runCompiler [cmodule] initialOpts { stdOut = True }
+
+cmodule :: Module
+cmodule  = package "Float" $ do
+  incl test1
+  incl test2
+
+test1 :: Def ('[IFloat] :-> Sint32)
+test1  = proc "test1" (\ f -> body (ret (castDefault f)))
+
+test2 :: Def ('[Sint32] :-> IFloat)
+test2  = proc "test2" (\ i -> body (ret (safeCast i)))
diff --git a/examples/Forever.hs b/examples/Forever.hs
new file mode 100644
--- /dev/null
+++ b/examples/Forever.hs
@@ -0,0 +1,37 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Forever where
+
+import Ivory.Language
+import Ivory.Compile.C.CmdlineFrontend
+
+factorial :: Def ('[Sint32] :-> Sint32)
+factorial  = proc "factorial" $ \ n ->
+  -- These are made up requires/ensures for testing purposes.
+  ensures (\r -> n <? r) $ body $ do
+  ifte_ (n >? 1)
+    (do n' <- call factorial (n - 1)
+        ret (n' * n)
+    )
+    (do ret n
+    )
+
+printResult :: Def ('[Sint32] :-> ())
+printResult = proc "print_result" $ \_ -> body retVoid
+
+foreverFactorial :: Def ('[Sint32] :-> ())
+foreverFactorial = proc "forever_factorial" $ \ n -> body $ do
+  forever $ do
+    res <- call factorial n
+    call_ printResult res
+
+cmodule :: Module
+cmodule = package "Forever" $ do
+  incl factorial
+  incl printResult
+  incl foreverFactorial
+
+runFactorial :: IO ()
+runFactorial = runCompiler [cmodule] initialOpts { stdOut = True }
+
diff --git a/examples/FunPtr.hs b/examples/FunPtr.hs
new file mode 100644
--- /dev/null
+++ b/examples/FunPtr.hs
@@ -0,0 +1,25 @@
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE DataKinds #-}
+
+module FunPtr where
+
+import Ivory.Compile.C.CmdlineFrontend
+import Ivory.Language
+
+f :: Def ('[Sint32] :-> Sint32)
+f  = proc "f" (\ n -> body (ret (n + 1)))
+
+invoke :: Def ('[ ProcPtr ('[Sint32] :-> Sint32), Sint32] :-> Sint32)
+invoke  = proc "invoke" (\ k n -> body (ret =<< indirect k n))
+
+test :: Def ('[] :-> Sint32)
+test  = proc "test" (body (ret =<< call invoke (procPtr f) 10))
+
+runFunPtr :: IO ()
+runFunPtr = runCompiler [cmodule] initialOpts { stdOut = True }
+
+cmodule :: Module
+cmodule = package "FunPtr" $ do
+  incl f
+  incl test
+  incl invoke
diff --git a/examples/PID.hs b/examples/PID.hs
new file mode 100644
--- /dev/null
+++ b/examples/PID.hs
@@ -0,0 +1,82 @@
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE FlexibleInstances #-}
+
+module PID where
+
+import Ivory.Compile.C.CmdlineFrontend
+import Ivory.Language
+
+[ivory|
+
+struct PID
+  { pid_mv  :: Stored IFloat
+  ; pid_i   :: Stored IFloat
+  ; pid_err :: Stored IFloat
+  }
+
+|]
+
+type SP   = IFloat -- Set point
+type PV   = IFloat -- Process (measured) value
+type Time = IFloat
+
+{-
+void pid_update(struct PID * pid,
+                sp_t sp,
+                pv_t pv,
+                timeinc_t dt
+                )
+{
+  float err = sp - pv;
+  float i   = pid->i + err*dt;
+  float d   = (err - pid->err) / dt;
+  pid->i    = ki*i;
+  pid->mv   = kp*err + pid->i + kd*d;
+  pid->err  = err;
+  return;
+}
+-}
+
+kp, ki, kd :: IFloat
+kp = 1.0
+ki = 0.1
+kd = 0.1
+
+pidUpdate :: Def ('[ Ref s (Struct "PID")
+                   , SP
+                   , PV
+                   , Time ]
+                  :-> IFloat)
+pidUpdate = proc "pid_update" $
+  \ pid sp pv dt ->
+  -- These are made up requires/ensures for testing purposes.
+    requires (checkStored (pid ~> pid_err) (\err -> err <? 1))
+  $ ensures  (\res -> checkStored (pid ~> pid_err) (\err -> err <? res))
+  $ body
+  $ do
+    err     <- assign (sp - pv)
+    i       <- deref $ pid ~> pid_i
+    i'      <- assign  $ ki * (i + err*dt)
+    prevErr <- deref $ pid ~> pid_err
+    d       <- assign  $ (err - prevErr) / dt
+    store (pid ~> pid_i)   i'
+    store (pid ~> pid_mv)  (kp*err + i' + kd*d)
+    store (pid ~> pid_err) err
+    ret err
+
+runPID :: IO ()
+runPID = runCompiler [cmodule] initialOpts { stdOut = True }
+
+cmodule :: Module
+cmodule = package "PID" $ do
+  defStruct (Proxy :: Proxy "PID")
+  incl pidUpdate
+  incl alloc_test
+
+alloc_test :: Def ('[] :-> IFloat)
+alloc_test  = proc "alloc_test" $ body $ do
+  pid <- local (istruct [pid_i .= ival 1])
+  ret =<< deref (pid ~> pid_i)
diff --git a/examples/PublicPrivate.hs b/examples/PublicPrivate.hs
new file mode 100644
--- /dev/null
+++ b/examples/PublicPrivate.hs
@@ -0,0 +1,46 @@
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE OverloadedStrings #-}
+
+module PublicPrivate where
+
+import Ivory.Language
+import Ivory.Compile.C.CmdlineFrontend
+
+
+[ivory|
+struct Foo { i :: Stored Uint32 }
+struct Bar { name :: Array 32 (Stored IChar) }
+|]
+
+privateHelper1 :: Def ('[Ref s (Struct "Foo")] :-> Ref s (Stored Uint32))
+privateHelper1  = proc "private_helper1" (\s -> body (ret (s ~> i)))
+
+privateHelper2 :: Def ('[] :-> ())
+privateHelper2  = proc "private_helper2" $ body retVoid
+
+publicFunction :: Def ('[Ref s (Struct "Bar")] :-> Uint32)
+publicFunction = proc "public_function" $ \_ -> body $ do
+  a <- call privateHelper1 (addrOf privateFoo)
+  call_ privateHelper2
+  ret =<< deref a
+
+privateFoo :: MemArea (Struct "Foo")
+privateFoo  = area "private_foo" Nothing
+
+cmodule :: Module
+cmodule = package "PublicPrivate" $ do
+  private $ do
+    defStruct (Proxy :: Proxy "Foo")
+    defMemArea privateFoo
+    incl privateHelper1
+    incl privateHelper2
+  public $ do
+    defStruct (Proxy :: Proxy "Bar")
+    incl publicFunction
+
+runPublicPrivate :: IO ()
+runPublicPrivate  = runCompiler [cmodule] initialOpts { stdOut = True, constFold = True }
diff --git a/examples/QC.hs b/examples/QC.hs
new file mode 100644
--- /dev/null
+++ b/examples/QC.hs
@@ -0,0 +1,72 @@
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE FlexibleInstances #-}
+
+module QC where
+
+import Ivory.Compile.C.CmdlineFrontend
+import Ivory.Language
+import Ivory.QuickCheck
+import Test.QuickCheck.Arbitrary
+
+[ivory|
+struct foo
+  { foo_a :: Stored IFloat
+  ; foo_b :: Stored Uint8
+  }
+|]
+
+-- Function we want to generate inputs for.
+func :: Def ('[Uint8
+              , Ref s (Array 3 (Stored Uint8))
+              , Ref s (Struct "foo")
+              ] :-> ())
+func = proc "func" $ \u arr str -> body $
+  arrayMap $ \ix -> do
+    a <- deref (arr ! ix)
+    b <- deref (str ~> foo_b)
+    store (arr ! ix) (a + b + u)
+
+type DriverDef = Def ('[] :-> ())
+
+-- Driver function.  Takes lists of the arguments we'll pass to the function
+-- test.
+driver :: [Uint8]
+       -> [Init (Array 3 (Stored Uint8))]
+       -> [Init (Struct "foo")]
+       -> DriverDef
+driver as0 as1 as2 = proc "main" $ body $ do
+  mapM_ oneCall (zip3 as0 as1 as2)
+
+  where
+  oneCall (a0, a1, a2) = do
+    a1' <- local a1
+    a2' <- local a2
+    call_ func a0 a1' a2'
+
+-- Generate the random values to pass.
+runTest :: IvoryGen DriverDef
+runTest = do
+  args0 <- samples num arbitrary
+  args1 <- samples num arbitrary
+  aFoos <- samples num foo_a
+  bFoos <- samples num foo_b
+  return $ driver args0 args1 (zipWith foo aFoos bFoos)
+  where
+  foo a b = istruct [ a, b ]
+  num = 10
+
+-- Compile!
+runTests :: IO ()
+runTests = do
+  d <- runIO runTest
+  runCompiler [cmodule d] initialOpts { includeDir = "test"
+                                      , srcDir     = "test"
+                                      , constFold  = True
+                                      }
+  where
+  cmodule d = package "qc" $ do
+    incl d
+    incl func
diff --git a/examples/SizeOf.hs b/examples/SizeOf.hs
new file mode 100644
--- /dev/null
+++ b/examples/SizeOf.hs
@@ -0,0 +1,28 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE DataKinds #-}
+
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+
+module SizeOf where
+
+import Ivory.Language
+
+[ivory|
+
+struct foo
+  { f1 :: Stored Uint8
+  ; f2 :: Stored Uint32
+  }
+
+|]
+
+
+test :: Def ('[] :-> Uint8)
+test  = proc "test" (body (ret (sizeOf (Proxy :: Proxy (Struct "foo")))))
+
+cmodule :: Module
+cmodule  = package "SizeOf" $ do
+  defStruct (Proxy :: Proxy "foo")
+  incl test
diff --git a/examples/String.hs b/examples/String.hs
new file mode 100644
--- /dev/null
+++ b/examples/String.hs
@@ -0,0 +1,28 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeOperators #-}
+
+module String where
+
+import Ivory.Language
+import Ivory.Compile.C.CmdlineFrontend
+
+printf :: Def ('[IString] :-> Sint32)
+printf  = importProc "printf" "stdio.h"
+
+printf2 :: Def ('[IString,Sint32] :-> Sint32)
+printf2  = importProc "printf" "stdio.h"
+
+test :: Def ('[] :-> ())
+test  = proc "test" $ body $ do
+  call_ printf "Hello, world\n"
+  call_ printf2 "howdy, %i \n" 3
+  retVoid
+
+runString :: IO ()
+runString = runCompiler [cmodule] initialOpts { stdOut = True }
+
+cmodule :: Module
+cmodule = package "String" $ do
+  incl printf
+  incl test
diff --git a/examples/TestClang.hs b/examples/TestClang.hs
new file mode 100644
--- /dev/null
+++ b/examples/TestClang.hs
@@ -0,0 +1,60 @@
+import System.Environment
+
+import qualified PID
+import qualified FibLoop
+import qualified Factorial
+import qualified String
+import qualified FunPtr
+import qualified Overflow
+import qualified Float
+import qualified Alloc
+import qualified Area
+import qualified Cond
+import qualified Forever
+import qualified PublicPrivate
+import qualified Bits
+import qualified SizeOf
+import qualified AddrOfRegression
+import qualified Array
+
+import Ivory.Compile.C.CmdlineFrontend
+import Ivory.Language (Module(),moduleName)
+import Ivory.Stdlib (stdlibModules)
+
+import qualified Ivory.Stdlib.SearchDir as S
+
+main :: IO ()
+main = do
+  args <- getArgs
+  let path = head args
+  let opts = initialOpts { includeDir = path, srcDir = path
+                         , rtIncludeDir = Nothing }
+
+  mapM_ (compileExample opts) modules
+
+  putStrLn "Compiling: Overflow"
+  Overflow.writeOverflow opts
+
+compileExample :: Opts -> Module -> IO ()
+compileExample opts m = do
+  putStrLn ("Compiling: " ++ moduleName m)
+  runCompilerWith Nothing (Just [S.searchDir]) [m] opts
+
+modules :: [Module]
+modules = [ PID.cmodule
+          , FibLoop.cmodule
+          , Factorial.cmodule
+          , String.cmodule
+          , FunPtr.cmodule
+          , Overflow.cmodule
+          , Float.cmodule
+          , Alloc.cmodule
+          , Area.cmodule
+          , Cond.cmodule
+          , Forever.cmodule
+          , PublicPrivate.cmodule
+          , Bits.cmodule
+          , SizeOf.cmodule
+          , AddrOfRegression.cmodule
+          , Array.cmodule
+          ] ++ stdlibModules
diff --git a/ivory-examples.cabal b/ivory-examples.cabal
new file mode 100644
--- /dev/null
+++ b/ivory-examples.cabal
@@ -0,0 +1,68 @@
+name:                ivory-examples
+version:             0.1.0.0
+author:              Galois, Inc
+maintainer:          trevor@galois.com
+copyright:           2013 Galois, Inc.
+category:            Language
+synopsis:            Ivory examples.
+description:         Various examples demonstrating the use of Ivory.
+homepage:            http://smaccmpilot.org/languages/ivory-introduction.html
+build-type:          Simple
+cabal-version:       >= 1.10
+license:             BSD3
+license-file:        LICENSE
+source-repository    this
+  type:     git
+  location: https://github.com/GaloisInc/ivory
+  tag:      hackage-examples-0100
+
+
+executable ivory-fibtutorial
+  main-is:              FibTutorial.hs
+  hs-source-dirs:       examples
+  build-depends:        base >= 4.6,
+                        pretty >= 1.1,
+                        monadLib >= 3.7,
+                        template-haskell >= 2.8,
+                        mainland-pretty >= 0.2.4,
+                        wl-pprint,
+                        ivory,
+                        ivory-opts,
+                        ivory-backend-c,
+                        ivory-quickcheck,
+                        ivory-stdlib,
+                        QuickCheck
+  default-language:     Haskell2010
+  ghc-options:          -Wall
+
+executable ivory-c-clang-test
+  main-is:              TestClang.hs
+  other-modules:        Factorial,
+                        FibLoop,
+                        PID,
+                        String,
+                        FunPtr,
+                        Float,
+                        Area,
+                        Cond,
+                        Forever,
+                        PublicPrivate,
+                        Bits,
+                        SizeOf,
+                        AddrOfRegression,
+                        QC
+  hs-source-dirs:       examples
+  build-depends:        base >= 4.6 && < 4.7,
+                        pretty >= 1.1,
+                        monadLib >= 3.7,
+                        template-haskell >= 2.8,
+                        mainland-pretty >= 0.2.4,
+                        wl-pprint,
+                        ivory,
+                        ivory-opts,
+                        ivory-quickcheck,
+                        ivory-backend-c,
+                        ivory-stdlib,
+                        QuickCheck
+  default-language:     Haskell2010
+  ghc-options:          -Wall