diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2014, Shohei Yasutake
+
+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 Shohei Yasutake 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/prove-everywhere-server.cabal b/prove-everywhere-server.cabal
new file mode 100644
--- /dev/null
+++ b/prove-everywhere-server.cabal
@@ -0,0 +1,40 @@
+-- Initial prove-everywhere-server.cabal generated by cabal init.  For
+-- further documentation, see http://haskell.org/cabal/users-guide/
+
+name:                prove-everywhere-server
+version:             0.1
+synopsis:            The server for ProveEverywhere
+description:         This is the server for ProveEverywhere project.
+homepage:            https://github.com/amutake/prove-everywhere
+license:             BSD3
+license-file:        LICENSE
+author:              Shohei Yasutake
+maintainer:          amutake.s@gmail.com
+-- copyright:
+category:            Web
+build-type:          Simple
+-- extra-source-files:
+cabal-version:       >=1.10
+
+executable prove-everywhere-server
+  main-is:             Main.hs
+  -- other-modules:
+  -- other-extensions:
+  build-depends:       base == 4.*
+                     , warp == 3.0.*
+                     , wai == 3.0.*
+                     , optparse-applicative == 0.9.*
+                     , process == 1.2.*
+                     , bytestring == 0.10.*
+                     , unordered-containers == 0.2.*
+                     , http-types == 0.8.*
+                     , aeson == 0.7.*
+                     , text == 1.1.*
+                     , parsers == 0.11.*
+                     , parsec == 3.1.*
+                     , safe == 0.3.*
+                     , time == 1.4.*
+                     , case-insensitive >= 0.2
+  hs-source-dirs:      src
+  default-language:    Haskell2010
+  ghc-options:         -Wall
diff --git a/src/Main.hs b/src/Main.hs
new file mode 100644
--- /dev/null
+++ b/src/Main.hs
@@ -0,0 +1,58 @@
+
+module Main where
+
+import Control.Exception
+import Options.Applicative
+import System.Process
+
+import ProveEverywhere.Types
+import ProveEverywhere.Server
+
+main :: IO ()
+main = do
+    config <- execParser opts
+    result <- getCoqtopVersion
+    case result of
+        Nothing -> putStrLn "coqtop not found"
+        Just (n, m, p) | (n, m, p) < (8, 4, 0) -> do
+            putStrLn $ concat
+                [ "coqtop (" ++ show n ++ "." ++ show m ++ "pl" ++ show p ++ ") found\n"
+                , "but this server does not support this version"
+                ]
+        Just (n, m, p) -> do
+            putStrLn $ "coqtop (" ++ show n ++ "." ++ show m ++ "pl" ++ show p ++ ") found"
+            putStrLn $ "Server started on port " ++ show (configPort config)
+            runServer config
+  where
+    opts = info (helper <*> configParser) $
+        fullDesc <> header "prove-everywhere-server - The server for ProveEverywhere"
+
+configParser :: Parser Config
+configParser = Config
+    <$> option (long "port" <>
+                short 'p' <>
+                metavar "PORT" <>
+                help "Specify port number")
+    <*> optional (option
+                  (long "number" <>
+                   short 'n' <>
+                   metavar "NUM_OF_PROCS" <>
+                   help "Max number of coqtop processes (default: infinity)"))
+    <*> optional (option
+                  (long "time" <>
+                   short 't' <>
+                   metavar "KILL_TIME" <>
+                   help "The time to terminate unused coqtop process (unit of time: minute) (default: infinity)"))
+
+getCoqtopVersion :: IO (Maybe (Int, Int, Int)) -- e.g., (8, 4, 4) = 8.4pl4
+getCoqtopVersion = handle failure $ do
+    v_all <- readProcess "coqtop" ["-v"] ""
+    let [n_str, '.', m_str, 'p', 'l', p_str]
+            = drop (length "The Coq Proof Assistant, version ")
+            . take (length "The Coq Proof Assistant, version *.*pl*")
+            $ v_all
+    let (n, m, p) = (read [n_str], read [m_str], read [p_str])
+    return (Just (n, m, p))
+  where
+    failure :: IOError -> IO (Maybe (Int, Int, Int))
+    failure _ = return Nothing