diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2015, Anders Persson, Emil Axelsson, Markus Aronsson
+
+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 Anders Persson, Emil Axelsson, Markus Aronsson nor the names of other
+      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/Concurrent.hs b/examples/Concurrent.hs
new file mode 100644
--- /dev/null
+++ b/examples/Concurrent.hs
@@ -0,0 +1,75 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Concurrent where
+
+import Prelude hiding (break)
+
+#if __GLASGOW_HASKELL__ < 710
+import Control.Applicative
+#endif
+
+import Language.Embedded.Imperative
+import Language.Embedded.Concurrent
+import Language.Embedded.CExp
+
+type L =
+  ThreadCMD :+:
+  ChanCMD CExp :+:
+  ControlCMD CExp :+:
+  FileCMD CExp
+
+-- | Deadlocks due to channel becoming full.
+deadlock :: Program L ()
+deadlock = do
+  c <- newChan 1
+  t <- fork $ readChan c >>= printf "%d\n"
+  writeChan c (1 :: CExp Int32)
+  writeChan c 2
+  writeChan c 3
+  printf "This never happens: %d\n" (4 :: CExp Int32)
+
+-- | Map a function over a file, then print the results. Mapping and printing
+--   happen in separate threads.
+mapFile :: (CExp Float -> CExp Float) -> FilePath -> Program L ()
+mapFile f i = do
+  c1 <- newCloseableChan 5
+  c2 <- newCloseableChan 5
+  fi <- fopen i ReadMode
+
+  t1 <- fork $ do
+    while (return true) $ do
+      x <- readChan c1
+      readOK <- lastChanReadOK c1
+      iff readOK
+        (void $ writeChan c2 (f x))
+        (closeChan c2 >> break)
+
+  t2 <- fork $ do
+    while (lastChanReadOK c2) $ do
+      readChan c2 >>= printf "%f\n"
+
+  t3 <- fork $ do
+    while (not_ <$> feof fi) $ do
+      fget fi >>= void . writeChan c1
+    fclose fi
+    closeChan c1
+  waitThread t2
+
+-- | Waiting for thread completion.
+waiting :: Program L ()
+waiting = do
+  t <- fork $ printf "Forked thread printing %d\n" (0 :: CExp Int32)
+  waitThread t
+  printf "Main thread printing %d\n" (1 :: CExp Int32)
+
+-- | A thread kills itself using its own thread ID.
+suicide :: Program L ()
+suicide = do
+  tid <- forkWithId $ \tid -> do
+    printf "This is printed. %d\n" (0 :: CExp Int32)
+    killThread tid
+    printf "This is not. %d\n" (0 :: CExp Int32)
+  waitThread tid
+  printf "The thread is dead, long live the thread! %d\n" (0 :: CExp Int32)
+
diff --git a/examples/Imperative.hs b/examples/Imperative.hs
new file mode 100644
--- /dev/null
+++ b/examples/Imperative.hs
@@ -0,0 +1,80 @@
+{-# LANGUAGE TypeOperators #-}
+
+module Imperative where
+
+
+
+import Data.Int
+import Data.Word
+
+import Language.Embedded.Expression (evalExp)
+import Language.Embedded.Imperative
+import Language.Embedded.Backend.C
+import Language.Embedded.CExp
+
+
+
+refProg :: Program (RefCMD CExp) (CExp Int32)
+refProg = do
+    r1 <- initRef 4
+    r2 <- initRef 5
+    a  <- unsafeFreezeRef r1
+    b  <- getRef r2
+    let c = (a #== 10 ? a+b $ b+a) + 3
+    setRef r2 c
+    return c
+
+type CMD1
+    =   RefCMD CExp
+    :+: ArrCMD CExp
+    :+: ControlCMD CExp
+
+arrProg :: Program CMD1 (CExp Int32)
+arrProg = do
+    ref <- initRef 4
+    arr <- newArr (10 :: CExp Word8)
+    setArr 3 45 arr
+    a   <- unsafeFreezeRef ref
+    b   <- getArr 3 arr
+    let c = a+b
+    iff (a #== 4)
+      (setRef ref c)
+      (setRef ref b)
+    return c
+
+evalRef :: IO Int32
+evalRef = fmap evalExp $ runIO refProg
+
+compRef = icompile refProg
+
+evalArr :: IO Int32
+evalArr = fmap evalExp $ runIO arrProg
+
+compArr = icompile arrProg
+
+
+
+type CMD2
+    =   RefCMD CExp
+    :+: ControlCMD CExp
+    :+: FileCMD CExp
+
+summer :: Program CMD2 ()
+summer = do
+    inp <- fopen "input" ReadMode
+    let cont = fmap not_ $ feof inp
+    sum <- initRef (0 :: CExp Float)
+    while cont $ do
+        f <- fget inp
+        s <- getRef sum
+        setRef sum (s+f+(3+4+5+6))
+    s <- getRef sum
+    printf "The sum is: %f\n" s
+
+runSummer :: IO ()
+runSummer = do
+    writeFile "input" $ unwords $ map show ([-5..4] :: [Float])
+    runIO summer
+
+compSummer = icompile summer
+
diff --git a/imperative-edsl.cabal b/imperative-edsl.cabal
new file mode 100644
--- /dev/null
+++ b/imperative-edsl.cabal
@@ -0,0 +1,135 @@
+name:                imperative-edsl
+version:             0.4.1
+synopsis:            Deep embedding of imperative programs with code generation
+description:         Deep embedding of imperative programs with code generation.
+                     .
+                     The main module for users who want to write imperative
+                     programs is "Language.Embedded.Imperative" (and optionally
+                     "Language.Embedded.Expr" which provides a simple expression
+                     language).
+                     .
+                     Examples can be found in the @examples@ directory.
+license:             BSD3
+license-file:        LICENSE
+author:              Anders Persson, Emil Axelsson, Markus Aronsson
+maintainer:          emax@chalmers.se
+copyright:           Copyright 2015 Anders Persson, Emil Axelsson, Markus Aronsson
+homepage:            https://github.com/emilaxelsson/imperative-edsl
+bug-reports:         https://github.com/emilaxelsson/imperative-edsl/issues
+category:            Language
+build-type:          Simple
+cabal-version:       >=1.10
+
+source-repository head
+  type:     git
+  location: git@github.com:emilaxelsson/imperative-edsl.git
+
+Flag old-syntactic
+  Description: Use syntactic < 2
+  Default:     False
+
+library
+  exposed-modules:
+    Control.Monads
+    Language.C.Monad
+    Language.Embedded.Expression
+    Language.Embedded.Traversal
+    Language.Embedded.Imperative.Args
+    Language.Embedded.Imperative.CMD
+    Language.Embedded.Imperative.Frontend.General
+    Language.Embedded.Imperative.Frontend
+    Language.Embedded.Imperative
+    Language.Embedded.Concurrent.CMD
+    Language.Embedded.Concurrent
+    Language.Embedded.Signature
+    Language.Embedded.Backend.C
+    Language.Embedded.CExp
+
+  other-modules:
+    Language.Embedded.Imperative.Backend.C
+    Language.Embedded.Concurrent.Backend.C
+      -- No need to export these since only the instances are interesting
+
+  default-language: Haskell2010
+
+  default-extensions:
+    ConstraintKinds
+    DefaultSignatures
+    DeriveDataTypeable
+    DeriveFunctor
+    FlexibleContexts
+    FlexibleInstances
+    GADTs
+    GeneralizedNewtypeDeriving
+    MultiParamTypeClasses
+    Rank2Types
+    ScopedTypeVariables
+    StandaloneDeriving
+    TypeFamilies
+    TypeOperators
+
+  other-extensions:
+    PolyKinds
+    QuasiQuotes
+    UndecidableInstances
+
+  build-depends:
+    array,
+    base >=4 && <5,
+    constraints,
+    containers,
+    exception-transformers,
+    language-c-quote >= 0.11 && < 0.12,
+    mainland-pretty >= 0.4 && < 0.5,
+    microlens >= 0.3.0.0,
+    microlens-mtl,
+    microlens-th,
+    mtl,
+    operational-alacarte,
+    tagged,
+      -- tagged needed for GHC 7.6
+    BoundedChan,
+    srcloc
+
+  if flag(old-syntactic)
+    build-depends:
+      syntactic < 2
+  else
+    build-depends:
+      open-typerep >= 0.4,
+      syntactic >= 3.2
+
+  hs-source-dirs: src
+
+test-suite Examples
+  type: exitcode-stdio-1.0
+
+  hs-source-dirs: tests examples
+
+  main-is: Examples.hs
+
+  other-modules:
+    Concurrent
+    Imperative
+
+  default-language: Haskell2010
+
+  build-depends:
+    base,
+    imperative-edsl,
+    mainland-pretty,
+    directory,
+    process
+
+test-suite Semantics
+  type: exitcode-stdio-1.0
+
+  hs-source-dirs: tests
+
+  main-is: Semantics.hs
+
+  default-language: Haskell2010
+
+  build-depends:
+    base,
+    imperative-edsl
diff --git a/src/Control/Monads.hs b/src/Control/Monads.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monads.hs
@@ -0,0 +1,129 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Control.Monads where
+
+
+
+#if __GLASGOW_HASKELL__ < 710
+import Control.Applicative
+#endif
+import Control.Monad.Exception
+import Control.Monad.Identity
+import Control.Monad.Reader
+import qualified Control.Monad.State.Lazy as L
+import Control.Monad.State.Strict
+import Control.Monad.Writer
+
+import Language.Embedded.Expression
+
+
+
+newtype SupplyT m a = SupplyT { unSupplyT :: StateT VarId m a }
+  deriving (Functor, Applicative, Monad, MonadFix, MonadIO, MonadTrans)
+
+type Supply = SupplyT Identity
+
+class Monad m => MonadSupply m
+  where
+    -- | Create a fresh variable identifier
+    fresh :: m VarId
+    default fresh :: (m ~ t n, MonadTrans t, MonadSupply n) => m VarId
+    fresh = lift fresh
+
+instance Monad m => MonadSupply (SupplyT m)
+  where
+    fresh = do
+        v <- SupplyT get
+        SupplyT $ put (v+1)
+        return v
+
+instance MonadSupply m             => MonadSupply (ExceptionT m)
+instance MonadSupply m             => MonadSupply (ReaderT  r m)
+instance MonadSupply m             => MonadSupply (L.StateT s m)
+instance MonadSupply m             => MonadSupply (StateT   s m)
+instance (MonadSupply m, Monoid w) => MonadSupply (WriterT  w m)
+
+instance MonadException m => MonadException (SupplyT m)
+  where
+    throw = lift . throw
+    catch m h = SupplyT $ catch (unSupplyT m) (unSupplyT . h)
+
+instance MonadReader r m => MonadReader r (SupplyT m)
+  where
+    ask     = lift ask
+    local f = SupplyT . local f . unSupplyT
+
+instance MonadState s m => MonadState s (SupplyT m)
+  where
+    get = lift get
+    put = lift . put
+
+instance MonadWriter w m => MonadWriter w (SupplyT m)
+  where
+    tell   = SupplyT . tell
+    listen = SupplyT . listen . unSupplyT
+    pass   = SupplyT . pass   . unSupplyT
+
+runSupplyT :: Monad m => SupplyT m a -> m a
+runSupplyT = flip evalStateT 0 . unSupplyT
+
+runSupply :: Supply a -> a
+runSupply = runIdentity . runSupplyT
+
+
+
+-- | Program location
+type Loc = Integer
+
+-- | Tick monad
+newtype TickT m a = TickT { unTickT :: StateT Loc m a }
+  deriving (Functor, Applicative, Monad, MonadFix, MonadTrans)
+
+type Tick = TickT Identity
+
+class Monad m => MonadTick m
+  where
+    tick :: m ()
+    default tick :: (m ~ t n, MonadTrans t, MonadTick n) => m ()
+    tick = lift tick
+    loc  :: m Loc
+    default loc :: (m ~ t n, MonadTrans t, MonadTick n) => m Loc
+    loc = lift loc
+
+instance Monad m => MonadTick (TickT m)
+  where
+    tick = do l <- loc; TickT $ put (l+1)
+    loc  = TickT get
+
+instance MonadTick m             => MonadTick (ReaderT  r m)
+instance MonadTick m             => MonadTick (L.StateT s m)
+instance MonadTick m             => MonadTick (StateT   s m)
+instance (MonadTick m, Monoid w) => MonadTick (WriterT  w m)
+
+instance MonadReader r m => MonadReader r (TickT m)
+  where
+    ask     = lift ask
+    local f = TickT . local f . unTickT
+
+instance MonadState s m => MonadState s (TickT m)
+  where
+    get = lift get
+    put = lift . put
+
+instance MonadWriter w m => MonadWriter w (TickT m)
+  where
+    tell   = TickT . tell
+    listen = TickT . listen . unTickT
+    pass   = TickT . pass   . unTickT
+
+runTickT :: Monad m => TickT m a -> m a
+runTickT = flip evalStateT 0 . unTickT
+
+runTick :: Tick a -> a
+runTick = runIdentity . runTickT
+
+-- | Create a fresh string identifier with the given prefix
+freshStr :: MonadSupply m => String -> m String
+freshStr prefix = liftM ((prefix ++) . show) fresh
+
diff --git a/src/Language/C/Monad.hs b/src/Language/C/Monad.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/C/Monad.hs
@@ -0,0 +1,449 @@
+-- Copyright (c) 2009-2010
+--         The President and Fellows of Harvard College.
+--
+-- Redistribution and use in source and binary forms, with or without
+-- modification, are permitted provided that the following conditions
+-- are met:
+-- 1. Redistributions of source code must retain the above copyright
+--    notice, this list of conditions and the following disclaimer.
+-- 2. 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.
+-- 3. Neither the name of the University 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 UNIVERSITY 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 UNIVERSITY 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.
+
+-- Copyright (c) 2011-2012, Geoffrey Mainland
+-- All rights reserved.
+--
+-- Redistribution and use in source and binary forms, with or without modification,
+-- are permitted provided that the following conditions are met:
+-- 1. Redistributions of source code must retain the above copyright notice, this
+--    list of conditions and the following disclaimer.
+--
+-- 2. 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.
+--
+-- 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 HOLDER 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.
+
+-- Copyright (c) 2015, Anders Persson
+--
+-- 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 Anders Persson nor the names of other
+--       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.
+
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+
+-- | A monad for C code generation
+module Language.C.Monad
+  where
+
+import Lens.Micro
+import Lens.Micro.Mtl
+import Lens.Micro.TH
+#if __GLASGOW_HASKELL__ < 710
+import Control.Applicative
+#endif
+import Control.Monad.Identity
+import Control.Monad.State.Strict
+import Control.Monad.Exception
+
+import Language.C.Quote.C
+import qualified Language.C.Syntax as C
+import qualified Data.Map as Map
+import qualified Data.Set as Set
+import Data.Monoid
+import Text.PrettyPrint.Mainland
+import Data.Loc
+import Data.List (partition,nub)
+
+-- | Code generation flags
+data Flags = Flags
+
+-- | Code generator state.
+data CEnv = CEnv
+    { _flags       :: Flags
+
+    , _unique      :: !Integer
+
+    , _modules     :: Map.Map String [C.Definition]
+    , _includes    :: Set.Set String
+    , _typedefs    :: [C.Definition]
+    , _prototypes  :: [C.Definition]
+    , _globals     :: [C.Definition]
+
+    , _aliases     :: Map.Map Integer String
+    , _params      :: [C.Param]
+    , _args        :: [C.Exp]
+    , _locals      :: [C.InitGroup]
+    , _stms        :: [C.Stm]
+    , _finalStms   :: [C.Stm]
+
+    , _usedVars    :: Set.Set C.Id
+    , _funUsedVars :: Map.Map String (Set.Set C.Id)
+    }
+
+makeLenses ''CEnv
+
+-- | Reimplementation of @<<%=@ from the lens package
+(<<%=) :: MonadState s m =>
+    (forall f . Functor f => LensLike' f s a) -> (a -> a) -> m a
+l <<%= f = do
+    s <- get
+    l %= f
+    return (s ^. l)
+
+-- | Reimplementation of @<<.=@ from the lens package
+(<<.=) :: MonadState s m =>
+    (forall f . Functor f => LensLike' f s a) -> a -> m a
+l <<.= f = do
+    s <- get
+    l .= f
+    return (s ^. l)
+
+-- | Default code generator state
+defaultCEnv :: Flags -> CEnv
+defaultCEnv fl = CEnv
+    { _flags       = fl
+    , _unique      = 0
+    , _modules     = mempty
+    , _includes    = mempty
+    , _typedefs    = mempty
+    , _prototypes  = mempty
+    , _globals     = mempty
+    , _aliases     = mempty
+    , _params      = mempty
+    , _args        = mempty
+    , _locals      = mempty
+    , _stms        = mempty
+    , _finalStms   = mempty
+    , _usedVars    = mempty
+    , _funUsedVars = mempty
+    }
+
+-- | Code generation type constraints
+type MonadC m = (Functor m, Applicative m, Monad m, MonadState CEnv m, MonadException m, MonadFix m)
+
+-- | The C code generation monad transformer
+newtype CGenT t a = CGenT { unCGenT :: StateT CEnv (ExceptionT t) a }
+  deriving (Functor, Applicative, Monad, MonadException, MonadState CEnv, MonadIO, MonadFix)
+
+type CGen = CGenT Identity
+
+-- | Run the C code generation monad
+runCGenT :: Monad m => CGenT m a -> CEnv -> m (a, CEnv)
+runCGenT m s = do
+    Right ac <- runExceptionT (runStateT (unCGenT m) s)
+    return ac
+
+-- | Run the C code generation monad
+runCGen :: CGen a -> CEnv -> (a, CEnv)
+runCGen m = runIdentity . runCGenT m
+
+-- | Extract a compilation unit from the 'CEnv' state
+cenvToCUnit :: CEnv -> [C.Definition]
+cenvToCUnit env =
+    [cunit|$edecls:incs
+           $edecls:tds
+           $edecls:protos
+           $edecls:globs|]
+  where
+    incs = map toInclude (Set.toList (_includes env))
+      where
+        toInclude :: String -> C.Definition
+        toInclude inc = [cedecl|$esc:include|]
+          where include = "#include " ++ inc
+    tds    = nub $ reverse $ _typedefs env
+    protos = nub $ reverse $ _prototypes env
+    globs  = nub $ reverse $ _globals env
+
+-- | Generate a C document
+prettyCGenT :: Monad m => CGenT m a -> m Doc
+prettyCGenT ma = do
+    (_,cenv) <- runCGenT ma (defaultCEnv Flags)
+    return $ ppr $ cenvToCUnit cenv
+
+prettyCGen :: CGen a -> Doc
+prettyCGen = runIdentity . prettyCGenT
+
+-- | Retrieve a fresh identifier
+freshId :: MonadC m => m Integer
+freshId = unique <<%= succ
+
+-- | Generate a fresh symbol by appending a fresh id to a base name
+gensym :: MonadC m => String -> m String
+gensym s = do
+    u <- freshId
+    return $ s ++ show u
+
+-- | Mark an identifier as used in this context.
+touchVar :: (MonadC m, ToIdent v) => v -> m ()
+touchVar v = usedVars %= Set.insert (toIdent v (SrcLoc NoLoc))
+
+-- | Set the 'Set' of identifers used in the body of the given function.
+setUsedVars :: MonadC m => String -> Set.Set C.Id -> m ()
+setUsedVars fun uvs = funUsedVars %= Map.insert fun uvs
+
+-- | Add an include pre-processor directive. Specify '<>' or '""' around
+-- the file name.
+addInclude :: MonadC m => String -> m ()
+addInclude inc = includes %= Set.insert inc
+
+-- | Add a local include directive. The argument will be surrounded by '""'
+addLocalInclude :: MonadC m => String -> m ()
+addLocalInclude inc = addInclude ("\"" ++ inc ++ "\"")
+
+-- | Add a system include directive. The argument will be surrounded by '<>'
+addSystemInclude :: MonadC m => String -> m ()
+addSystemInclude inc = addInclude ("<" ++ inc ++ ">")
+
+-- | Add a type definition
+addTypedef :: MonadC m => C.Definition -> m ()
+addTypedef def = typedefs %= (def:)
+
+-- | Add a function prototype
+addPrototype :: MonadC m => C.Definition -> m ()
+addPrototype def = prototypes %= (def:)
+
+-- | Add a global definition
+addGlobal :: MonadC m => C.Definition -> m ()
+addGlobal def = globals %= (def:)
+
+-- | Add multiple global definitions
+addGlobals :: MonadC m => [C.Definition] -> m ()
+addGlobals defs = globals %= (defs++)
+
+-- | Let a variable be known by another name
+withAlias :: MonadC m => Integer -> String -> m a -> m a
+withAlias i n act = do
+  oldAliases <- aliases <<%= Map.insert i n
+  a <- act
+  aliases .= oldAliases
+  return a
+
+-- | Add a function parameter when building a function definition
+addParam :: MonadC m => C.Param -> m ()
+addParam param = params %= (param:)
+
+addParams :: MonadC m => [C.Param] -> m ()
+addParams ps = params %= (reverse ps++)
+
+-- | Add a function argument when building a function call
+addArg :: MonadC m => C.Exp -> m ()
+addArg arg = args %= (arg:)
+
+-- | Add a local declaration (including initializations)
+addLocal :: MonadC m => C.InitGroup -> m ()
+addLocal def = do
+  locals %= (def:)
+  case def of
+    C.InitGroup _ _ is _ -> forM_ is $ \(C.Init id _ _ _ _ _) -> touchVar id
+    _                    -> return ()
+
+-- | Add multiple local declarations
+addLocals :: MonadC m => [C.InitGroup] -> m ()
+addLocals defs = mapM_ addLocal defs -- locals %= (reverse defs++)
+
+-- | Add a statement to the current block
+addStm :: MonadC m => C.Stm -> m ()
+addStm stm = stms %= (stm:)
+
+-- | Add a sequence of statements to the current block
+addStms :: MonadC m => [C.Stm] -> m ()
+addStms ss = stms %= (reverse ss++)
+
+-- | Add a statement to the end of the current block
+addFinalStm :: MonadC m => C.Stm -> m ()
+addFinalStm stm = finalStms %= (stm:)
+
+-- | Run an action in a new block
+inBlock :: MonadC m => m a -> m a
+inBlock ma = do
+    (a, items) <- inNewBlock ma
+    addStm [cstm|{ $items:items }|]
+    return a
+
+-- | Run an action as a block and capture the items.
+-- Does not place the items in an actual C block.
+inNewBlock :: MonadC m => m a -> m (a, [C.BlockItem])
+inNewBlock ma = do
+    oldLocals    <- locals    <<.= mempty
+    oldStms      <- stms      <<.= mempty
+    oldFinalStms <- finalStms <<.= mempty
+    x <- ma
+    ls  <- reverse <$> (locals    <<.= oldLocals)
+    ss  <- reverse <$> (stms      <<.= oldStms)
+    fss <- reverse <$> (finalStms <<.= oldFinalStms)
+    return (x, map C.BlockDecl ls  ++
+               map C.BlockStm  ss  ++
+               map C.BlockStm  fss
+           )
+
+-- | Run an action as a block and capture the items.
+-- Does not place the items in an actual C block.
+inNewBlock_ :: MonadC m => m a -> m [C.BlockItem]
+inNewBlock_ ma = snd <$> inNewBlock ma
+
+-- | Run an action as a function declaration.
+-- Does not create a new function.
+inNewFunction :: MonadC m => m a -> m (a,Set.Set C.Id,[C.Param],[C.BlockItem])
+inNewFunction comp = do
+    oldParams <- params <<.= mempty
+    oldUsedVars <- usedVars <<.= mempty
+    (a,items)  <- inNewBlock comp
+    ps <- params <<.= oldParams
+    uvs <- usedVars <<.= oldUsedVars
+    return (a, uvs, reverse ps, items)
+
+-- | Declare a function
+inFunction :: MonadC m => String -> m a -> m a
+inFunction = inFunctionTy [cty|void|]
+
+-- | Declare a function with the given return type.
+inFunctionTy :: MonadC m => C.Type -> String -> m a -> m a
+inFunctionTy ty fun ma = do
+    (a,uvs,ps,items) <- inNewFunction ma
+    setUsedVars fun uvs
+    addPrototype [cedecl| $ty:ty $id:fun($params:ps);|]
+    addGlobal [cedecl| $ty:ty $id:fun($params:ps){ $items:items }|]
+    return a
+
+-- | Collect all global definitions in the current state
+collectDefinitions :: MonadC m => m a -> m (a, [C.Definition])
+collectDefinitions ma = do
+    oldIncludes   <- includes   <<.= mempty
+    oldTypedefs   <- typedefs   <<.= mempty
+    oldPrototypes <- prototypes <<.= mempty
+    oldGlobals    <- globals    <<.= mempty
+    a  <- ma
+    s' <- get
+    modify $ \s -> s { _includes   = oldIncludes    -- <> _includes s'
+                     , _typedefs   = oldTypedefs    -- <> _typedefs s'
+                     , _prototypes = oldPrototypes  -- <> _prototypes s'
+                     , _globals    = oldGlobals     -- <> _globals s'
+                     }
+    return (a, cenvToCUnit s')
+
+-- | Collect all function arguments in the current state
+collectArgs :: MonadC m => m [C.Exp]
+collectArgs = args <<.= mempty
+
+-- | Declare a C translation unit
+inModule :: MonadC m => String -> m a -> m a
+inModule name prg = do
+    oldUnique <- unique <<.= 0
+    (a, defs) <- collectDefinitions prg
+    unique .= oldUnique
+    modules %= Map.insertWith (<>) name defs
+    return a
+
+-- | Wrap a program in a main function
+wrapMain :: MonadC m => m a -> m ()
+wrapMain prog = do
+    (_,uvs,params,items) <- inNewFunction $ prog >> addStm [cstm| return 0; |]
+    setUsedVars "main" uvs
+    addGlobal [cedecl| int main($params:params){ $items:items }|]
+
+-- | Lift the declarations of all variables that are shared between functions
+--   to the top level. This relies on variable IDs being unique across
+--   programs, not just across the functions in which they are declared.
+--
+--   Only affects locally declared vars, not function arguments.
+liftSharedLocals :: MonadC m => m a -> m ()
+liftSharedLocals prog = do
+    prog
+    uvs <- Set.unions . Map.elems . onlyShared . _funUsedVars <$> get
+    -- This could be more efficient by just filtering each function for the
+    -- vars we *know* are in there, provided that we had a Map from function
+    -- names to bodies.
+    oldglobs <- _globals <$> get
+    let (globs, shared) = unzip $ map (extractDecls (`Set.member` uvs)) oldglobs
+        sharedList = Set.toList $ Set.unions shared
+        sharedDecls = map (\ig -> C.DecDef ig (SrcLoc NoLoc)) sharedList
+    void $ globals <<.= (globs ++ sharedDecls)
+  where
+    -- Only keep vars shared between functions by intersecting with the union
+    -- of all other funs' uvs. TODO: optimize.
+    onlyShared :: Map.Map String (Set.Set C.Id) -> Map.Map String (Set.Set C.Id)
+    onlyShared alluvs =
+        Map.mapWithKey funUVSIntersects alluvs
+      where
+        funUVSIntersects fun uvs =
+          Set.intersection uvs $ Set.unions $ Map.elems $ Map.delete fun alluvs
+
+-- | Remove all declarations matching a predicate from the given function
+--   and return them in a separate list.
+extractDecls :: (C.Id -> Bool)
+             -> C.Definition
+             -> (C.Definition, Set.Set C.InitGroup)
+extractDecls pred (C.FuncDef (C.Func ds id decl params bis loc') loc) =
+  case foldr perBI ([], Set.empty) bis of
+    (bis', igs) -> (C.FuncDef (C.Func ds id decl params bis' loc') loc, igs)
+  where
+    perBI decl@(C.BlockDecl ig@(C.InitGroup ds attrs is loc)) (bis, igs) =
+      case partition (\(C.Init id _ _ _ _ _) -> pred id) is of
+        ([], unmach) ->
+          (decl : bis, igs)
+        (match, []) ->
+          (bis, Set.insert ig igs)
+        (match, unmatch) ->
+          (C.BlockDecl (C.InitGroup ds attrs unmatch loc) : bis,
+           Set.insert (C.InitGroup ds attrs match loc) igs)
+    perBI bi (bis, igs) =
+      (bi:bis, igs)
+extractDecls _ decl =
+  (decl, Set.empty)
diff --git a/src/Language/Embedded/Backend/C.hs b/src/Language/Embedded/Backend/C.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Embedded/Backend/C.hs
@@ -0,0 +1,67 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE QuasiQuotes #-}
+
+-- | C code generation for 'Program'
+
+module Language.Embedded.Backend.C where
+
+
+
+#if __GLASGOW_HASKELL__ < 710
+import Control.Applicative
+#endif
+
+import Data.Loc (noLoc)
+import qualified Language.C.Syntax as C
+
+import Control.Monad.Operational.Higher
+import Language.C.Monad
+
+import Text.PrettyPrint.Mainland (pretty)
+
+
+
+--------------------------------------------------------------------------------
+-- * Utilities
+--------------------------------------------------------------------------------
+
+-- | Create a named type
+namedType :: String -> C.Type
+namedType t = C.Type
+    (C.DeclSpec [] [] (C.Tnamed (C.Id t noLoc) [] noLoc) noLoc)
+    (C.DeclRoot noLoc)
+    noLoc
+
+-- | Return the argument of a boolean negation expression
+viewNotExp :: C.Exp -> Maybe C.Exp
+viewNotExp (C.UnOp C.Lnot a _)                     = Just a
+viewNotExp (C.FnCall (C.Var (C.Id "!" _) _) [a] _) = Just a
+  -- Apparently this is what `!` parses to
+viewNotExp _ = Nothing
+
+
+
+--------------------------------------------------------------------------------
+-- * Code generation user interface
+--------------------------------------------------------------------------------
+
+-- | Compile a program to C code represented as a string
+--
+-- For programs that make use of the primitives in
+-- "Language.Embedded.Concurrent", the resulting C code can be compiled as
+-- follows:
+--
+-- > gcc -Iinclude csrc/chan.c -lpthread YOURPROGRAM.c
+compile :: (Interp instr CGen, HFunctor instr) => Program instr a -> String
+compile = pretty 80 . prettyCGen . liftSharedLocals . wrapMain . interpret
+
+-- | Compile a program to C code and print it on the screen
+--
+-- For programs that make use of the primitives in
+-- "Language.Embedded.Concurrent", the resulting C code can be compiled as
+-- follows:
+--
+-- > gcc -Iinclude csrc/chan.c -lpthread YOURPROGRAM.c
+icompile :: (Interp instr CGen, HFunctor instr) => Program instr a -> IO ()
+icompile = putStrLn . compile
+
diff --git a/src/Language/Embedded/CExp.hs b/src/Language/Embedded/CExp.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Embedded/CExp.hs
@@ -0,0 +1,452 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE TemplateHaskell #-}
+
+-- | Typed deep embedding of simple C expressions
+--
+-- This is a subset of C expressions that only have simple non-compound and
+-- non-pointed types, and that don't contain any control structures.
+--
+-- (Of course, nothing stops one from translating 'CExp' to something other than
+-- C, but its constructors and set of supported types is inspired by C.)
+
+module Language.Embedded.CExp where
+
+
+
+import Data.Int
+import Data.Maybe
+import Data.Word
+#if __GLASGOW_HASKELL__ < 710
+import Data.Monoid
+#endif
+import Data.Typeable
+
+#if MIN_VERSION_syntactic(3,0,0)
+import Language.Syntactic
+import Language.Syntactic.Functional (Denotation)
+import Language.Syntactic.TH
+#else
+import Language.Syntactic
+#endif
+
+#if MIN_VERSION_syntactic(3,0,0)
+import Data.TypeRep hiding (Typeable, gcast)
+import Data.TypeRep.TH
+import Data.TypeRep.Types.Basic
+import Data.TypeRep.Types.Tuple
+import Data.TypeRep.Types.IntWord
+#endif
+
+import Language.C.Quote.C
+import Language.C.Syntax (Type, UnOp (..), BinOp (..), Exp (UnOp, BinOp))
+import qualified Language.C.Syntax as C
+
+import Language.C.Monad
+import Language.Embedded.Expression
+
+
+
+--------------------------------------------------------------------------------
+-- * Types
+--------------------------------------------------------------------------------
+
+-- | Types supported by C
+class (Show a, Eq a, Typeable a) => CType a
+  where
+    cType :: MonadC m => proxy a -> m Type
+
+instance CType Bool   where cType _ = addSystemInclude "stdbool.h" >> return [cty| typename bool     |]
+instance CType Int8   where cType _ = addSystemInclude "stdint.h"  >> return [cty| typename int8_t   |]
+instance CType Int16  where cType _ = addSystemInclude "stdint.h"  >> return [cty| typename int16_t  |]
+instance CType Int32  where cType _ = addSystemInclude "stdint.h"  >> return [cty| typename int32_t  |]
+instance CType Int64  where cType _ = addSystemInclude "stdint.h"  >> return [cty| typename int64_t  |]
+instance CType Word8  where cType _ = addSystemInclude "stdint.h"  >> return [cty| typename uint8_t  |]
+instance CType Word16 where cType _ = addSystemInclude "stdint.h"  >> return [cty| typename uint16_t |]
+instance CType Word32 where cType _ = addSystemInclude "stdint.h"  >> return [cty| typename uint32_t |]
+instance CType Word64 where cType _ = addSystemInclude "stdint.h"  >> return [cty| typename uint64_t |]
+
+instance CType Float  where cType _ = return [cty| float |]
+instance CType Double where cType _ = return [cty| double |]
+
+#if MIN_VERSION_syntactic(3,0,0)
+instance ShowClass CType where showClass _ = "CType"
+
+pCType :: Proxy CType
+pCType = Proxy
+
+deriveWitness ''CType ''BoolType
+deriveWitness ''CType ''FloatType
+deriveWitness ''CType ''DoubleType
+deriveWitness ''CType ''IntWordType
+
+derivePWitness ''CType ''BoolType
+derivePWitness ''CType ''FloatType
+derivePWitness ''CType ''DoubleType
+derivePWitness ''CType ''IntWordType
+
+instance PWitness CType CharType t
+instance PWitness CType ListType t
+instance PWitness CType TupleType t
+instance PWitness CType FunType t
+#endif
+
+-- | Return whether the type of the expression is a floating-point numeric type
+isFloat :: forall a . CType a => CExp a -> Bool
+isFloat a
+    | t == typeOf (undefined :: Float)  = True
+    | t == typeOf (undefined :: Double) = True
+    | otherwise = False
+  where
+    t = typeOf (undefined :: a)
+
+-- | Return whether the type of the expression is a non-floating-point type
+isExact :: CType a => CExp a -> Bool
+isExact = not . isFloat
+
+
+
+--------------------------------------------------------------------------------
+-- * Expressions
+--------------------------------------------------------------------------------
+
+-- | Syntactic symbols for C
+data Sym sig
+  where
+    -- Function or literal
+#if MIN_VERSION_syntactic(3,0,0)
+    Fun  :: Signature sig => String -> Denotation sig -> Sym sig
+#else
+    Fun  :: String -> Denotation sig -> Sym sig
+#endif
+    -- Unary operator
+    UOp  :: UnOp -> (a -> b) -> Sym (a :-> Full b)
+    -- Binary operator
+    Op   :: BinOp -> (a -> b -> c) -> Sym (a :-> b :-> Full c)
+    -- Type casting (ignored when generating code)
+    Cast :: (a -> b) -> Sym (a :-> Full b)
+    -- Conditional
+    Cond :: Sym (Bool :-> a :-> a :-> Full a)
+    -- Variable (only for compilation)
+    Var  :: String -> Sym (Full a)
+
+data T sig
+  where
+    T :: CType (DenResult sig) => { unT :: Sym sig } -> T sig
+
+-- | C expression
+newtype CExp a = CExp {unCExp :: ASTF T a}
+
+instance Syntactic (CExp a)
+  where
+    type Domain (CExp a)   = T
+    type Internal (CExp a) = a
+    desugar = unCExp
+    sugar   = CExp
+
+type instance VarPred CExp = CType
+
+evalSym :: Sym sig -> Denotation sig
+evalSym (Fun _ a) = a
+evalSym (UOp _ f) = f
+evalSym (Op  _ f) = f
+evalSym (Cast f)  = f
+evalSym Cond      = \c t f -> if c then t else f
+evalSym (Var v)   = error $ "evalCExp: cannot evaluate variable " ++ v
+
+-- | Evaluate an expression
+evalCExp :: CExp a -> a
+evalCExp (CExp e) = go e
+  where
+    go :: AST T sig -> Denotation sig
+    go (Sym (T s)) = evalSym s
+    go (f :$ a)    = go f $ go a
+
+instance EvalExp CExp
+  where
+    litExp a = CExp $ Sym $ T $ Fun (show a) a
+    evalExp  = evalCExp
+
+-- | Compile an expression
+compCExp :: forall m a . MonadC m => CExp a -> m Exp
+compCExp = simpleMatch (go . unT) . unCExp
+  where
+    compCExp' :: ASTF T b -> m Exp
+    compCExp' = compCExp . CExp
+
+    go :: Sym sig -> Args (AST T) sig -> m Exp
+    go (Var v) Nil = return [cexp| $id:v |]
+    go (Fun lit _) Nil = case lit of
+      "True"  -> addSystemInclude "stdbool.h" >> return [cexp| true |]
+      "False" -> addSystemInclude "stdbool.h" >> return [cexp| false |]
+      l       -> return [cexp| $id:l |]
+    go (Fun fun _) args = do
+      as <- sequence $ listArgs compCExp' args
+      return [cexp| $id:fun($args:as) |]
+    go (UOp op _) (a :* Nil) = do
+      a' <- compCExp' a
+      return $ UnOp op a' mempty
+    go (Op op _) (a :* b :* Nil) = do
+      a' <- compCExp' a
+      b' <- compCExp' b
+      return $ BinOp op a' b' mempty
+    go (Cast f) (a :* Nil) = do
+      a' <- compCExp' a
+      return [cexp| $a' |]
+    go Cond (c :* t :* f :* Nil) = do
+      c' <- compCExp' c
+      t' <- compCExp' t
+      f' <- compCExp' f
+      return $ C.Cond c' t' f' mempty
+
+instance CompExp CExp
+  where
+    varExp = CExp . Sym . T . Var . showVar
+      where showVar v = 'v' : show v
+    compExp  = compCExp
+    compType = cType
+
+-- | One-level constant folding: if all immediate sub-expressions are literals,
+-- the expression is reduced to a single literal
+constFold :: CExp a -> CExp a
+constFold = CExp . match go . unCExp
+  where
+    go :: T sig -> Args (AST T) sig -> AST T (Full (DenResult sig))
+    go (T s) as = res
+      where
+        e   = appArgs (Sym $ T s) as
+        res = if and $ listArgs (isJust . viewLit . CExp) as
+                then unCExp $ value $ evalCExp $ CExp e
+                else e
+  -- Deeper constant folding would require a way to witness `Show` for arbitrary
+  -- sub-expressions. This is certainly doable, but seems to complicate things
+  -- for not much gain (currently).
+
+-- | Get the value of a literal expression
+viewLit :: CExp a -> Maybe a
+viewLit (CExp (Sym (T (Fun _ a)))) = Just a
+viewLit _ = Nothing
+
+castAST :: forall a b . Typeable b => ASTF T a -> Maybe (ASTF T b)
+castAST a = simpleMatch go a
+  where
+    go :: (DenResult sig ~ a) => T sig -> Args (AST T) sig -> Maybe (ASTF T b)
+    go (T _) _ = gcast a
+
+
+
+--------------------------------------------------------------------------------
+-- * User interface
+--------------------------------------------------------------------------------
+
+-- | Create a named variable
+variable :: CType a => String -> CExp a
+variable = CExp . Sym . T . Var
+
+-- | Construct a literal expression
+value :: CType a => a -> CExp a
+value a = CExp $ Sym $ T $ Fun (show a) a
+
+true, false :: CExp Bool
+true  = value True
+false = value False
+
+instance (Num a, CType a) => Num (CExp a)
+  where
+    fromInteger = value . fromInteger
+
+    a + b
+      | Just 0 <- viewLit a, isExact a = b
+      | Just 0 <- viewLit b, isExact a = a
+      | otherwise = constFold $ sugarSym (T $ Op Add (+)) a b
+
+    a - b
+      | Just 0 <- viewLit a, isExact a = negate b
+      | Just 0 <- viewLit b, isExact a = a
+      | a == b,              isExact a = 0
+      | otherwise = constFold $ sugarSym (T $ Op Sub (-)) a b
+
+    a * b
+      | Just 0 <- viewLit a, isExact a = value 0
+      | Just 0 <- viewLit b, isExact a = value 0
+      | Just 1 <- viewLit a, isExact a = b
+      | Just 1 <- viewLit b, isExact a = a
+      | otherwise = constFold $ sugarSym (T $ Op Mul (*)) a b
+
+    negate a = constFold $ sugarSym (T $ UOp Negate negate) a
+
+    abs    = error "abs not implemented for CExp"
+    signum = error "signum not implemented for CExp"
+
+instance (Fractional a, CType a) => Fractional (CExp a)
+  where
+    fromRational = value . fromRational
+    a / b = constFold $ sugarSym (T $ Op Div (/)) a b
+
+    recip = error "recip not implemented for CExp"
+
+-- | Integer division truncated toward zero
+quot_ :: (Integral a, CType a) => CExp a -> CExp a -> CExp a
+quot_ a b
+    | Just 0 <- viewLit a = 0
+    | Just 1 <- viewLit b = a
+    | a == b              = 1
+    | otherwise           = constFold $ sugarSym (T $ Op Div quot) a b
+
+-- | Integer remainder satisfying
+--
+-- > (x `quot_` y)*y + (x #% y) == x
+(#%) :: (Integral a, CType a) => CExp a -> CExp a -> CExp a
+a #% b
+    | Just 0 <- viewLit a = 0
+    | Just 1 <- viewLit b = 0
+    | a == b              = 0
+    | otherwise           = constFold $ sugarSym (T $ Op Mod rem) a b
+
+-- | Integral type casting
+i2n :: (Integral a, Num b, CType b) => CExp a -> CExp b
+i2n a = constFold $ sugarSym (T $ Cast (fromInteger . toInteger)) a
+
+-- | Boolean negation
+not_ :: CExp Bool -> CExp Bool
+not_ (CExp (nt :$ a))
+    | Just (T (UOp Lnot _)) <- prj nt
+    , Just a' <- castAST a = CExp a'
+not_ a = constFold $ sugarSym (T $ UOp Lnot not) a
+
+-- | Equality
+(#==) :: (Eq a, CType a) => CExp a -> CExp a -> CExp Bool
+a #== b
+    | a == b, isExact a = true
+    | otherwise         = constFold $ sugarSym (T $ Op Eq (==)) a b
+
+-- | In-equality
+(#!=) :: (Eq a, CType a) => CExp a -> CExp a -> CExp Bool
+a #!= b
+    | a == b, isExact a = false
+    | otherwise         = constFold $ sugarSym (T $ Op Ne (/=)) a b
+
+(#<) :: (Ord a, CType a) => CExp a -> CExp a -> CExp Bool
+a #< b
+    | a == b, isExact a = false
+    | otherwise         = constFold $ sugarSym (T $ Op Lt (<)) a b
+
+(#>) :: (Ord a, CType a) => CExp a -> CExp a -> CExp Bool
+a #> b
+    | a == b, isExact a = false
+    | otherwise         = constFold $ sugarSym (T $ Op Gt (>)) a b
+
+(#<=) :: (Ord a, CType a) => CExp a -> CExp a -> CExp Bool
+a #<= b
+    | a == b, isExact a = true
+    | otherwise         = constFold $ sugarSym (T $ Op Le (<=)) a b
+
+(#>=) :: (Ord a, CType a) => CExp a -> CExp a -> CExp Bool
+a #>= b
+    | a == b, isExact a = true
+    | otherwise         = constFold $ sugarSym (T $ Op Ge (>=)) a b
+
+infix 4 #==, #!=, #<, #>, #<=, #>=
+
+-- | Conditional expression
+cond :: CType a
+    => CExp Bool  -- ^ Condition
+    -> CExp a     -- ^ True branch
+    -> CExp a     -- ^ False branch
+    -> CExp a
+cond c t f
+    | Just c' <- viewLit c = if c' then t else f
+    | t == f = t
+cond (CExp (nt :$ a)) t f
+    | Just (T (UOp Lnot _)) <- prj nt
+    , Just a' <- castAST a = cond (CExp a') f t
+cond c t f = constFold $ sugarSym (T Cond) c t f
+
+-- | Condition operator; use as follows:
+--
+-- > cond1 ? a $
+-- > cond2 ? b $
+-- > cond3 ? c $
+-- >         default
+(?) :: CType a
+    => CExp Bool  -- ^ Condition
+    -> CExp a     -- ^ True branch
+    -> CExp a     -- ^ False branch
+    -> CExp a
+(?) = cond
+
+infixl 1 ?
+
+
+
+--------------------------------------------------------------------------------
+-- Instances
+--------------------------------------------------------------------------------
+
+#if MIN_VERSION_syntactic(3,0,0)
+deriveSymbol ''Sym
+#endif
+
+#if MIN_VERSION_syntactic(3,0,0)
+instance Render Sym
+  where
+    renderSym (Fun name _) = name
+    renderSym (UOp op _)   = show op
+    renderSym (Op op _)    = show op
+    renderSym (Cast _)     = "cast"
+    renderSym (Var v)      = v
+    renderArgs = renderArgsSmart
+
+instance Equality Sym
+  where
+    equal = equalDefault
+    hash  = hashDefault
+
+instance StringTree Sym
+
+instance Symbol T where symSig (T s) = symSig s
+
+instance Render T
+  where
+    renderSym (T s)     = renderSym s
+    renderArgs as (T s) = renderArgs as s
+
+instance Equality T
+  where
+    equal (T s) (T t) = equal s t
+    hash (T s)        = hash s
+
+instance StringTree T
+  where
+    stringTreeSym as (T s) = stringTreeSym as s
+
+#else
+
+instance Semantic Sym
+  where
+    semantics (Fun name f) = Sem name f
+    semantics (UOp op f)   = Sem (show op) f
+    semantics (Op op f)    = Sem (show op) f
+    semantics (Cast f)     = Sem "cast" f
+    semantics (Var v)      = Sem v undefined
+
+instance Equality Sym
+  where
+    equal    = equalDefault
+    exprHash = exprHashDefault
+
+instance Semantic T
+  where
+    semantics (T s) = semantics s
+
+instance Equality T
+  where
+    equal (T s) (T t) = equal s t
+    exprHash (T s)    = exprHash s
+
+#endif
+
+deriving instance Eq (CExp a)
+  -- Must be placed here due to the sequential dependencies introduced by
+  -- Template Haskell
+
diff --git a/src/Language/Embedded/Concurrent.hs b/src/Language/Embedded/Concurrent.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Embedded/Concurrent.hs
@@ -0,0 +1,95 @@
+-- | Basic concurrency primitives.
+module Language.Embedded.Concurrent (
+    ThreadId (..),
+    ChanBound, Chan (..),
+    ThreadCMD,
+    ChanCMD,
+    Closeable, Uncloseable,
+    fork, forkWithId, asyncKillThread, killThread, waitThread,
+    newChan, newCloseableChan, readChan, writeChan,
+    closeChan, lastChanReadOK,
+  ) where
+
+import Control.Monad.Operational.Higher
+import Language.Embedded.Expression
+import Language.Embedded.Concurrent.CMD
+import Language.Embedded.Concurrent.Backend.C ()
+
+-- | Fork off a computation as a new thread.
+fork :: (ThreadCMD :<: instr)
+     => ProgramT instr m ()
+     -> ProgramT instr m ThreadId
+fork = forkWithId . const
+
+-- | Fork off a computation as a new thread, with access to its own thread ID.
+forkWithId :: (ThreadCMD :<: instr)
+           => (ThreadId -> ProgramT instr m ())
+           -> ProgramT instr m ThreadId
+forkWithId = singleton . inj . ForkWithId
+
+-- | Forcibly terminate a thread, then continue execution immediately.
+asyncKillThread :: (ThreadCMD :<: instr) => ThreadId -> ProgramT instr m ()
+asyncKillThread = singleton . inj . Kill
+
+-- | Forcibly terminate a thread. Blocks until the thread is actually dead.
+killThread :: (ThreadCMD :<: instr, Monad m) => ThreadId -> ProgramT instr m ()
+killThread t = do
+  singleton . inj $ Kill t
+  waitThread t
+
+-- | Wait for a thread to terminate.
+waitThread :: (ThreadCMD :<: instr) => ThreadId -> ProgramT instr m ()
+waitThread = singleton . inj . Wait
+
+-- | Create a new channel. Writing a reference type to a channel will copy the
+--   /reference/ into the queue, not its contents.
+--
+--   We'll likely want to change this, actually copying arrays and the like
+--   into the queue instead of sharing them across threads.
+newChan :: (VarPred (IExp instr) a, ChanCMD (IExp instr) :<: instr)
+        => IExp instr ChanBound
+        -> ProgramT instr m (Chan Uncloseable a)
+newChan = singleE . NewChan
+
+newCloseableChan :: (VarPred (IExp instr) a, ChanCMD (IExp instr) :<: instr)
+        => IExp instr ChanBound
+        -> ProgramT instr m (Chan Closeable a)
+newCloseableChan = singleE . NewChan
+
+-- | Read an element from a channel. If channel is empty, blocks until there
+--   is an item available.
+--   If 'closeChan' has been called on the channel *and* if the channel is
+--   empty, @readChan@ returns an undefined value immediately.
+readChan :: (VarPred (IExp instr) a, ChanCMD (IExp instr) :<: instr)
+         => Chan t a
+         -> ProgramT instr m (IExp instr a)
+readChan = singleE . ReadChan
+
+-- | Write a data element to a channel.
+--   If 'closeChan' has been called on the channel, all calls to @writeChan@
+--   become non-blocking no-ops and return @False@, otherwise returns @True@.
+writeChan :: (VarPred (IExp instr) a,
+              VarPred (IExp instr) Bool,
+              ChanCMD (IExp instr) :<: instr)
+        => Chan t a
+        -> IExp instr a
+        -> ProgramT instr m (IExp instr Bool)
+writeChan c = singleE . WriteChan c
+
+-- | When 'readChan' was last called on the given channel, did the read
+--   succeed?
+--   Always returns @True@ unless 'closeChan' has been called on the channel.
+--   Always returns @True@ if the channel has never been read.
+lastChanReadOK :: (VarPred (IExp instr) Bool, ChanCMD (IExp instr) :<: instr)
+               => Chan Closeable a
+               -> ProgramT instr m (IExp instr Bool)
+lastChanReadOK = singleE . ReadOK
+
+-- | Close a channel. All subsequent write operations will be no-ops.
+--   After the channel is drained, all subsequent read operations will be
+--   no-ops as well.
+closeChan :: (ChanCMD (IExp instr) :<: instr)
+          => Chan Closeable a
+          -> ProgramT instr m ()
+closeChan = singleE . CloseChan
+
diff --git a/src/Language/Embedded/Concurrent/Backend/C.hs b/src/Language/Embedded/Concurrent/Backend/C.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Embedded/Concurrent/Backend/C.hs
@@ -0,0 +1,87 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE QuasiQuotes #-}
+
+module Language.Embedded.Concurrent.Backend.C where
+
+
+
+#if __GLASGOW_HASKELL__ < 710
+import Control.Applicative
+#endif
+import Control.Monad.Operational.Higher
+import Data.Proxy
+import Language.Embedded.Expression
+import Language.Embedded.Concurrent.CMD
+import Language.C.Quote.C
+import Language.C.Monad
+import qualified Language.C.Syntax as C
+
+
+
+instance ToIdent ThreadId where
+  toIdent (TIDComp tid) = C.Id $ "t" ++ show tid
+
+instance ToIdent (Chan t a) where
+  toIdent (ChanComp c) = C.Id $ "chan" ++ show c
+
+threadFun :: ThreadId -> String
+threadFun tid = "thread_" ++ show tid
+
+-- | Compile `ThreadCMD`.
+--   TODO: sharing for threads with the same body
+compThreadCMD :: ThreadCMD CGen a -> CGen a
+compThreadCMD (ForkWithId body) = do
+  tid <- TIDComp <$> freshId
+  let funName = threadFun tid
+  _ <- inFunctionTy [cty|void*|] funName $ do
+    addParam [cparam| void* unused |]
+    body tid
+    addStm [cstm| return NULL; |]
+  addSystemInclude "pthread.h"
+  touchVar tid
+  addLocal [cdecl| typename pthread_t $id:tid; |]
+  addStm [cstm| pthread_create(&$id:tid, NULL, $id:funName, NULL); |]
+  return tid
+compThreadCMD (Kill tid) = do
+  touchVar tid
+  addStm [cstm| pthread_cancel($id:tid); |]
+compThreadCMD (Wait tid) = do
+  touchVar tid
+  addStm [cstm| pthread_join($id:tid, NULL); |]
+
+-- | Compile `ChanCMD`.
+compChanCMD :: forall exp prog a. CompExp exp
+            => ChanCMD exp prog a
+            -> CGen a
+compChanCMD cmd@(NewChan sz) = do
+  addLocalInclude "chan.h"
+  t <- compTypePP2 (Proxy :: Proxy exp) cmd
+  sz' <- compExp sz
+  c <- ChanComp <$> freshId
+  addGlobal [cedecl| typename chan_t $id:c; |]
+  addStm [cstm| $id:c = chan_new(sizeof($ty:t), $sz'); |]
+  return c
+compChanCMD (WriteChan c x) = do
+  x' <- compExp x
+  (v,name) <- freshVar
+  (ok,okname) <- freshVar
+  let _ = v `asTypeOf` x
+  addStm [cstm| $id:name = $x'; |]
+  addStm [cstm| $id:okname = chan_write($id:c, &$id:name); |]
+  return ok
+compChanCMD (ReadChan c) = do
+  (var,name) <- freshVar
+  addStm [cstm| chan_read($id:c, &$id:name); |]
+  return var
+compChanCMD (CloseChan c) = do
+  addStm [cstm| chan_close($id:c); |]
+compChanCMD (ReadOK c) = do
+  (var,name) <- freshVar
+  addStm [cstm| $id:name = chan_last_read_ok($id:c); |]
+  return var
+
+instance Interp ThreadCMD CGen where
+  interp = compThreadCMD
+instance CompExp exp => Interp (ChanCMD exp) CGen where
+  interp = compChanCMD
+
diff --git a/src/Language/Embedded/Concurrent/CMD.hs b/src/Language/Embedded/Concurrent/CMD.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Embedded/Concurrent/CMD.hs
@@ -0,0 +1,153 @@
+{-# LANGUAGE CPP #-}
+
+module Language.Embedded.Concurrent.CMD (
+    TID, ThreadId (..),
+    CID, ChanBound, Chan (..),
+    ThreadCMD (..),
+    ChanCMD (..),
+    Closeable, Uncloseable
+  ) where
+
+
+
+#if __GLASGOW_HASKELL__ < 710
+import Control.Applicative
+#endif
+import Control.Monad
+import Control.Monad.Operational.Higher
+import Data.IORef
+import Data.Typeable
+import Language.Embedded.Expression
+import qualified Control.Concurrent as CC
+import qualified Control.Concurrent.BoundedChan as Bounded
+import Data.Word (Word16)
+
+
+
+-- | Maximum number of elements in some bounded channel.
+type ChanBound = Word16
+
+type TID = VarId
+type CID = VarId
+
+-- | A "flag" which may be waited upon. A flag starts of unset, and can be set
+--   using 'setFlag'. Once set, the flag stays set forever.
+data Flag a = Flag (IORef Bool) (CC.MVar a)
+
+-- | Create a new, unset 'Flag'.
+newFlag :: IO (Flag a)
+newFlag = Flag <$> newIORef False <*> CC.newEmptyMVar
+
+-- | Set a 'Flag'; guaranteed not to block.
+--   If @setFlag@ is called on a flag which was already set, the value of said
+--   flag is not updated.
+--   @setFlag@ returns the status of the flag prior to the call: is the flag
+--   was already set the return value is @True@, otherwise it is @False@.
+setFlag :: Flag a -> a -> IO Bool
+setFlag (Flag flag var) val = do
+  set <- atomicModifyIORef flag $ \set -> (True, set)
+  when (not set) $ CC.putMVar var val
+  return set
+
+-- | Wait until the given flag becomes set, then return its value. If the flag
+--   is already set, return the value immediately.
+waitFlag :: Flag a -> IO a
+waitFlag (Flag _ var) = CC.withMVar var return
+
+data ThreadId
+  = TIDEval CC.ThreadId (Flag ())
+  | TIDComp TID
+    deriving (Typeable)
+
+instance Show ThreadId where
+  show (TIDEval tid _) = show tid
+  show (TIDComp tid)   = show tid
+
+data Closeable
+data Uncloseable
+
+-- | A bounded channel.
+data Chan t a
+  = ChanEval (Bounded.BoundedChan a) (IORef Bool) (IORef Bool)
+  | ChanComp CID
+
+data ThreadCMD (prog :: * -> *) a where
+  ForkWithId :: (ThreadId -> prog ()) -> ThreadCMD prog ThreadId
+  Kill       :: ThreadId -> ThreadCMD prog ()
+  Wait       :: ThreadId -> ThreadCMD prog ()
+
+data ChanCMD exp (prog :: * -> *) a where
+  NewChan   :: VarPred exp a => exp ChanBound -> ChanCMD exp prog (Chan t a)
+  ReadChan  :: VarPred exp a => Chan t a -> ChanCMD exp prog (exp a)
+  WriteChan :: (VarPred exp a, VarPred exp Bool)
+            => Chan t a -> exp a -> ChanCMD exp prog (exp Bool)
+  CloseChan :: Chan Closeable a -> ChanCMD exp prog ()
+  ReadOK    :: VarPred exp Bool
+            => Chan Closeable a -> ChanCMD exp prog (exp Bool)
+
+instance HFunctor ThreadCMD where
+  hfmap f (ForkWithId p) = ForkWithId $ f . p
+  hfmap _ (Kill tid)     = Kill tid
+  hfmap _ (Wait tid)     = Wait tid
+
+instance HFunctor (ChanCMD exp) where
+  hfmap _ (NewChan sz)    = NewChan sz
+  hfmap _ (ReadChan c)    = ReadChan c
+  hfmap _ (WriteChan c x) = WriteChan c x
+  hfmap _ (CloseChan c)   = CloseChan c
+  hfmap _ (ReadOK c)      = ReadOK c
+
+type instance IExp (ThreadCMD :+: i) = IExp i
+
+type instance IExp (ChanCMD e)       = e
+type instance IExp (ChanCMD e :+: i) = e
+
+runThreadCMD :: ThreadCMD IO a
+             -> IO a
+runThreadCMD (ForkWithId p) = do
+  f <- newFlag
+  tidvar <- CC.newEmptyMVar
+  cctid <- CC.forkIO . void $ CC.takeMVar tidvar >>= p >> setFlag f ()
+  let tid = TIDEval cctid f
+  CC.putMVar tidvar tid
+  return tid
+runThreadCMD (Kill (TIDEval t f)) = do
+  setFlag f ()
+  CC.killThread t
+  return ()
+runThreadCMD (Wait (TIDEval _ f)) = do
+  waitFlag f
+
+runChanCMD :: forall exp a. EvalExp exp
+           => ChanCMD exp IO a -> IO a
+runChanCMD (NewChan sz) =
+  ChanEval <$> Bounded.newBoundedChan (fromIntegral $ evalExp sz)
+           <*> newIORef False
+           <*> newIORef True
+runChanCMD (ReadChan (ChanEval c closedref lastread)) = do
+  closed <- readIORef closedref
+  mval <- Bounded.tryReadChan c
+  case mval of
+    Just x -> do
+        return $ litExp x
+    Nothing
+      | closed -> do
+        writeIORef lastread False
+        return undefined
+      | otherwise -> do
+        litExp <$> Bounded.readChan c
+runChanCMD (WriteChan (ChanEval c closedref _) x) = do
+  closed <- readIORef closedref
+  if closed
+    then return (litExp False)
+    else Bounded.writeChan c (evalExp x) >> return (litExp True)
+runChanCMD (CloseChan (ChanEval _ closedref _)) = do
+  writeIORef closedref True
+runChanCMD (ReadOK (ChanEval _ _ lastread)) = do
+  litExp <$> readIORef lastread
+
+instance Interp ThreadCMD IO where
+  interp = runThreadCMD
+instance EvalExp exp => Interp (ChanCMD exp) IO where
+  interp = runChanCMD
+
diff --git a/src/Language/Embedded/Expression.hs b/src/Language/Embedded/Expression.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Embedded/Expression.hs
@@ -0,0 +1,93 @@
+{-# LANGUAGE QuasiQuotes #-}
+
+-- | Interface for evaluation and compilation of pure expressions
+module Language.Embedded.Expression
+  ( VarId
+  , VarPred
+  , EvalExp(..)
+  , CompExp(..)
+  , freshVar
+  , freshVar_
+  )
+  where
+
+import Data.Proxy
+import Data.Constraint
+import Language.C.Monad
+import Language.C.Quote.C
+import Language.C.Syntax (Exp,Type)
+import qualified Language.C.Syntax as C
+
+
+
+-- | Constraint on the types of variables in a given expression language
+type family VarPred (exp :: * -> *) :: * -> Constraint
+
+-- | General interface for evaluating expressions
+class EvalExp exp
+  where
+    -- | Literal expressions
+    litExp  :: VarPred exp a => a -> exp a
+
+    -- | Evaluation of (closed) expressions
+    evalExp :: exp a -> a
+
+-- | General interface for compiling expressions
+class CompExp exp where
+    -- | Variable expressions
+    varExp  :: VarPred exp a => VarId -> exp a
+
+    -- | Compilation of expressions
+    --
+    -- /NOTE: It is assumed that free variables in the expression are rendered as @vIII@, where/
+    -- /      @III@ is the variable identifier./
+    compExp :: (MonadC m) => exp a -> m Exp
+
+    -- | Extract expression type
+    compType :: forall m a
+             .  (MonadC m, VarPred exp a)
+             => exp a -> m Type
+    compType _ = compTypeP (Proxy :: Proxy (exp a))
+    {-# INLINE compType #-}
+
+    -- | Extract expression type
+    compTypeP :: forall proxy m a
+              .  (MonadC m, VarPred exp a)
+              => proxy (exp a) -> m Type
+    compTypeP _ = compTypePP (Proxy :: Proxy exp) (Proxy :: Proxy a)
+    {-# INLINE compTypeP #-}
+
+    -- | Extract expression type
+    compTypePP :: forall proxy1 proxy2 m a
+               .  (MonadC m, VarPred exp a)
+               => proxy1 exp -> proxy2 a -> m Type
+    compTypePP _ _ = compTypePP2 (Proxy :: Proxy exp) (Proxy :: Proxy (Proxy a))
+    {-# INLINE compTypePP #-}
+
+    -- | Extract expression type
+    compTypePP2 :: forall proxy proxy1 proxy2 m a
+                .  (MonadC m, VarPred exp a)
+                => proxy exp -> proxy1 (proxy2 a) -> m Type
+    compTypePP2 _ _ = compType (undefined :: exp a)
+    {-# INLINE compTypePP2 #-}
+
+    {-# MINIMAL varExp , compExp , (compType | compTypeP | compTypePP | compTypePP2 ) #-}
+
+-- | Variable identifier
+type VarId = Integer
+
+-- | Create and declare a fresh variable and return its name
+freshVar :: forall exp m a. (CompExp exp, VarPred exp a, MonadC m) => m (exp a, C.Id)
+freshVar = do
+    v <- fmap varExp freshId
+    t <- compTypeP (Proxy :: Proxy (exp a))
+    C.Var n _ <- compExp v
+    touchVar n
+    case t of
+      C.Type _ C.Ptr{} _ -> addLocal [cdecl| $ty:t $id:n = NULL; |]
+      _                  -> addLocal [cdecl| $ty:t $id:n; |]
+    return (v,n)
+
+-- | Create and declare a fresh variable
+freshVar_ :: forall exp m a. (CompExp exp, VarPred exp a, MonadC m) => m (exp a)
+freshVar_ = fst `fmap` freshVar
diff --git a/src/Language/Embedded/Imperative.hs b/src/Language/Embedded/Imperative.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Embedded/Imperative.hs
@@ -0,0 +1,60 @@
+-- | Deep embedding of imperative programs with code generation. This is the
+-- main module for users who want to write imperative programs.
+--
+-- The 'Program' type is parameterized by an instruction set that can be
+-- combined in a modular way; e.g:
+--
+-- @
+-- type MyProg exp a = `Program` (`RefCMD` exp `:+:` `FileCMD` exp) a
+-- @
+--
+-- Also, instructions are parameterized on the expression language. In the above
+-- example, @exp@ can be any type (of kind @* -> *@) that implements the
+-- 'EvalExp' and 'CompExp' classes.
+--
+-- Some examples of using the library are found in the @examples@ directory.
+
+module Language.Embedded.Imperative
+  ( module Control.Monad
+  , module Data.Int
+  , module Data.Word
+    -- * Program monad
+  , ProgramT
+  , Program
+  , interpretT
+  , interpret
+    -- * Imperative instructions
+  , RefCMD
+  , ArrCMD
+  , ControlCMD
+  , FileCMD
+  , CallCMD
+    -- * Types of Printf arguments
+  , PrintfArg
+    -- * Composing instruction sets
+  , (:+:)
+  , (:<:)
+  , IExp
+    -- * Interpreting expressions
+  , VarPred
+  , EvalExp
+  , CompExp
+    -- * Front end
+  , module Language.Embedded.Imperative.Frontend.General
+  , module Language.Embedded.Imperative.Frontend
+  ) where
+
+
+
+import Control.Monad
+import Data.Int
+import Data.Word
+
+import Control.Monad.Operational.Higher
+
+import Language.Embedded.Expression
+import Language.Embedded.Imperative.CMD
+import Language.Embedded.Imperative.Frontend.General
+import Language.Embedded.Imperative.Frontend
+import Language.Embedded.Imperative.Backend.C ()
+
diff --git a/src/Language/Embedded/Imperative/Args.hs b/src/Language/Embedded/Imperative/Args.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Embedded/Imperative/Args.hs
@@ -0,0 +1,100 @@
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE PolyKinds   #-}
+
+-- | Various types of function arguments
+
+module Language.Embedded.Imperative.Args where
+
+import Control.Monad
+import Data.Proxy
+import Language.C.Quote.C
+import Language.C.Syntax
+import Language.Embedded.Expression
+import Language.Embedded.Imperative.CMD
+import Language.Embedded.Backend.C
+
+-- | Value argument
+data ValArg exp where
+  ValArg :: VarPred exp a => exp a -> ValArg exp
+
+instance Arg ValArg where
+  mkArg   (ValArg a) = compExp a
+  mkParam (ValArg a) = do
+    t <- compType a
+    return [cparam| $ty:t |]
+
+  mapArg predCast f (ValArg (a :: exp a)) =
+    predCast (Proxy :: Proxy a) $ ValArg (f a)
+
+  mapMArg predCast f (ValArg (a :: exp a)) =
+    predCast (Proxy :: Proxy a) $ liftM ValArg (f a)
+
+-- | Reference argument
+data RefArg exp where
+  RefArg :: VarPred exp a => Ref a -> RefArg exp
+
+instance Arg RefArg where
+  mkArg   (RefArg r) = return [cexp| &$id:r |]
+  mkParam (RefArg (r :: Ref a) :: RefArg exp) = do
+    t <- compTypeP (Proxy :: Proxy (exp a))
+    return [cparam| $ty:t* |]
+
+  mapArg predCast _ (RefArg (r :: Ref a)) =
+    predCast (Proxy :: Proxy a) $ RefArg r
+
+  mapMArg predCast _ (RefArg (r :: Ref a)) =
+    predCast (Proxy :: Proxy a) $ return $ RefArg r
+
+-- | Array argument
+data ArrArg exp where
+  ArrArg :: VarPred exp a => Arr n a -> ArrArg exp
+
+instance Arg ArrArg where
+  mkArg   (ArrArg a) = return [cexp| $id:a |]
+  mkParam (ArrArg (a :: Arr n a) :: ArrArg exp) = do
+    t <- compTypeP (Proxy :: Proxy (exp a))
+    return [cparam| $ty:t* |]
+
+  mapArg predCast _ (ArrArg (a :: Arr n a)) =
+    predCast (Proxy :: Proxy a) $ ArrArg a
+
+  mapMArg predCast _ (ArrArg (a :: Arr n a)) =
+    predCast (Proxy :: Proxy a) $ return $ ArrArg a
+
+-- | Abstract object argument
+data ObjArg exp where
+  ObjArg :: Object -> ObjArg exp
+
+instance Arg ObjArg where
+  mkArg   (ObjArg o) = return [cexp| $id:o |]
+  mkParam (ObjArg (Object True t _))  = let t' = namedType t in return [cparam| $ty:t'* |]
+  mkParam (ObjArg (Object False t _)) = let t' = namedType t in return [cparam| $ty:t' |]
+  mapArg  _ _ (ObjArg o) = ObjArg o
+  mapMArg _ _ (ObjArg o) = return $ ObjArg o
+
+
+-- | Constant string argument
+data StrArg exp where
+  StrArg :: String -> StrArg exp
+
+instance Arg StrArg where
+  mkArg   (StrArg s) = return [cexp| $string:s |]
+  mkParam (StrArg s) = return [cparam| const char* |]
+  mapArg  _ _ (StrArg s) = StrArg s
+  mapMArg _ _ (StrArg s) = return $ StrArg s
+
+-- | Modifier that takes the address of another argument
+newtype Addr arg exp = Addr (arg exp)
+
+instance Arg arg => Arg (Addr arg) where
+  mkArg (Addr arg) = do
+    e <- mkArg arg
+    return [cexp| &$e |]
+  mkParam (Addr arg) = do
+    p <- mkParam arg
+    case p of
+       Param mid spec decl loc -> return $ Param mid spec (Ptr [] decl loc) loc
+       _ -> error "Cannot deal with antiquotes"
+  mapArg  predCast f (Addr arg) = Addr (mapArg predCast f arg)
+  mapMArg predCast f (Addr arg) = liftM Addr (mapMArg predCast f arg)
+
diff --git a/src/Language/Embedded/Imperative/Backend/C.hs b/src/Language/Embedded/Imperative/Backend/C.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Embedded/Imperative/Backend/C.hs
@@ -0,0 +1,200 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE QuasiQuotes #-}
+
+-- | C code generation for imperative commands
+
+module Language.Embedded.Imperative.Backend.C where
+
+
+
+#if __GLASGOW_HASKELL__ < 710
+import Control.Applicative
+#endif
+import Control.Monad.State
+import Data.Proxy
+
+import Language.C.Quote.C
+import qualified Language.C.Syntax as C
+
+import Control.Monad.Operational.Higher
+import Language.C.Monad
+import Language.Embedded.Expression
+import Language.Embedded.Imperative.CMD
+import Language.Embedded.Imperative.Frontend.General
+import Language.Embedded.Backend.C
+
+-- | Compile `RefCMD`
+compRefCMD :: forall exp prog a. CompExp exp
+           => RefCMD exp prog a -> CGen a
+compRefCMD cmd@NewRef = do
+    t <- compTypePP2 (Proxy :: Proxy exp) cmd
+    r <- RefComp <$> freshId
+    case t of
+      C.Type _ C.Ptr{} _ -> addLocal [cdecl| $ty:t $id:r = NULL; |]
+      _                  -> addLocal [cdecl| $ty:t $id:r; |]
+    return r
+compRefCMD (InitRef exp) = do
+    t <- compType exp
+    r <- RefComp <$> freshId
+    v <- compExp exp
+    addLocal [cdecl| $ty:t $id:r; |]
+    addStm   [cstm| $id:r = $v; |]
+    return r
+compRefCMD (GetRef ref) = do
+    (v,_) <- freshVar
+    e <- compExp v
+    touchVar ref
+    addStm [cstm| $e = $id:ref; |]
+    return v
+compRefCMD (SetRef ref exp) = do
+    v <- compExp exp
+    touchVar ref
+    addStm [cstm| $id:ref = $v; |]
+
+-- | Compile `ArrCMD`
+compArrCMD :: forall exp prog a. CompExp exp
+           => ArrCMD exp prog a -> CGen a
+compArrCMD cmd@(NewArr size) = do
+    sym <- gensym "a"
+    v   <- compExp size
+    t   <- compTypePP2 (Proxy :: Proxy exp) cmd
+    addLocal [cdecl| $ty:t $id:sym[ $v ]; |]
+    return $ ArrComp sym
+compArrCMD cmd@(NewArr_) = do
+    sym <- gensym "a"
+    t   <- compTypePP2 (Proxy :: Proxy exp) cmd
+    addLocal [cdecl| $ty:t * $id:sym; |]
+    return $ ArrComp sym
+compArrCMD (GetArr expi arr) = do
+    (v,n) <- freshVar
+    i     <- compExp expi
+    touchVar arr
+    addStm [cstm| $id:n = $id:arr[ $i ]; |]
+    return v
+compArrCMD (SetArr expi expv arr) = do
+    v <- compExp expv
+    i <- compExp expi
+    touchVar arr
+    addStm [cstm| $id:arr[ $i ] = $v; |]
+
+-- | Compile `ControlCMD`
+compControlCMD :: CompExp exp => ControlCMD exp CGen a -> CGen a
+compControlCMD (If c t f) = do
+    cc <- compExp c
+    ct <- inNewBlock_ t
+    cf <- inNewBlock_ f
+    case (ct, cf) of
+      ([],[]) -> return ()
+      (_ ,[]) -> addStm [cstm| if (   $cc) {$items:ct} |]
+      ([],_ ) -> addStm [cstm| if ( ! $cc) {$items:cf} |]
+      (_ ,_ ) -> addStm [cstm| if (   $cc) {$items:ct} else {$items:cf} |]
+compControlCMD (While cont body) = do
+    s <- get
+    noop <- do
+        conte <- cont
+        contc <- compExp conte
+        case contc of
+          C.Var (C.Id "false"  _) _ -> return True
+          _ -> return False
+    put s
+    bodyc <- inNewBlock_ $ do
+        conte <- cont
+        contc <- compExp conte
+        case contc of
+          C.Var (C.Id "true"  _) _ -> return ()
+          _ -> case viewNotExp contc of
+              Just a -> addStm [cstm| if ($a) {break;} |]
+              _      -> addStm [cstm| if (! $contc) {break;} |]
+        body
+    when (not noop) $ addStm [cstm| while (1) {$items:bodyc} |]
+compControlCMD (For lo hi body) = do
+    loe   <- compExp lo
+    hie   <- compExp hi
+    (i,n) <- freshVar
+    bodyc <- inNewBlock_ (body i)
+    addStm [cstm| for ($id:n=$loe; $id:n<=$hie; $id:n++) {$items:bodyc} |]
+compControlCMD Break = addStm [cstm| break; |]
+
+compIOMode :: IOMode -> String
+compIOMode ReadMode      = "r"
+compIOMode WriteMode     = "w"
+compIOMode AppendMode    = "a"
+compIOMode ReadWriteMode = "r+"
+
+-- | Compile `FileCMD`
+compFileCMD :: CompExp exp => FileCMD exp CGen a -> CGen a
+compFileCMD (FOpen path mode) = do
+    addInclude "<stdio.h>"
+    addInclude "<stdlib.h>"
+    sym <- gensym "v"
+    addLocal [cdecl| typename FILE * $id:sym; |]
+    addStm   [cstm| $id:sym = fopen($id:path',$string:mode'); |]
+    return $ HandleComp sym
+  where
+    path' = show path
+    mode' = compIOMode mode
+compFileCMD (FClose h) = do
+    touchVar h
+    addStm [cstm| fclose($id:h); |]
+compFileCMD (FPrintf h form as) = do
+    addInclude "<stdio.h>"
+    touchVar h
+    let h'     = [cexp| $id:h |]
+        form'  = show form
+        form'' = [cexp| $id:form' |]
+    as' <- fmap ([h',form'']++) $ sequence [compExp a | PrintfArg a <- as]
+    addStm [cstm| fprintf($args:as'); |]
+compFileCMD cmd@(FGet h) = do
+    (v,n) <- freshVar
+    touchVar h
+    let mkProxy = (\_ -> Proxy) :: FileCMD exp prog (exp a) -> Proxy a
+        form    = formatSpecifier (mkProxy cmd)
+    addStm [cstm| fscanf($id:h, $string:form, &$id:n); |]
+    return v
+compFileCMD (FEof h) = do
+    addInclude "<stdbool.h>"
+    (v,n) <- freshVar
+    touchVar h
+    addStm [cstm| $id:n = feof($id:h); |]
+    return v
+
+compObjectCMD :: CompExp exp => ObjectCMD exp CGen a -> CGen a
+compObjectCMD (NewObject t) = do
+    sym <- gensym "obj"
+    let t' = namedType t
+    addLocal [cdecl| $ty:t' * $id:sym; |]
+    return $ Object True t sym
+compObjectCMD (InitObject fun pnt t args) = do
+    sym <- gensym "obj"
+    let t' = namedType t
+    as  <- mapM mkArg args
+    addLocal [cdecl| $ty:t' * $id:sym; |]
+    addStm   [cstm|  $id:sym = $id:fun($args:as); |]
+    return $ Object pnt t sym
+
+compCallCMD :: CompExp exp => CallCMD exp CGen a -> CGen a
+compCallCMD (AddInclude inc)    = addInclude inc
+compCallCMD (AddDefinition def) = addGlobal def
+compCallCMD (AddExternFun fun res args) = do
+    tres  <- compTypeP res
+    targs <- mapM mkParam args
+    addGlobal [cedecl| extern $ty:tres $id:fun($params:targs); |]
+compCallCMD (AddExternProc proc args) = do
+    targs <- mapM mkParam args
+    addGlobal [cedecl| extern void $id:proc($params:targs); |]
+compCallCMD (CallFun fun as) = do
+    as'   <- mapM mkArg as
+    (v,n) <- freshVar
+    addStm [cstm| $id:n = $id:fun($args:as'); |]
+    return v
+compCallCMD (CallProc fun as) = do
+    as' <- mapM mkArg as
+    addStm [cstm| $id:fun($args:as'); |]
+
+instance CompExp exp => Interp (RefCMD exp)     CGen where interp = compRefCMD
+instance CompExp exp => Interp (ArrCMD exp)     CGen where interp = compArrCMD
+instance CompExp exp => Interp (ControlCMD exp) CGen where interp = compControlCMD
+instance CompExp exp => Interp (FileCMD exp)    CGen where interp = compFileCMD
+instance CompExp exp => Interp (ObjectCMD exp)  CGen where interp = compObjectCMD
+instance CompExp exp => Interp (CallCMD exp)    CGen where interp = compCallCMD
+
diff --git a/src/Language/Embedded/Imperative/CMD.hs b/src/Language/Embedded/Imperative/CMD.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Embedded/Imperative/CMD.hs
@@ -0,0 +1,457 @@
+{-# LANGUAGE CPP #-}
+
+-- | Imperative commands. These commands can be used with the 'Program' monad,
+-- and different command types can be combined using (':+:').
+--
+-- These commands are general imperative constructs independent of the back end,
+-- except for 'CallCMD' which is C-specific.
+
+module Language.Embedded.Imperative.CMD
+  ( -- * References
+    Ref (..)
+  , RefCMD (..)
+    -- * Arrays
+  , Arr (..)
+  , ArrCMD (..)
+    -- * Control flow
+  , ControlCMD (..)
+    -- * File handling
+  , Handle (..)
+  , stdin
+  , stdout
+  , Formattable (..)
+  , FileCMD (..)
+  , PrintfArg (..)
+    -- * Abstract objects
+  , Object (..)
+  , ObjectCMD (..)
+    -- * External function calls (C-specific)
+  , FunArg (..)
+  , VarPredCast
+  , Arg (..)
+  , CallCMD (..)
+  ) where
+
+
+
+import Data.Array.IO
+import Data.Char (isSpace)
+import Data.Int
+import Data.IORef
+import Data.Typeable
+import Data.Word
+import System.IO (IOMode (..))
+import qualified System.IO as IO
+import qualified Text.Printf as Printf
+
+#if __GLASGOW_HASKELL__ < 708
+import Data.Proxy
+#endif
+
+import Control.Monad.Operational.Higher
+
+import Control.Monads
+import Language.Embedded.Expression
+import Language.Embedded.Traversal
+import qualified Language.C.Syntax as C
+import Language.C.Quote.C (ToIdent (..))
+import Language.C.Monad
+
+
+--------------------------------------------------------------------------------
+-- * References
+--------------------------------------------------------------------------------
+
+-- | Mutable reference
+data Ref a
+    = RefComp VarId
+    | RefEval (IORef a)
+  deriving Typeable
+
+-- | Identifiers from references
+instance ToIdent (Ref a)
+  where
+    toIdent (RefComp r) = C.Id ('v' : show r)
+
+-- | Commands for mutable references
+data RefCMD exp (prog :: * -> *) a
+  where
+    NewRef  :: VarPred exp a => RefCMD exp prog (Ref a)
+    InitRef :: VarPred exp a => exp a -> RefCMD exp prog (Ref a)
+    GetRef  :: VarPred exp a => Ref a -> RefCMD exp prog (exp a)
+    SetRef  :: VarPred exp a => Ref a -> exp a -> RefCMD exp prog ()
+      -- `VarPred` for `SetRef` is not needed for code generation, but it can be useful when
+      -- interpreting with a dynamically typed store. `VarPred` can then be used to supply a
+      -- `Typeable` dictionary for casting.
+#if  __GLASGOW_HASKELL__>=708
+  deriving Typeable
+#endif
+
+instance HFunctor (RefCMD exp)
+  where
+    hfmap _ NewRef       = NewRef
+    hfmap _ (InitRef a)  = InitRef a
+    hfmap _ (GetRef r)   = GetRef r
+    hfmap _ (SetRef r a) = SetRef r a
+
+instance CompExp exp => DryInterp (RefCMD exp)
+  where
+    dryInterp NewRef       = liftM RefComp fresh
+    dryInterp (InitRef _)  = liftM RefComp fresh
+    dryInterp (GetRef _)   = liftM varExp fresh
+    dryInterp (SetRef _ _) = return ()
+
+type instance IExp (RefCMD e)       = e
+type instance IExp (RefCMD e :+: i) = e
+
+
+
+--------------------------------------------------------------------------------
+-- * Arrays
+--------------------------------------------------------------------------------
+
+-- | Mutable array
+data Arr n a
+    = ArrComp String
+    | ArrEval (IOArray n a)
+  deriving Typeable
+
+-- | Identifiers from arrays
+instance ToIdent (Arr i a)
+  where
+    toIdent (ArrComp arr) = C.Id arr
+
+-- | Commands for mutable arrays
+data ArrCMD exp (prog :: * -> *) a
+  where
+    NewArr :: (VarPred exp a, VarPred exp n, Integral n, Ix n) => exp n -> ArrCMD exp prog (Arr n a)
+    NewArr_ :: (VarPred exp a, VarPred exp n, Integral n, Ix n) => ArrCMD exp prog (Arr n a)
+    GetArr :: (VarPred exp a, Integral n, Ix n)                => exp n -> Arr n a -> ArrCMD exp prog (exp a)
+    SetArr :: (Integral n, Ix n)                               => exp n -> exp a -> Arr n a -> ArrCMD exp prog ()
+#if  __GLASGOW_HASKELL__>=708
+  deriving Typeable
+#endif
+
+instance HFunctor (ArrCMD exp)
+  where
+    hfmap _ (NewArr n)       = NewArr n
+    hfmap _ (NewArr_)        = NewArr_
+    hfmap _ (GetArr i arr)   = GetArr i arr
+    hfmap _ (SetArr i a arr) = SetArr i a arr
+
+instance CompExp exp => DryInterp (ArrCMD exp)
+  where
+    dryInterp (NewArr _)   = liftM ArrComp $ freshStr "a"
+    dryInterp (NewArr_)      = liftM ArrComp $ freshStr "a"
+    dryInterp (GetArr _ _)   = liftM varExp fresh
+    dryInterp (SetArr _ _ _) = return ()
+
+type instance IExp (ArrCMD e)       = e
+type instance IExp (ArrCMD e :+: i) = e
+
+
+
+--------------------------------------------------------------------------------
+-- * Control flow
+--------------------------------------------------------------------------------
+
+data ControlCMD exp prog a
+  where
+    If    :: exp Bool -> prog () -> prog () -> ControlCMD exp prog ()
+    While :: prog (exp Bool) -> prog () -> ControlCMD exp prog ()
+    For   :: (VarPred exp n, Integral n) =>
+             exp n -> exp n -> (exp n -> prog ()) -> ControlCMD exp prog ()
+    Break :: ControlCMD exp prog ()
+
+instance HFunctor (ControlCMD exp)
+  where
+    hfmap g (If c t f)        = If c (g t) (g f)
+    hfmap g (While cont body) = While (g cont) (g body)
+    hfmap g (For lo hi body)  = For lo hi (g . body)
+    hfmap _ Break             = Break
+
+instance DryInterp (ControlCMD exp)
+  where
+    dryInterp (If _ _ _)  = return ()
+    dryInterp (While _ _) = return ()
+    dryInterp (For _ _ _) = return ()
+    dryInterp Break       = return ()
+
+type instance IExp (ControlCMD e)       = e
+type instance IExp (ControlCMD e :+: i) = e
+
+
+
+--------------------------------------------------------------------------------
+-- * File handling
+--------------------------------------------------------------------------------
+
+-- | File handle
+data Handle
+    = HandleComp String
+    | HandleEval IO.Handle
+  deriving Typeable
+
+-- | Identifiers from handles
+instance ToIdent Handle
+  where
+    toIdent (HandleComp h) = C.Id h
+
+-- | Handle to stdin
+stdin :: Handle
+stdin = HandleComp "stdin"
+
+-- | Handle to stdout
+stdout :: Handle
+stdout = HandleComp "stdout"
+
+-- | Values that can be printed\/scanned using @printf@\/@scanf@
+class (Typeable a, Read a, Printf.PrintfArg a) => Formattable a
+  where
+    formatSpecifier :: Proxy a -> String
+
+instance Formattable Int    where formatSpecifier _ = "%d"
+instance Formattable Int8   where formatSpecifier _ = "%d"
+instance Formattable Int16  where formatSpecifier _ = "%d"
+instance Formattable Int32  where formatSpecifier _ = "%d"
+instance Formattable Int64  where formatSpecifier _ = "%d"
+instance Formattable Word   where formatSpecifier _ = "%u"
+instance Formattable Word8  where formatSpecifier _ = "%u"
+instance Formattable Word16 where formatSpecifier _ = "%u"
+instance Formattable Word32 where formatSpecifier _ = "%u"
+instance Formattable Word64 where formatSpecifier _ = "%u"
+instance Formattable Float  where formatSpecifier _ = "%f"
+instance Formattable Double where formatSpecifier _ = "%f"
+
+data FileCMD exp (prog :: * -> *) a
+  where
+    FOpen   :: FilePath -> IOMode                       -> FileCMD exp prog Handle
+    FClose  :: Handle                                   -> FileCMD exp prog ()
+    FEof    :: VarPred exp Bool => Handle               -> FileCMD exp prog (exp Bool)
+    FPrintf :: Handle -> String -> [PrintfArg exp]      -> FileCMD exp prog ()
+    FGet    :: (Formattable a, VarPred exp a) => Handle -> FileCMD exp prog (exp a)
+
+data PrintfArg exp where
+  PrintfArg :: (Printf.PrintfArg a, VarPred exp a) => exp a -> PrintfArg exp
+
+instance HFunctor (FileCMD exp)
+  where
+    hfmap _ (FOpen file mode)     = FOpen file mode
+    hfmap _ (FClose hdl)          = FClose hdl
+    hfmap _ (FPrintf hdl form as) = FPrintf hdl form as
+    hfmap _ (FGet hdl)            = FGet hdl
+    hfmap _ (FEof hdl)            = FEof hdl
+
+instance CompExp exp => DryInterp (FileCMD exp)
+  where
+    dryInterp (FOpen _ _)     = liftM HandleComp $ freshStr "h"
+    dryInterp (FClose _)      = return ()
+    dryInterp (FPrintf _ _ _) = return ()
+    dryInterp (FGet _)        = liftM varExp fresh
+    dryInterp (FEof _)        = liftM varExp fresh
+
+type instance IExp (FileCMD e)       = e
+type instance IExp (FileCMD e :+: i) = e
+
+
+
+--------------------------------------------------------------------------------
+-- * Abstract objects
+--------------------------------------------------------------------------------
+
+data Object = Object
+    { pointed    :: Bool
+    , objectType :: String
+    , objectId   :: String
+    }
+  deriving (Eq, Show, Ord, Typeable)
+
+-- | Identifiers from objects
+instance ToIdent Object
+  where
+    toIdent (Object _ _ o) = C.Id o
+
+data ObjectCMD exp (prog :: * -> *) a
+  where
+    NewObject
+        :: String  -- Type
+        -> ObjectCMD exp prog Object
+    InitObject
+        :: String -- Function name
+        -> Bool   -- Pointed object?
+        -> String -- Object Type
+        -> [FunArg exp]
+        -> ObjectCMD exp prog Object
+
+instance HFunctor (ObjectCMD exp)
+  where
+    hfmap _ (NewObject t)        = NewObject t
+    hfmap _ (InitObject s p t a) = InitObject s p t a
+
+instance DryInterp (ObjectCMD exp)
+  where
+    dryInterp (NewObject t)        = liftM (Object True t) $ freshStr "obj"
+    dryInterp (InitObject _ _ t _) = liftM (Object True t) $ freshStr "obj"
+
+type instance IExp (ObjectCMD e)       = e
+type instance IExp (ObjectCMD e :+: i) = e
+
+
+
+--------------------------------------------------------------------------------
+-- * External function calls (C-specific)
+--------------------------------------------------------------------------------
+
+data FunArg exp where
+  FunArg :: Arg arg => arg exp -> FunArg exp
+
+-- | Evidence that @`VarPred` exp1@ implies @`VarPred` exp2@
+type VarPredCast exp1 exp2 = forall a b .
+    VarPred exp1 a => Proxy a -> (VarPred exp2 a => b) -> b
+
+class Arg arg where
+  mkArg   :: CompExp exp => arg exp -> CGen C.Exp
+  mkParam :: CompExp exp => arg exp -> CGen C.Param
+
+  -- | Map over the expression(s) in an argument
+  mapArg  :: VarPredCast exp1 exp2
+          -> (forall a . VarPred exp1 a => exp1 a -> exp2 a)
+          -> arg exp1
+          -> arg exp2
+
+  -- | Monadic map over the expression(s) in an argument
+  mapMArg :: Monad m
+          => VarPredCast exp1 exp2
+          -> (forall a . VarPred exp1 a => exp1 a -> m (exp2 a))
+          -> arg exp1
+          -> m (arg exp2)
+
+instance Arg FunArg where
+  mkArg   (FunArg arg) = mkArg arg
+  mkParam (FunArg arg) = mkParam arg
+  mapArg  predCast f (FunArg arg) = FunArg (mapArg predCast f arg)
+  mapMArg predCast f (FunArg arg) = liftM FunArg (mapMArg predCast f arg)
+
+data CallCMD exp (prog :: * -> *) a
+  where
+    AddInclude    :: String       -> CallCMD exp prog ()
+    AddDefinition :: C.Definition -> CallCMD exp prog ()
+    AddExternFun  :: VarPred exp res
+                  => String
+                  -> proxy (exp res)
+                  -> [FunArg exp]
+                  -> CallCMD exp prog ()
+    AddExternProc :: String -> [FunArg exp] -> CallCMD exp prog ()
+    CallFun       :: VarPred exp a => String -> [FunArg exp] -> CallCMD exp prog (exp a)
+    CallProc      ::                  String -> [FunArg exp] -> CallCMD exp prog ()
+
+instance HFunctor (CallCMD exp)
+  where
+    hfmap _ (AddInclude incl)           = AddInclude incl
+    hfmap _ (AddDefinition def)         = AddDefinition def
+    hfmap _ (AddExternFun fun res args) = AddExternFun fun res args
+    hfmap _ (AddExternProc proc args)   = AddExternProc proc args
+    hfmap _ (CallFun fun args)          = CallFun fun args
+    hfmap _ (CallProc proc args)        = CallProc proc args
+
+instance CompExp exp => DryInterp (CallCMD exp)
+  where
+    dryInterp (AddInclude _)       = return ()
+    dryInterp (AddDefinition _)    = return ()
+    dryInterp (AddExternFun _ _ _) = return ()
+    dryInterp (AddExternProc _ _)  = return ()
+    dryInterp (CallFun _ _)        = liftM varExp fresh
+    dryInterp (CallProc _ _)       = return ()
+
+type instance IExp (CallCMD e)       = e
+type instance IExp (CallCMD e :+: i) = e
+
+
+
+--------------------------------------------------------------------------------
+-- * Running commands
+--------------------------------------------------------------------------------
+
+runRefCMD :: forall exp prog a . EvalExp exp => RefCMD exp prog a -> IO a
+runRefCMD (InitRef a)                       = fmap RefEval $ newIORef $ evalExp a
+runRefCMD NewRef                            = fmap RefEval $ newIORef $ error "reading uninitialized reference"
+runRefCMD (SetRef (RefEval r) a)            = writeIORef r $ evalExp a
+runRefCMD (GetRef (RefEval (r :: IORef b))) = fmap litExp $ readIORef r
+
+runArrCMD :: EvalExp exp => ArrCMD exp prog a -> IO a
+runArrCMD (NewArr n) = fmap ArrEval $ newArray_ (0, fromIntegral (evalExp n)-1)
+runArrCMD (NewArr_) = error "NewArr_ not allowed in interpreted mode"
+runArrCMD (SetArr i a (ArrEval arr)) =
+    writeArray arr (fromIntegral (evalExp i)) (evalExp a)
+runArrCMD (GetArr i (ArrEval arr)) =
+    fmap litExp $ readArray arr (fromIntegral (evalExp i))
+
+runControlCMD :: EvalExp exp => ControlCMD exp IO a -> IO a
+runControlCMD (If c t f)        = if evalExp c then t else f
+runControlCMD (While cont body) = loop
+  where loop = do
+          c <- cont
+          when (evalExp c) $ body >> loop
+runControlCMD (For lo hi body) = loop (evalExp lo)
+  where
+    hi' = evalExp hi
+    loop i
+      | i <= hi'  = body (litExp i) >> loop (i+1)
+      | otherwise = return ()
+runControlCMD Break = error "cannot run programs involving break"
+
+evalHandle :: Handle -> IO.Handle
+evalHandle (HandleEval h)        = h
+evalHandle (HandleComp "stdin")  = IO.stdin
+evalHandle (HandleComp "stdout") = IO.stdout
+
+readWord :: IO.Handle -> IO String
+readWord h = do
+    eof <- IO.hIsEOF h
+    if eof
+    then return ""
+    else do
+      c  <- IO.hGetChar h
+      if isSpace c
+      then return ""
+      else do
+        cs <- readWord h
+        return (c:cs)
+
+evalFPrintf :: EvalExp exp =>
+    [PrintfArg exp] -> (forall r . Printf.HPrintfType r => r) -> IO ()
+evalFPrintf []            pf = pf
+evalFPrintf (PrintfArg a:as) pf = evalFPrintf as (pf $ evalExp a)
+
+runFileCMD :: EvalExp exp => FileCMD exp IO a -> IO a
+runFileCMD (FOpen file mode)              = fmap HandleEval $ IO.openFile file mode
+runFileCMD (FClose (HandleEval h))        = IO.hClose h
+runFileCMD (FClose (HandleComp "stdin"))  = return ()
+runFileCMD (FClose (HandleComp "stdout")) = return ()
+runFileCMD (FPrintf h format as)          = evalFPrintf as (Printf.hPrintf (evalHandle h) format)
+runFileCMD (FGet h)   = do
+    w <- readWord $ evalHandle h
+    case reads w of
+        [(f,"")] -> return $ litExp f
+        _        -> error $ "fget: no parse (input " ++ show w ++ ")"
+runFileCMD (FEof h) = fmap litExp $ IO.hIsEOF $ evalHandle h
+
+runObjectCMD :: ObjectCMD exp IO a -> IO a
+runObjectCMD (NewObject _) = error "cannot run programs involving newObject"
+runObjectCMD (InitObject _ _ _ _) = error "cannot run programs involving initObject"
+
+runCallCMD :: EvalExp exp => CallCMD exp IO a -> IO a
+runCallCMD (AddInclude _)       = return ()
+runCallCMD (AddDefinition _)    = return ()
+runCallCMD (AddExternFun _ _ _) = return ()
+runCallCMD (AddExternProc _ _)  = return ()
+runCallCMD (CallFun _ _)        = error "cannot run programs involving callFun"
+runCallCMD (CallProc _ _)       = error "cannot run programs involving callProc"
+
+instance EvalExp exp => Interp (RefCMD exp)     IO where interp = runRefCMD
+instance EvalExp exp => Interp (ArrCMD exp)     IO where interp = runArrCMD
+instance EvalExp exp => Interp (ControlCMD exp) IO where interp = runControlCMD
+instance EvalExp exp => Interp (FileCMD exp)    IO where interp = runFileCMD
+instance                Interp (ObjectCMD exp)  IO where interp = runObjectCMD
+instance EvalExp exp => Interp (CallCMD exp)    IO where interp = runCallCMD
+
diff --git a/src/Language/Embedded/Imperative/Frontend.hs b/src/Language/Embedded/Imperative/Frontend.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Embedded/Imperative/Frontend.hs
@@ -0,0 +1,459 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- Front end for imperative instructions
+--
+-- These instructions are general imperative constructs independent of the back
+-- end, except for the stuff under \"External function calls\" which is
+-- C-specific.
+
+module Language.Embedded.Imperative.Frontend where
+
+
+
+import Prelude hiding (break)
+
+import Data.Array.IO
+import Data.IORef
+import Data.Typeable
+import System.IO.Unsafe
+
+#if __GLASGOW_HASKELL__ < 708
+import Data.Proxy
+#endif
+import Language.C.Quote.C
+
+import Control.Monad.Operational.Higher
+import Language.Embedded.Expression
+import Language.Embedded.Imperative.CMD
+import Language.Embedded.Imperative.Frontend.General
+import Language.Embedded.Imperative.Args
+
+
+
+--------------------------------------------------------------------------------
+-- * References
+--------------------------------------------------------------------------------
+
+-- | Create an uninitialized reference
+newRef :: (VarPred (IExp instr) a, RefCMD (IExp instr) :<: instr) => ProgramT instr m (Ref a)
+newRef = singleE NewRef
+
+-- | Create an initialized reference
+initRef :: (VarPred (IExp instr) a, RefCMD (IExp instr) :<: instr) =>
+    IExp instr a -> ProgramT instr m (Ref a)
+initRef = singleE . InitRef
+
+-- | Get the contents of a reference
+getRef :: (VarPred (IExp instr) a, RefCMD (IExp instr) :<: instr) =>
+    Ref a -> ProgramT instr m (IExp instr a)
+getRef = singleE . GetRef
+
+-- | Set the contents of a reference
+setRef :: (VarPred (IExp instr) a, RefCMD (IExp instr) :<: instr) =>
+    Ref a -> IExp instr a -> ProgramT instr m ()
+setRef r = singleE . SetRef r
+
+-- | Modify the contents of reference
+modifyRef
+    :: ( VarPred (IExp instr) a
+       , EvalExp (IExp instr)
+       , CompExp (IExp instr)
+       , RefCMD (IExp instr) :<: instr
+       , Monad m
+       )
+    => Ref a -> (IExp instr a -> IExp instr a) -> ProgramT instr m ()
+modifyRef r f = setRef r . f =<< unsafeFreezeRef r
+
+-- | Read the value of a reference without returning in the monad
+--
+-- WARNING: Don't use this function unless you really know what you are doing.
+-- It is almost always better to use 'unsafeFreezeRef' instead.
+--
+-- 'veryUnsafeFreezeRef' behaves predictably when doing code generation, but it
+-- can give strange results when evaluating in 'IO', as explained here:
+--
+-- <http://fun-discoveries.blogspot.se/2015/09/strictness-can-fix-non-termination.html>
+veryUnsafeFreezeRef :: (VarPred exp a, EvalExp exp, CompExp exp) =>
+    Ref a -> exp a
+veryUnsafeFreezeRef (RefEval r) = litExp $! unsafePerformIO $! readIORef r
+veryUnsafeFreezeRef (RefComp v) = varExp v
+
+-- | Freeze the contents of reference (only safe if the reference is never
+-- written to after the freezing)
+unsafeFreezeRef :: (VarPred exp a, EvalExp exp, CompExp exp, Monad m) =>
+    Ref a -> ProgramT instr m (exp a)
+unsafeFreezeRef r = return $! veryUnsafeFreezeRef r
+  -- Strict applications (here and in `veryUnsafeFreezeRef`) are needed when
+  -- evaluating in `IO` to force `readIORef` to be performed before the next
+  -- action.
+  --
+  -- The `modifyRef` test case fails if the strict applications are removed, so
+  -- this seems to work. If there's a problem, another possibility would be to
+  -- make `unsafeFreezeRef` an instruction in `RefCMD`. This would avoid the
+  -- need for `unsafePerformIO`.
+
+
+
+--------------------------------------------------------------------------------
+-- * Arrays
+--------------------------------------------------------------------------------
+
+-- | Create an uninitialized an array
+newArr
+    :: ( pred a
+       , pred i
+       , Integral i
+       , Ix i
+       , ArrCMD (IExp instr) :<: instr
+       , pred ~ VarPred (IExp instr)
+       )
+    => IExp instr i -> ProgramT instr m (Arr i a)
+newArr n = singleE $ NewArr n
+
+newArr_
+    :: ( pred a
+       , pred i
+       , Integral i
+       , Ix i
+       , ArrCMD (IExp instr) :<: instr
+       , pred ~ VarPred (IExp instr)
+       )
+    => ProgramT instr m (Arr i a)
+newArr_ = singleE $ NewArr_
+
+-- | Set the contents of an array
+getArr
+    :: ( VarPred (IExp instr) a
+       , ArrCMD (IExp instr) :<: instr
+       , Integral i
+       , Ix i
+       )
+    => IExp instr i -> Arr i a -> ProgramT instr m (IExp instr a)
+getArr i arr = singleE $ GetArr i arr
+
+-- | Set the contents of an array
+setArr
+    :: ( VarPred (IExp instr) a
+       , ArrCMD (IExp instr) :<: instr
+       , Integral i
+       , Ix i
+       )
+    => IExp instr i -> IExp instr a -> Arr i a -> ProgramT instr m ()
+setArr i a arr = singleE (SetArr i a arr)
+
+
+
+--------------------------------------------------------------------------------
+-- * Control flow
+--------------------------------------------------------------------------------
+
+-- | Conditional statement
+iff :: (ControlCMD (IExp instr) :<: instr)
+    => IExp instr Bool      -- ^ Condition
+    -> ProgramT instr m ()  -- ^ True branch
+    -> ProgramT instr m ()  -- ^ False branch
+    -> ProgramT instr m ()
+iff b t f = singleE $ If b t f
+
+-- | Conditional statement that returns an expression
+ifE
+    :: ( VarPred (IExp instr) a
+       , ControlCMD (IExp instr) :<: instr
+       , RefCMD (IExp instr)     :<: instr
+       , Monad m
+       )
+    => IExp instr Bool                  -- ^ Condition
+    -> ProgramT instr m (IExp instr a)  -- ^ True branch
+    -> ProgramT instr m (IExp instr a)  -- ^ False branch
+    -> ProgramT instr m (IExp instr a)
+ifE b t f = do
+    r <- newRef
+    iff b (t >>= setRef r) (f >>= setRef r)
+    getRef r
+
+-- | While loop
+while :: (ControlCMD (IExp instr) :<: instr)
+    => ProgramT instr m (IExp instr Bool)  -- ^ Continue condition
+    -> ProgramT instr m ()                 -- ^ Loop body
+    -> ProgramT instr m ()
+while b t = singleE $ While b t
+
+-- | While loop that returns an expression
+whileE
+    :: ( VarPred (IExp instr) a
+       , ControlCMD (IExp instr) :<: instr
+       , RefCMD (IExp instr)     :<: instr
+       , Monad m
+       )
+    => ProgramT instr m (IExp instr Bool)  -- ^ Continue condition
+    -> ProgramT instr m (IExp instr a)     -- ^ Loop body
+    -> ProgramT instr m (IExp instr a)
+whileE b t = do
+    r <- newRef
+    while b (t >>= setRef r)
+    getRef r
+
+-- | For loop
+for :: (ControlCMD (IExp instr) :<: instr, Integral n, VarPred (IExp instr) n)
+    => IExp instr n                           -- ^ Start index
+    -> IExp instr n                           -- ^ Stop index
+    -> (IExp instr n -> ProgramT instr m ())  -- ^ Loop body
+    -> ProgramT instr m ()
+for lo hi body = singleE $ For lo hi body
+
+-- | For loop
+forE
+    :: ( Integral n
+       , VarPred (IExp instr) n
+       , VarPred (IExp instr) a
+       , ControlCMD (IExp instr) :<: instr
+       , RefCMD (IExp instr)     :<: instr
+       , Monad m
+       )
+    => IExp instr n                                       -- ^ Start index
+    -> IExp instr n                                       -- ^ Stop index
+    -> (IExp instr n -> ProgramT instr m (IExp instr a))  -- ^ Loop body
+    -> ProgramT instr m (IExp instr a)
+forE lo hi body = do
+    r <- newRef
+    for lo hi (body >=> setRef r)
+    getRef r
+
+-- | Break out from a loop
+break :: (ControlCMD (IExp instr) :<: instr) => ProgramT instr m ()
+break = singleE Break
+
+
+
+--------------------------------------------------------------------------------
+-- * File handling
+--------------------------------------------------------------------------------
+
+-- | Open a file
+fopen :: (FileCMD (IExp instr) :<: instr) => FilePath -> IOMode -> ProgramT instr m Handle
+fopen file = singleE . FOpen file
+
+-- | Close a file
+fclose :: (FileCMD (IExp instr) :<: instr) => Handle -> ProgramT instr m ()
+fclose = singleE . FClose
+
+-- | Check for end of file
+feof :: (VarPred (IExp instr) Bool, FileCMD (IExp instr) :<: instr) =>
+    Handle -> ProgramT instr m (IExp instr Bool)
+feof = singleE . FEof
+
+class PrintfType r
+  where
+    type PrintfExp r :: * -> *
+    fprf :: Handle -> String -> [PrintfArg (PrintfExp r)] -> r
+
+instance (FileCMD (IExp instr) :<: instr, a ~ ()) => PrintfType (ProgramT instr m a)
+  where
+    type PrintfExp (ProgramT instr m a) = IExp instr
+    fprf h form as = singleE $ FPrintf h form (reverse as)
+
+instance (Formattable a, VarPred exp a, PrintfType r, exp ~ PrintfExp r) =>
+    PrintfType (exp a -> r)
+  where
+    type PrintfExp (exp a -> r) = exp
+    fprf h form as = \a -> fprf h form (PrintfArg a : as)
+
+-- | Print to a handle. Accepts a variable number of arguments.
+fprintf :: PrintfType r => Handle -> String -> r
+fprintf h format = fprf h format []
+
+-- | Put a single value to a handle
+fput :: forall instr a m
+    .  (Formattable a, VarPred (IExp instr) a, FileCMD (IExp instr) :<: instr)
+    => Handle
+    -> String        -- ^ Prefix
+    -> IExp instr a  -- ^ Expression to print
+    -> String        -- ^ Suffix
+    -> ProgramT instr m ()
+fput hdl prefix a suffix =
+    fprintf hdl (prefix ++ formatSpecifier (Proxy :: Proxy a) ++ suffix) a
+
+-- | Get a single value from a handle
+fget
+    :: ( Formattable a
+       , VarPred (IExp instr) a
+       , FileCMD (IExp instr) :<: instr
+       )
+    => Handle -> ProgramT instr m (IExp instr a)
+fget = singleE . FGet
+
+-- | Print to @stdout@. Accepts a variable number of arguments.
+printf :: PrintfType r => String -> r
+printf = fprintf stdout
+
+
+
+--------------------------------------------------------------------------------
+-- * Abstract objects
+--------------------------------------------------------------------------------
+
+-- | Create a pointer to an abstract object. The only thing one can do with such
+-- objects is to pass them to 'callFun' or 'callProc'.
+newObject :: (ObjectCMD (IExp instr) :<: instr)
+    => String  -- ^ Object type
+    -> ProgramT instr m Object
+newObject = singleE . NewObject
+
+-- | Call a function to create a pointed object
+initObject :: (ObjectCMD (IExp instr) :<: instr)
+    => String                 -- ^ Function name
+    -> String                 -- ^ Object type
+    -> [FunArg (IExp instr)]  -- ^ Arguments
+    -> ProgramT instr m Object
+initObject fun ty args = singleE $ InitObject fun True ty args
+
+-- | Call a function to create an object
+initUObject :: (ObjectCMD (IExp instr) :<: instr)
+    => String                 -- ^ Function name
+    -> String                 -- ^ Object type
+    -> [FunArg (IExp instr)]  -- ^ Arguments
+    -> ProgramT instr m Object
+initUObject fun ty args = singleE $ InitObject fun False ty args
+
+
+
+--------------------------------------------------------------------------------
+-- * External function calls (C-specific)
+--------------------------------------------------------------------------------
+
+-- | Add an @#include@ statement to the generated code
+addInclude :: (CallCMD (IExp instr) :<: instr) => String -> ProgramT instr m ()
+addInclude = singleE . AddInclude
+
+-- | Add a global definition to the generated code
+--
+-- Can be used conveniently as follows:
+--
+-- > {-# LANGUAGE QuasiQuotes #-}
+-- >
+-- > import Language.Embedded.Imperative
+-- > import Language.C.Quote.C
+-- >
+-- > prog = do
+-- >     ...
+-- >     addDefinition myCFunction
+-- >     ...
+-- >   where
+-- >     myCFunction = [cedecl|
+-- >       void my_C_function( ... )
+-- >       {
+-- >           // C code
+-- >           // goes here
+-- >       }
+-- >       |]
+addDefinition :: (CallCMD (IExp instr) :<: instr) => Definition -> ProgramT instr m ()
+addDefinition = singleE . AddDefinition
+
+-- | Declare an external function
+addExternFun :: (VarPred exp res, CallCMD exp :<: instr, exp ~ IExp instr)
+    => String           -- ^ Function name
+    -> proxy (exp res)  -- ^ Proxy for expression and result type
+    -> [FunArg exp]     -- ^ Arguments (only used to determine types)
+    -> ProgramT instr m ()
+addExternFun fun res args = singleE $ AddExternFun fun res args
+
+-- | Declare an external procedure
+addExternProc :: (CallCMD exp :<: instr, exp ~ IExp instr)
+    => String        -- ^ Procedure name
+    -> [FunArg exp]  -- ^ Arguments (only used to determine types)
+    -> ProgramT instr m ()
+addExternProc proc args = singleE $ AddExternProc proc args
+
+-- | Call a function
+callFun :: (VarPred (IExp instr) a, CallCMD (IExp instr) :<: instr)
+    => String                 -- ^ Function name
+    -> [FunArg (IExp instr)]  -- ^ Arguments
+    -> ProgramT instr m (IExp instr a)
+callFun fun as = singleE $ CallFun fun as
+
+-- | Call a procedure
+callProc :: (CallCMD (IExp instr) :<: instr)
+    => String                 -- ^ Procedure name
+    -> [FunArg (IExp instr)]  -- ^ Arguments
+    -> ProgramT instr m ()
+callProc fun as = singleE $ CallProc fun as
+
+-- | Declare and call an external function
+externFun :: forall instr m exp res
+    .  (VarPred exp res, CallCMD exp :<: instr, exp ~ IExp instr, Monad m)
+    => String        -- ^ Function name
+    -> [FunArg exp]  -- ^ Arguments
+    -> ProgramT instr m (exp res)
+externFun fun args = do
+    addExternFun fun (Proxy :: Proxy (exp res)) args
+    callFun fun args
+
+-- | Declare and call an external procedure
+externProc :: (CallCMD exp :<: instr, exp ~ IExp instr, Monad m)
+    => String        -- ^ Procedure name
+    -> [FunArg exp]  -- ^ Arguments
+    -> ProgramT instr m ()
+externProc proc args = do
+    addExternProc proc args
+    callProc proc args
+
+-- | Get current time as number of seconds passed today
+getTime :: (VarPred (IExp instr) Double, CallCMD (IExp instr) :<: instr, Monad m) =>
+    ProgramT instr m (IExp instr Double)
+getTime = do
+    addInclude "<sys/time.h>"
+    addInclude "<sys/resource.h>"
+    addDefinition getTimeDef
+    callFun "get_time" []
+  where
+    getTimeDef = [cedecl|
+      double get_time()
+      {
+          struct timeval t;
+          struct timezone tzp;
+          gettimeofday(&t, &tzp);
+          return t.tv_sec + t.tv_usec*1e-6;
+      }
+      |]
+      -- From http://stackoverflow.com/questions/2349776/how-can-i-benchmark-c-code-easily
+
+-- Arguments
+
+-- | Constant string argument
+strArg :: String -> FunArg exp
+strArg = FunArg . StrArg
+
+-- | Value argument
+valArg :: VarPred exp a => exp a -> FunArg exp
+valArg = FunArg . ValArg
+
+-- | Reference argument
+refArg :: VarPred exp a => Ref a -> FunArg exp
+refArg = FunArg . RefArg
+
+-- | Array argument
+arrArg :: VarPred exp a => Arr n a -> FunArg exp
+arrArg = FunArg . ArrArg
+
+-- | Abstract object argument
+objArg :: Object -> FunArg exp
+objArg = FunArg . ObjArg
+
+-- | Modifier that takes the address of another argument
+addr :: FunArg exp -> FunArg exp
+addr = FunArg . Addr
+
+
+
+--------------------------------------------------------------------------------
+-- * Running programs
+--------------------------------------------------------------------------------
+
+-- | Run a program in 'IO'. Note that not all instructions are supported for
+-- running in 'IO'. For example, calls to external C functions are not
+-- supported.
+runIO :: (Interp instr IO, HFunctor instr) => Program instr a -> IO a
+runIO = interpret
+
diff --git a/src/Language/Embedded/Imperative/Frontend/General.hs b/src/Language/Embedded/Imperative/Frontend/General.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Embedded/Imperative/Frontend/General.hs
@@ -0,0 +1,29 @@
+-- | Exports the general parts of imperative front ends. The motivation for this
+-- module is to support making specialized front ends (e.g. like
+-- "Language.Embedded.Imperative.Frontend" but for a specific instruction set).
+-- These exports are the parts of the front end that are independent of the
+-- instruction set and/or expression language.
+
+module Language.Embedded.Imperative.Frontend.General
+  ( Ref
+  , Arr
+  , IO.IOMode (..)
+  , Handle
+  , stdin
+  , stdout
+  , Formattable
+  , Object
+  , FunArg (..)
+  , Definition
+  , cedecl
+  ) where
+  -- Note: Important not to export the constructors of `Ref`, `Arr` or `Handle`,
+  -- since the user is not supposed to inspect such values.
+
+import qualified System.IO as IO
+
+import Language.Embedded.Imperative.CMD
+
+import Language.C.Syntax
+import Language.C.Quote.C
+
diff --git a/src/Language/Embedded/Signature.hs b/src/Language/Embedded/Signature.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Embedded/Signature.hs
@@ -0,0 +1,105 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Language.Embedded.Signature where
+
+import Data.Proxy
+
+import Language.C.Monad
+import Language.Embedded.Expression
+
+import Language.C.Quote.C
+import Language.C.Syntax (Id(..),Exp(..),Type)
+
+
+-- * Language
+
+-- | Signature annotations
+data Ann exp a where
+  Empty  :: Ann exp a
+  Native :: (VarPred exp a) => exp len -> Ann exp [a]
+  Named  :: String -> Ann exp a
+
+-- | Signatures
+data Signature exp a where
+  Ret    :: (VarPred exp a) => String -> exp a -> Signature exp a
+  Ptr    :: (VarPred exp a) => String -> exp a -> Signature exp a
+  Lam    :: (VarPred exp a) => Ann exp a -> (exp a -> Signature exp b)
+         -> Signature exp (a -> b)
+
+
+-- * Combinators
+
+lam :: (VarPred exp a)
+    => (exp a -> Signature exp b) -> Signature exp (a -> b)
+lam f = Lam Empty $ \x -> f x
+
+name :: (VarPred exp a)
+     => String -> (exp a -> Signature exp b) -> Signature exp (a -> b)
+name s f = Lam (Named s) $ \x -> f x
+
+ret,ptr :: (VarPred exp a)
+        => String -> exp a -> Signature exp a
+ret = Ret
+ptr = Ptr
+
+arg :: (VarPred exp a)
+    => Ann exp a -> (exp a -> exp b) -> (exp b -> Signature exp c) -> Signature exp (a -> c)
+arg s g f = Lam s $ \x -> f (g x)
+
+
+
+-- * Compilation
+
+-- | Compile a function @Signature@ to C code
+translateFunction :: forall m exp a. (MonadC m, CompExp exp)
+                  => Signature exp a -> m ()
+translateFunction sig = go sig (return ())
+  where
+    go :: forall d. Signature exp d -> m () -> m ()
+    go (Ret n a) prelude = do
+      t <- compType a
+      inFunctionTy t n $ do
+        prelude
+        e <- compExp a
+        addStm [cstm| return $e; |]
+    go (Ptr n a) prelude = do
+      t <- compType a
+      inFunction n $ do
+        prelude
+        e <- compExp a
+        addParam [cparam| $ty:t *out |]
+        addStm [cstm| *out = $e; |]
+    go fun@(Lam Empty f) prelude = do
+      t <- compTypePP (Proxy :: Proxy exp) (argProxy fun)
+      v <- fmap varExp freshId
+      Var n _ <- compExp v
+      go (f v) $ prelude >> addParam [cparam| $ty:t $id:n |]
+    go fun@(Lam n@(Native l) f) prelude = do
+      t <- compTypePP (Proxy :: Proxy exp) (elemProxy n fun)
+      i <- freshId
+      let w = varExp i
+      Var (Id m _) _ <- compExp w
+      let n = m ++ "_buf"
+      withAlias i ('&':m) $ go (f w) $ do
+        prelude
+        len <- compExp l
+        addLocal [cdecl| struct array $id:m = { .buffer = $id:n
+                                              , .length=$len
+                                              , .elemSize=sizeof($ty:t)
+                                              , .bytes=sizeof($ty:t)*$len
+                                              }; |]
+        addParam [cparam| $ty:t * $id:n |]
+    go fun@(Lam (Named s) f) prelude = do
+      t <- compTypePP (Proxy :: Proxy exp) (argProxy fun)
+      i <- freshId
+      withAlias i s $ go (f $ varExp i) $ prelude >> addParam [cparam| $ty:t $id:s |]
+
+    argProxy :: Signature exp (b -> c) -> Proxy b
+    argProxy _ = Proxy
+
+    elemProxy :: Ann exp [b] -> Signature exp ([b] -> c) -> Proxy b
+    elemProxy _ _ = Proxy
+
diff --git a/src/Language/Embedded/Traversal.hs b/src/Language/Embedded/Traversal.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Embedded/Traversal.hs
@@ -0,0 +1,49 @@
+{-# LANGUAGE CPP #-}
+
+-- | Methods for traversing programs
+
+module Language.Embedded.Traversal where
+
+
+
+import Control.Monad.Operational.Higher
+
+import Control.Monads
+
+
+
+-- | Dry (effect-less) interpretation of an instruction. This class is like
+-- 'Interp' without the monad parameter, so it cannot have different instances
+-- for different monads.
+class DryInterp instr
+  where
+    -- | Dry interpretation of an instruction. This function is like 'interp'
+    -- except that it interprets in any monad that can supply fresh variables.
+    dryInterp :: MonadSupply m => instr m a -> m a
+
+-- | Interpretation of a program as a combination of dry interpretation and
+-- effectful observation
+observe_ :: (DryInterp instr, HFunctor instr, MonadSupply m)
+    => (forall a . instr m a -> a -> m ())  -- ^ Function for observing instructions
+    -> Program instr a
+    -> m a
+observe_ obs = interpretWithMonad $ \i -> do
+    a <- dryInterp i
+    obs i a
+    return a
+
+-- | Interpretation of a program as a combination of dry interpretation and
+-- effectful observation
+observe :: (DryInterp instr, HFunctor instr, MonadSupply m)
+    => (forall a . instr m a -> a -> m a)  -- ^ Function for observing instructions
+    -> Program instr a
+    -> m a
+observe obs = interpretWithMonad $ \i -> do
+    a <- dryInterp i
+    obs i a
+
+instance (DryInterp i1, DryInterp i2) => DryInterp (i1 :+: i2)
+  where
+    dryInterp (Inl i) = dryInterp i
+    dryInterp (Inr i) = dryInterp i
+
diff --git a/tests/Examples.hs b/tests/Examples.hs
new file mode 100644
--- /dev/null
+++ b/tests/Examples.hs
@@ -0,0 +1,22 @@
+import Imperative ()
+import Concurrent ()
+import Language.Embedded.CExp
+import Language.Embedded.Imperative
+import Language.Embedded.Backend.C
+import System.IO
+import System.Process
+import System.Directory
+import System.Exit
+
+main = do let c = compile $
+                 do addInclude "<stdio.h>" :: Program (CallCMD CExp) ()
+                    callProc "printf" [strArg "Hello World!\n"]
+          (fp,h) <- openTempFile "" "temp.c"
+          hPutStrLn h c
+          hClose h
+          system $ "gcc " ++ fp
+          e <- system "./a.out"
+          removeFile fp
+          removeFile "a.out"
+          exitWith e
+
diff --git a/tests/Semantics.hs b/tests/Semantics.hs
new file mode 100644
--- /dev/null
+++ b/tests/Semantics.hs
@@ -0,0 +1,22 @@
+import Language.Embedded.Expression (evalExp)
+import Language.Embedded.Imperative
+import Language.Embedded.CExp
+
+
+
+-- Test that `modifyRef` doesn't loop. It will loop if evaluation of `setRef` is
+-- too lazy so that the `unsafeFreezeRef` happens before `setRef` in
+-- `modifyRef`.
+modifyRefProg :: Program (RefCMD CExp) (CExp Int32)
+modifyRefProg = do
+    r <- initRef 0
+    modifyRef r (+1)
+    getRef r
+
+testModifyRef = do
+    1 <- fmap evalExp $ runIO modifyRefProg
+    return ()
+
+main = do
+    testModifyRef
+