diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,25 @@
+Copyright (c) Tom Hawkins 2014
+
+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.
+3. For non-commercial use only.
+
+THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``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 AUTHORS 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/Language/ACL2.hs b/Language/ACL2.hs
new file mode 100644
--- /dev/null
+++ b/Language/ACL2.hs
@@ -0,0 +1,261 @@
+-- | A DSL for ACL2.
+module Language.ACL2
+  ( Expr (..)
+  , check
+  , check'
+  , mutualRecursion
+  , defun
+  , defun'
+  , defconst
+  , defthm
+  , thm
+  , call
+  , obj
+  , quote
+  , consp
+  , cons
+  , car
+  , cdr
+  , nth
+  , len
+  , take'
+  , nthcdr
+  , updateNth
+  , append
+  , let'
+  , if'
+  , case'
+  , assoc
+  , var
+  , list
+  , lit
+  , string
+  , nil
+  , t
+  , zp
+  , zip'
+  , undefined'
+  , equal
+  , not'
+  , and'
+  , or'
+  , implies
+  , goodbye
+  , integerp
+  , mod'
+  , (<.)
+  , (>.)
+  , (<=.)
+  , (>=.)
+  ) where
+
+import Data.List
+import System.Environment
+import System.Process
+
+data SExpr
+  = SV String
+  | SA [SExpr]
+
+instance Show SExpr where
+  show a = case a of
+    SV a -> a ++ "\n"
+    SA args -> "( " ++ indent (concatMap show args) ++ ")\n"
+      where
+      indent = drop 2 . unlines . map ("  " ++) . lines
+
+data Expr
+  = Obj [Expr]
+  | Lit String
+  deriving (Eq, Ord)
+
+instance Show Expr where show = show . sExpr
+
+instance Num Expr where
+  a + b = call "+" [a, b]
+  a - b = call "-" [a, b]
+  a * b = call "*" [a, b]
+  negate a = 0 - a
+  abs = undefined
+  signum = undefined
+  fromInteger = Lit . show
+
+sExpr :: Expr -> SExpr
+sExpr a = case a of
+  Obj     a   -> SA $ map sExpr a
+  Lit     a   -> SV a
+
+check'' :: Bool -> [Expr] -> IO Bool
+check'' debug a = do
+  exe <- savedACL2
+  (_, result, _) <- readProcessWithExitCode exe [] code
+  let pass = not $ any (isPrefixOf "ACL2 Error") $ lines result
+  if debug
+    then do
+      putStrLn code
+      putStrLn result
+    else return ()
+  return pass
+  where
+  code = unlines $ map show a
+  savedACL2 :: IO FilePath
+  savedACL2 = do
+    env <- getEnvironment
+    case lookup "ACL2_SOURCES" env of
+      Nothing -> error "Environment variable ACL2_SOURCES not set."
+      Just a -> return $ a ++ "/saved_acl2"
+
+check :: [Expr] -> IO Bool
+check = check'' False
+
+check' :: [Expr] -> IO Bool
+check' = check'' True
+
+uni :: String -> Expr -> Expr
+uni f a = call f [a]
+
+bin :: String -> Expr -> Expr -> Expr
+bin f a b = call f [a, b]
+
+tri :: String -> Expr -> Expr -> Expr -> Expr
+tri f a b c = call f [a, b, c]
+
+mutualRecursion :: [Expr] -> Expr
+mutualRecursion = call "mutual-recursion"
+
+defun :: String -> [String] -> Expr -> Expr
+defun name args body = call "defun" [var name, obj $ map var args, body]
+
+defun' :: String -> [String] -> Expr -> Expr -> Expr
+defun' name args measure body = call "defun"
+  [ var name
+  , obj $ map var args
+  , call "declare" [call "xargs" [var ":measure", call "nfix" [measure]]]
+  , body
+  ]
+
+defconst :: String -> Expr -> Expr
+defconst name const = call "defconst" [var name, const]
+
+defthm :: String -> Expr -> Expr
+defthm name a = call "defthm" [var name, a]
+
+thm :: Expr -> Expr
+thm = uni "thm"
+ 
+call :: String -> [Expr] -> Expr
+call a b = Obj $ var a : b
+
+obj :: [Expr] -> Expr
+obj = Obj
+
+quote :: Expr -> Expr
+quote = uni "quote"
+
+list :: [Expr] -> Expr
+list a = call "list" a
+
+consp :: Expr -> Expr
+consp = uni "consp"
+
+cons :: Expr -> Expr -> Expr
+cons = bin "cons"
+
+car :: Expr -> Expr
+car = uni "car"
+
+cdr :: Expr -> Expr
+cdr = uni "cdr"
+
+nth :: Expr -> Expr -> Expr
+nth = bin "nth"
+
+len :: Expr -> Expr
+len = uni "len"
+
+take' :: Expr -> Expr -> Expr
+take' = bin "take"
+
+nthcdr :: Expr -> Expr -> Expr
+nthcdr = bin "nthcdr"
+
+updateNth :: Expr -> Expr -> Expr -> Expr
+updateNth = tri "update-nth"
+
+append :: Expr -> Expr -> Expr
+append = bin "append"
+
+let' :: [(String, Expr)] -> Expr -> Expr
+let' a b = case b of
+  Obj [Lit "let*", Obj lets, expr] -> call "let*" [obj $ [ obj [var n, e] | (n, e) <- a ] ++ lets, expr]
+  _ -> call "let*" [obj [ obj [var n, e] | (n, e) <- a ], b]
+
+var :: String -> Expr
+var = Lit
+
+lit :: String -> Expr
+lit = Lit
+
+string :: String -> Expr
+string = Lit . show
+
+nil :: Expr
+nil = Lit "nil"
+
+t :: Expr
+t = Lit "t"
+
+if' :: Expr -> Expr -> Expr -> Expr
+if' = tri "if"
+
+case' :: Expr -> [(Expr, Expr)] -> Expr -> Expr
+case' a b c = call "case" $ a : [ obj [a, b] | (a, b) <- b ] ++ [call "otherwise" [c]]
+
+zp :: Expr -> Expr
+zp = uni "zp"
+
+zip' :: Expr -> Expr
+zip' = uni "zip"
+
+integerp :: Expr -> Expr
+integerp = uni "integerp"
+
+undefined' :: Expr
+undefined' = Lit "undefined"
+
+equal :: Expr -> Expr -> Expr
+equal = bin "equal"
+
+not' :: Expr -> Expr
+not' = uni "not"
+
+and' :: Expr -> Expr -> Expr
+and' = bin "and"
+
+or' :: Expr -> Expr -> Expr
+or' = bin "or"
+
+implies :: Expr -> Expr -> Expr
+implies = bin "implies"
+
+goodbye :: Expr
+goodbye = call "good-bye" []
+
+mod' :: Expr -> Expr -> Expr
+mod' = bin "mod"
+
+(<.) :: Expr -> Expr -> Expr
+(<.) = bin "<"
+
+(<=.) :: Expr -> Expr -> Expr
+(<=.) = bin "<="
+
+(>.) :: Expr -> Expr -> Expr
+(>.) = bin ">"
+
+(>=.) :: Expr -> Expr -> Expr
+(>=.) = bin ">="
+
+assoc :: Expr -> Expr -> Expr
+assoc = bin "assoc"
+
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,6 @@
+module Main (main) where
+
+import Distribution.Simple (defaultMain)
+
+main :: IO ()
+main = defaultMain
diff --git a/acl2.cabal b/acl2.cabal
new file mode 100644
--- /dev/null
+++ b/acl2.cabal
@@ -0,0 +1,29 @@
+name:    acl2
+version: 0.0.0
+
+category: Language, Formal Methods
+
+synopsis:    Writing and calling ACL2 from Haskell.
+description: Writing and calling ACL2 from Haskell.
+
+author:     Tom Hawkins  <tomahawkins@gmail.com>
+maintainer: Tom Hawkins  <tomahawkins@gmail.com>
+
+license: BSD3
+license-file: LICENSE
+
+build-type:    Simple
+cabal-version: >= 1.9.2
+
+library
+  build-depends:
+    base     >= 4.0 && < 6.0,
+    process  >= 1.0 && < 2.0
+  exposed-modules:
+    Language.ACL2
+  ghc-options: -W
+
+source-repository head
+  type:     git
+  location: git://github.com/tomahawkins/acl2.git
+