diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,27 @@
+Copyright (c) Tom Hawkins 2010
+
+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. Neither the name of the author nor the names of his contributors
+   may be used to endorse or promote products derived from this software
+   without specific prior written permission.
+
+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/LTL.hs b/Language/LTL.hs
new file mode 100644
--- /dev/null
+++ b/Language/LTL.hs
@@ -0,0 +1,65 @@
+-- | Using linear temporal logic (LTL) to verify embedded software and hardware.
+module Language.LTL
+  (
+  -- * Formula Combinators
+    N, B, R, F, E
+  -- * Verification Directives
+  , Directive (..)
+  , checkVCD
+  ) where
+
+import Data.VCD
+
+data N -- Number phantom type.
+data B -- Boolean phantom type.
+data R -- Regular expression phantom type.
+data F -- Formula phantom type.
+
+-- | Class of booleans or formulas.
+class BF a
+instance BF B
+instance BF F
+
+-- | Class of booleans or regular expressions.
+class BR a
+instance BR B
+instance BR R
+
+-- | Class of numbers or booleans.
+class NB a
+instance NB N
+instance NB B
+
+-- | LTL (and other) expressions.
+data E a where
+  Var      :: NB a => [String] -> E a
+  Add      :: E N -> E N -> E N
+  Sub      :: E N -> E N -> E N
+  Mul      :: E N -> E N -> E N
+  Eq       :: NB a => E a -> E a -> E B
+  Lt       :: E N -> E N -> E B
+  Sequence :: (BR a, BR b) => E a -> E b -> E R
+  Infusion :: (BR a, BR b) => E a -> E b -> E R
+  Not      :: BF a => E a -> E a
+  And      :: E a -> E a -> E a
+  Or       :: E a -> E a -> E a
+  Empty    :: E R
+  Many     :: BR a => E a -> E R
+  Formula' :: BR a => E a -> E F
+  Formula  :: BR a => E a -> E F
+  Next'    :: E F -> E F
+  Until'   :: E F -> E F -> E F
+  Imply    :: E R -> E F
+
+-- | Verification directives.
+data Directive
+  = Assert String (E F)  -- ^ Property must be true.
+  | Assume String (E F)  -- ^ Property is assumed to be true.  Becomes an assertion in simulation.
+  | Cover  String (E R)  -- ^ Sequence must be excited.
+
+-- | Check VCD data against a set of verification directives.  Returns a list of violations with time of failure (Just: safety violation, Nothing: liveness violation).
+checkVCD :: String -> Int -> [Directive] -> [(Directive, Maybe Int)]
+checkVCD vcd period formulas = []
+  where
+  VCD _ defs samples = parseVCD vcd
+
diff --git a/Setup.lhs b/Setup.lhs
new file mode 100644
--- /dev/null
+++ b/Setup.lhs
@@ -0,0 +1,8 @@
+#! /usr/bin/env runhaskell
+
+> module Main (main) where
+>
+> import Distribution.Simple (defaultMain)
+>
+> main :: IO ()
+> main = defaultMain
diff --git a/ltl.cabal b/ltl.cabal
new file mode 100644
--- /dev/null
+++ b/ltl.cabal
@@ -0,0 +1,39 @@
+name:    ltl
+version: 0.0.0
+
+category: Language
+
+synopsis: Using linear temporal logic (LTL) to verify embedded software and hardware.
+
+description:
+  TODO
+
+author:     Tom Hawkins <tomahawkins@gmail.com>
+maintainer: Tom Hawkins <tomahawkins@gmail.com>
+
+license:      BSD3
+license-file: LICENSE
+
+homepage: http://tomahawkins.org
+
+build-type:    Simple
+cabal-version: >= 1.6
+
+library
+    build-depends:
+        base       >= 4.2 && < 5,
+        vcd        >= 0.1
+
+    exposed-modules:
+        Language.LTL
+
+    extensions: GADTs, EmptyDataDecls
+
+    if impl(ghc > 6.8)
+          ghc-options: -fwarn-tabs
+    ghc-options:       -W
+
+source-repository head
+    type:     git
+    location: git://github.com/tomahawkins/ltl.git
+