diff --git a/PTQ.cabal b/PTQ.cabal
--- a/PTQ.cabal
+++ b/PTQ.cabal
@@ -1,5 +1,5 @@
 Name:            PTQ
-Version:         0.0.4
+Version:         0.0.5
 License:         LGPL
 License-File:    COPYING
 Author:          Masahiro Sakai
@@ -29,18 +29,18 @@
   Main-Is: Main.hs
   Hs-Source-Dirs: src
   Other-Modules:
-     Expr
+     IL
      P
      Translation
      Parser
      Report
+     Version
   Extensions:
      EmptyDataDecls
      GADTs
      MultiParamTypeClasses
      TypeOperators
      TypeSynonymInstances
-     GeneralizedNewtypeDeriving
   Build-Depends: base >=4 && <5, haskell98, mtl, containers
   if flag(UTF8Terminal)
     CPP-Options: "-DUSE_UTF8"
@@ -50,11 +50,12 @@
   Main-Is: CGIMain.hs
   Hs-Source-Dirs: src
   Other-Modules:
-     Expr
+     IL
      P
      Translation
      Parser
-     Report
+     Version
+     ReportHTML
      CGI
      URLEncoding
   Extensions:
@@ -63,9 +64,8 @@
      MultiParamTypeClasses
      TypeOperators
      TypeSynonymInstances
-     GeneralizedNewtypeDeriving
      CPP
-  Build-Depends: base >=4 && <5, haskell98, mtl, containers, network
+  Build-Depends: base >=4 && <5, haskell98, mtl, containers, network, xml
   if flag(UTF8CGI)
     CPP-Options: "-DUSE_UTF8"
     Build-Depends: utf8-string
diff --git a/README b/README
--- a/README
+++ b/README
@@ -34,9 +34,8 @@
   PTQ> quit
   %
 
-== Simple CGI interface
+== CGI interface
 
 By locating ptq.cgi, cgi/index.html and cgi/main.html to the place
 where CGI is executable, you can try it on the web.
-
-Currenly it also runs at ((<URL:http://www.tom.sfc.keio.ac.jp/~sakai/hsPTQ/>)).
+Demo site runs at <http://www.tom.sfc.keio.ac.jp/~sakai/hsPTQ/>.
diff --git a/src/CGIMain.hs b/src/CGIMain.hs
--- a/src/CGIMain.hs
+++ b/src/CGIMain.hs
@@ -9,7 +9,8 @@
 -- Portability :  portable
 
 module Main where
-import Report
+
+import ReportHTML
 import CGI
 import Control.Concurrent
 
@@ -26,4 +27,5 @@
     Nothing ->
 	HTTPResponse (textContentType "text/plain" "us-ascii") "(no input)\n"
     Just s  ->
-	HTTPResponse (textContentType "text/plain" "utf-8") (report s)
+	--HTTPResponse (textContentType "text/plain" "utf-8") (report s)
+        HTTPResponse (textContentType "text/html" "utf-8") (report s)
diff --git a/src/Expr.hs b/src/Expr.hs
deleted file mode 100644
--- a/src/Expr.hs
+++ /dev/null
@@ -1,246 +0,0 @@
------------------------------------------------------------------------------
--- |
--- Module      :  Expr
--- Copyright   :  (c) Masahiro Sakai 2007-2009
--- License     :  BSD3-style (see LICENSE)
--- 
--- Maintainer:    masahiro.sakai@gmail.com
--- Stability   :  experimental
--- Portability :  non-portable
-
-{-# LANGUAGE CPP, GeneralizedNewtypeDeriving #-}
-module Expr
-    ( Op1 (..)
-    , Op2 (..)
-    , Binder (..)
-    , Expr (..)
-    , Scope (..)
-    , Name
-    , lambda
-    , forall
-    , exists
-    , int
-    , ext
-    , (<@>)
-    , abstract
-    , instantiate
-    , normalize
-    , RenderM
-    , runRenderM
-    , renderExpr
-    , renderExprU
-    ) where
-
-import Control.Monad.RWS
-import Data.List
-
------------------------------------------------------------------------------
-
-data Op1 = Not | Box | F | H | Int | Ext deriving (Eq,Show)
-data Op2 = And | Or | Imply | Equiv | Id deriving (Eq,Show)
-data Binder = Lambda | Forall | Exists deriving (Eq,Show)
-
-infixl 9 :@
-
-data Expr
-    = FVar Name          -- 自由変数
-    | BVar !Int          -- 束縛変数
-    | Expr :@ Expr       -- 関数適用
-    | Const String       -- 定数 (≒自由変数)
-    | Op1 !Op1 Expr      -- 前置演算子
-    | Op2 !Op2 Expr Expr -- 中置演算子
-    | Bind !Binder Scope -- 変数束縛
-
-instance Show Expr where
-#ifdef USE_UTF8
-    showsPrec d x = runRenderM (renderExprU d x)
-#else
-    showsPrec d x = runRenderM (renderExpr d x)
-#endif
-
-newtype Scope = Sc Expr deriving Show
-type Name = String
-
------------------------------------------------------------------------------
-
-lambda :: Name -> Expr -> Expr
-lambda name expr = Bind Lambda (abstract name expr)
-
-forall :: Name -> Expr -> Expr
-forall name expr = Bind Forall (abstract name expr)
-
-exists :: Name -> Expr -> Expr
-exists name expr = Bind Exists (abstract name expr)
-
-int :: Expr -> Expr
-int = Op1 Int
-
-ext :: Expr -> Expr
-ext = Op1 Ext
-
--- 「a{b}」を「a <@> b」と表記
-infixl 9 <@>
-(<@>) :: Expr -> Expr -> Expr
-fun <@> arg = ext fun :@ arg
-
------------------------------------------------------------------------------
-
-varChange :: (Int -> Name -> Expr) -> (Int -> Int -> Expr) -> Expr -> Expr
-varChange f g = h 0
-  where
-    h :: Int -> Expr -> Expr
-    h outer (FVar name)  = f outer name
-    h outer (BVar index) = g outer index
-    h outer (Bind q (Sc body)) = Bind q (Sc (h (outer+1) body))
-    h outer (fun :@ arg) = h outer fun :@ h outer arg
-    h _     (Const s)    = Const s
-    h outer (Op1 op a)   = Op1 op (h outer a)
-    h outer (Op2 op a b) = Op2 op (h outer a) (h outer b)
-
-abstract :: Name -> Expr -> Scope
-abstract name expr = Sc (varChange f g expr)
-  where
-    f outer name' | name==name'  = BVar outer
-                  | otherwise    = FVar name'
-    g outer index | index>=outer = BVar (index+1)
-                  | otherwise    = BVar index
-
-instantiate :: Expr -> Scope -> Expr
-instantiate image (Sc body) = varChange f g body
-  where
-    f _ name = FVar name
-    g outer index | index==outer = varShift outer image
-                  | index>outer  = BVar (index-1)
-                  | otherwise    = BVar index
-
--- 外を指している変数のインデックスをずらす
-varShift :: Int -> Expr -> Expr
-varShift 0 = id
-varShift n = varChange f g 
-  where
-    f _ name  = FVar name
-    g outer index | index>=outer = BVar (index+n)
-                  | otherwise    = BVar index
-
-normalize :: Expr -> Expr
-normalize (Bind Lambda (Sc body)) =
-  case normalize body of
-    f :@ BVar 0 | not (0 `elem` bvs f) -> varShift (-1) f -- η-conversion
-    body -> Bind Lambda (Sc body)
-normalize (Bind q (Sc body)) = Bind q (Sc (normalize body))
-normalize (fun :@ arg) =
-  case normalize fun of
-    Bind Lambda body -> normalize (instantiate arg' body) -- β-reduction
-    fun -> fun :@ arg'
-  where arg' = normalize arg
-normalize (Op1 Ext a)  =
-  case normalize a of
-    Op1 Int b -> b
-    a' -> Op1 Ext a'
-normalize (Op1 op a)   = Op1 op (normalize a)
-normalize (Op2 op a b) = Op2 op (normalize a) (normalize b)
-normalize x = x
-
-bvs :: Expr -> [Int]
-bvs (FVar _) = []
-bvs (BVar n) = [n]
-bvs (f :@ x) = bvs f ++ bvs x
-bvs (Const _) = []
-bvs (Op1 _ e) = bvs e
-bvs (Op2 _ e1 e2) = bvs e1 ++ bvs e2
-bvs (Bind b (Sc e)) = [n - 1 | n <- bvs e, n /= 0]
-
------------------------------------------------------------------------------
-
-newtype RenderM a = RenderM (RWS [Name] () Int a)
-  deriving (Monad, MonadReader [Name])
-
-runRenderM :: RenderM a -> a
-runRenderM (RenderM m) = 
-  case runRWS m [] 0 of
-    (a, _, _) -> a
-
-render :: Bool -> Int -> Expr -> RenderM ShowS
-render u = h
-  where
-    h d e = case e of
-      FVar name  -> return $ showString name
-      BVar index -> do
-        vs <- ask
-        return $ showString (vs !! index)
-      Bind q _ -> f d q e
-      Op1 Ext a :@ b -> do
-        a' <- h (app_prec+1) a
-        b' <- h 0 b
-        return $ showParen (d > app_prec)
-               $ a' . showString " {" . b' . showChar '}'
-      a :@ b  -> do 
-        a' <- h app_prec a
-        b' <- h (app_prec+1) b
-        return $ showParen (d > app_prec) $ a' . showChar ' ' . b'
-      Const s -> return $ showString s
-      Op1 op a -> do
-        t <- h (prec+1) a
-        return $ showParen (d > prec)
-               $ showString s . t
-        where
-          s = case op of
-                Not -> if u then "¬" else "not " -- ¬ (U+00AC)
-                Box -> if u then "◻" else "[]"  -- ◻ (U+25FB) が正しそうだが □ (U+25A1) を使うのが無難か?
-                F   -> "F "
-                H   -> "H "
-                Int -> if u then "˄" else "Int " -- ˄ (U+02C4)
-                Ext -> if u then "˅" else "Ext " -- ˅ (U+02C5)
-          prec = case op of
-                   Int | u -> app_prec + 1
-                   Ext | u -> app_prec + 1
-                   _ -> app_prec
-      Op2 op a b -> do
-        a' <- h (l prec) a
-        b' <- h (r prec) b
-        return $ showParen (d > prec)
-               $ a' . showChar ' ' . showString s . showChar ' ' . b'
-        where
-          (s,prec,l,r) =
-      	    case op of
-              And   -> (if u then "∧" else "&&",  4, id, id)     -- ∧ (U+2227)
-              Or    -> (if u then "∨" else "||",  3, id, id)     -- ∨ (U+2228)
-              Imply -> (if u then "→" else "->",  1, (+1), id)   -- → (U+2192)
-              Equiv -> (if u then "↔" else "<->", 1, (+1), (+1)) -- ↔ (U+2194)
-              Id    -> ("=",   2, (+1), (+1))
-
-    f :: Int -> Binder -> Expr -> RenderM ShowS
-    f d b e = do
-      (xs, s) <- go e
-      return $ showParen (d > 0) $
-        showString (g b) . showString (intercalate " " xs) . showString ". " . s
-      where
-        go :: Expr -> RenderM ([Name], ShowS)
-        go (Bind b' (Sc body)) | b==b' = do
-          x <- gensym 
-          (xs, s) <- local (x:) $ go body
-          return (x:xs, s)
-        go e = do
-          s <- h 0 e
-          return ([], s)
-
-    g :: Binder -> String
-    g Lambda = if u then "λ" else "\\" -- λ (U+03BB)
-    g Forall = if u then "∀" else "forall " -- ∀ (U+2200)
-    g Exists = if u then "∃" else "exists " -- ∃ (U+2203)
-
-
-renderExpr :: Int -> Expr -> RenderM ShowS
-renderExpr = render False
-
-renderExprU :: Int -> Expr -> RenderM ShowS
-renderExprU = render True
-
-app_prec :: Int
-app_prec = 10
-
-gensym :: RenderM Name
-gensym = RenderM $ do 
-    i <- get
-    put (i+1)
-    return ("x"++show i)
diff --git a/src/IL.hs b/src/IL.hs
new file mode 100644
--- /dev/null
+++ b/src/IL.hs
@@ -0,0 +1,319 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  IL
+-- Copyright   :  (c) Masahiro Sakai 2007-2009
+-- License     :  BSD3-style (see LICENSE)
+-- 
+-- Maintainer:    masahiro.sakai@gmail.com
+-- Stability   :  experimental
+-- Portability :  non-portable
+
+{-# LANGUAGE CPP #-}
+module IL
+    ( Type (..)
+    , renderType
+    , Op1 (..)
+    , Op2 (..)
+    , Binder (..)
+    , Expr (..)
+    , Scope (..)
+    , Name
+    , lambda
+    , forall
+    , exists
+    , int
+    , ext
+    , (<@>)
+    , abstract
+    , instantiate
+    , normalize
+    , renderExpr
+    , typeCheck
+    ) where
+
+import Control.Monad.RWS
+import Data.List
+import Data.Monoid
+import Data.Function
+
+-- --------------------------------------------------------------------------
+
+infixr 0 :->
+
+data Type
+  = Prop
+  | E
+  | S Type
+  | (:->) Type Type
+  deriving (Eq, Ord)
+
+instance Show Type where
+#ifdef USE_UTF8
+  showsPrec = renderType True
+#else
+  showsPrec = renderType False
+#endif
+
+renderType :: Bool -> Int -> Type -> ShowS
+renderType unicode = f
+  where
+    f _ Prop = showString "t"
+    f _ E = showString "e"
+    f d (S t) = showParen (d > 0) $ showString "s" . arr . f 0 t
+    f d (t1 :-> t2) = showParen (d > 0) $ f 1 t1 . arr . f 0 t2
+    arr = if unicode then showString "→" else showString "->"
+
+-- --------------------------------------------------------------------------
+
+infixl 9 :@
+
+data Expr
+    = FVar Name          -- 自由変数
+    | BVar !Int          -- 束縛変数
+    | Expr :@ Expr       -- 関数適用
+    | Const Name         -- 定数 (≒自由変数)
+    | Op1 !Op1 Expr      -- 前置演算子
+    | Op2 !Op2 Expr Expr -- 中置演算子
+    | Bind !Binder Type Scope -- 変数束縛
+
+data Op1 = Not | Box | F | H | Int | Ext deriving (Eq,Ord,Show)
+data Op2 = And | Or | Imply | Equiv | Id deriving (Eq,Ord,Show)
+data Binder = Lambda | Forall | Exists deriving (Eq,Ord,Show)
+
+newtype Scope = Sc Expr deriving Show
+type Name = (String, Type)
+
+instance Show Expr where
+#ifdef USE_UTF8
+    showsPrec = renderExpr True False
+#else
+    showsPrec = renderExpr False False
+#endif
+
+lambda :: Name -> Expr -> Expr
+lambda name expr = Bind Lambda (snd name) (abstract name expr)
+
+forall :: Name -> Expr -> Expr
+forall name expr = Bind Forall (snd name) (abstract name expr)
+
+exists :: Name -> Expr -> Expr
+exists name expr = Bind Exists (snd name) (abstract name expr)
+
+int :: Expr -> Expr
+int = Op1 Int
+
+ext :: Expr -> Expr
+ext = Op1 Ext
+
+-- 「a{b}」を「a <@> b」と表記
+infixl 9 <@>
+(<@>) :: Expr -> Expr -> Expr
+fun <@> arg = ext fun :@ arg
+
+varChange :: (Int -> Name -> Expr) -> (Int -> Int -> Expr) -> Expr -> Expr
+varChange f g = h 0
+  where
+    h :: Int -> Expr -> Expr
+    h outer (FVar name)  = f outer name
+    h outer (BVar index) = g outer index
+    h outer (Bind q t (Sc body)) = Bind q t (Sc (h (outer+1) body))
+    h outer (fun :@ arg) = h outer fun :@ h outer arg
+    h _     (Const s)    = Const s
+    h outer (Op1 op a)   = Op1 op (h outer a)
+    h outer (Op2 op a b) = Op2 op (h outer a) (h outer b)
+
+abstract :: Name -> Expr -> Scope
+abstract name expr = Sc (varChange f g expr)
+  where
+    f outer name' | name==name'  = BVar outer
+                  | otherwise    = FVar name'
+    g outer index | index>=outer = BVar (index+1)
+                  | otherwise    = BVar index
+
+instantiate :: Expr -> Scope -> Expr
+instantiate image (Sc body) = varChange f g body
+  where
+    f _ name = FVar name
+    g outer index | index==outer = varShift outer image
+                  | index>outer  = BVar (index-1)
+                  | otherwise    = BVar index
+
+-- 外を指している変数のインデックスをずらす
+varShift :: Int -> Expr -> Expr
+varShift 0 = id
+varShift n = varChange f g 
+  where
+    f _ name  = FVar name
+    g outer index | index>=outer = BVar (index+n)
+                  | otherwise    = BVar index
+
+normalize :: Expr -> Expr
+normalize (Bind Lambda t (Sc body)) =
+  case normalize body of
+    f :@ BVar 0 | not (0 `elem` bvs f) -> varShift (-1) f -- η-conversion
+    body' -> Bind Lambda t (Sc body')
+normalize (Bind q t (Sc body)) = Bind q t (Sc (normalize body))
+normalize (fun :@ arg) =
+  case normalize fun of
+    Bind Lambda t body -> normalize (instantiate arg' body) -- β-reduction
+    fun' -> fun' :@ arg'
+  where arg' = normalize arg
+normalize (Op1 Ext a)  =
+  case normalize a of
+    Op1 Int b -> b
+    a' -> Op1 Ext a'
+normalize (Op1 op a)   = Op1 op (normalize a)
+normalize (Op2 op a b) = Op2 op (normalize a) (normalize b)
+normalize x = x
+
+bvs :: Expr -> [Int]
+bvs (FVar _) = []
+bvs (BVar n) = [n]
+bvs (f :@ x) = bvs f ++ bvs x
+bvs (Const _) = []
+bvs (Op1 _ e) = bvs e
+bvs (Op2 _ e1 e2) = bvs e1 ++ bvs e2
+bvs (Bind _ _ (Sc e)) = [n - 1 | n <- bvs e, n /= 0]
+
+-- --------------------------------------------------------------------------
+
+type RenderM = RWS [Name] () Int
+
+renderExpr :: Bool -> Bool -> Int -> Expr -> ShowS
+renderExpr unicode uncurrying d e =
+  case runRWS (h d e) [] 0 of
+    (a, _, _) -> a
+  where
+    h d e = case e of
+      FVar name  -> return $ showString (fst name)
+      BVar index -> do
+        vs <- ask
+        return $ showString $ fst (vs !! index)
+      Bind q _ _ -> f d q e
+      a :@ b | uncurrying -> f a [b]
+        where
+          f (e1 :@ e2) xs = f e1 (e2:xs)
+          f e xs = uncurriedApp e xs
+      Op1 Ext a :@ b -> do
+        a' <- h (app_prec+1) a
+        b' <- h 0 b
+        return $ showParen (d > app_prec)
+               $ a' . showString " {" . b' . showChar '}'
+      a :@ b  -> do 
+        a' <- h app_prec a
+        b' <- h (app_prec+1) b
+        return $ showParen (d > app_prec) $ a' . showChar ' ' . b'
+      Const s -> return $ showString (fst s)
+      Op1 op a -> do
+        t <- h (prec+1) a
+        return $ showParen (d > prec)
+               $ showString s . t
+        where
+          s = case op of
+                Not -> if unicode then "¬" else "not " -- ¬ (U+00AC)
+                Box -> if unicode then "◻" else "[]"  -- ◻ (U+25FB) が正しそうだが □ (U+25A1) を使うのが無難か?
+                F   -> "F "
+                H   -> "H "
+                Int -> if unicode then "˄" else "Int " -- ˄ (U+02C4)
+                Ext -> if unicode then "˅" else "Ext " -- ˅ (U+02C5)
+          prec = case op of
+                   Int | unicode -> app_prec + 1
+                   Ext | unicode -> app_prec + 1
+                   _ -> app_prec
+      Op2 op a b -> do
+        a' <- h (l prec) a
+        b' <- h (r prec) b
+        return $ showParen (d > prec)
+               $ a' . showChar ' ' . showString s . showChar ' ' . b'
+        where
+          (s,prec,l,r) =
+      	    case op of
+              And   -> (if unicode then "∧" else "&&",  4, id, id)     -- ∧ (U+2227)
+              Or    -> (if unicode then "∨" else "||",  3, id, id)     -- ∨ (U+2228)
+              Imply -> (if unicode then "→" else "->",  1, (+1), id)   -- → (U+2192)
+              Equiv -> (if unicode then "↔" else "<->", 1, (+1), (+1)) -- ↔ (U+2194)
+              Id    -> ("=", 5, (+1), (+1))
+
+    f :: Int -> Binder -> Expr -> RenderM ShowS
+    f d b e = do
+      (xs, s) <- go e
+      let b' = case b of
+            Lambda -> if unicode then "λ" else "\\" -- λ (U+03BB)
+            Forall -> if unicode then "∀" else "forall " -- ∀ (U+2200)
+            Exists -> if unicode then "∃" else "exists " -- ∃ (U+2203)
+          ys :: [(Type, [String])]
+          ys = [(snd (head ys), map fst ys) | ys <- groupBy ((==) `on` snd) xs]
+          ws :: [String]
+          ws = [intercalate ", " zs ++ " : "++ renderType unicode 0 t "" | (t, zs) <- ys]
+      return $ showParen (d > 0) $
+        showString b' . showString (intercalate ", " ws) . showString ". " . s
+      where
+        go :: Expr -> RenderM ([Name], ShowS)
+        go (Bind b' t (Sc body)) | b==b' = do
+          x <- gensym t
+          (xs, s) <- local (x:) $ go body
+          return (x:xs, s)
+        go e = do
+          s <- h 0 e
+          return ([], s)
+
+    uncurriedApp :: Expr -> [Expr] -> RenderM ShowS
+    uncurriedApp e xs = do
+      bs <- mapM (liftM Endo . h 0) $ reverse xs
+      let cs = appEndo $ mconcat $ intersperse (Endo (showString ", ")) bs
+      case e of
+        Op1 Ext e2 -> do
+          a <- h (app_prec+1) e2
+          return $ showParen (d > app_prec)
+                 $ a . showString "{" . cs . showChar '}'
+        _ -> do
+          a <- h (app_prec+1) e
+          return $ showParen (d > app_prec)
+                 $ a . showString "(" . cs . showChar ')'
+
+app_prec :: Int
+app_prec = 10
+
+gensym :: Type -> RenderM Name
+gensym t = do 
+  i <- get
+  put (i+1)
+  return ("x"++show i, t)
+
+-- ---------------------------------------------------------------------------
+
+typeCheck ::[Type] -> Expr -> Maybe Type
+typeCheck = f
+  where
+    f _ (FVar (_,t)) = return t
+    f env (BVar n) = return (env !! n)
+    f env (e1 :@ e2) = do
+      (t1 :-> t2) <- f env e1
+      t3 <- f env e2
+      guard $ t1 == t3
+      return t2
+    f env (Const (_,t)) = return t
+    f env (Op1 Ext e) = do
+      S t <- f env e
+      return t
+    f env (Op1 Int e) = do
+      t <- f env e
+      return (S t)
+    f env (Op1 op e) = do
+      Prop <- f env e
+      return Prop
+    f env (Op2 Id e1 e2) = do
+      t1 <- f env e1
+      t2 <- f env e2
+      guard $ t1 == t2
+      return Prop
+    f env (Op2 op e1 e2) = do
+      Prop <- f env e1
+      Prop <- f env e2
+      return Prop
+    f env (Bind Lambda t (Sc e)) = do
+      t2 <- f (t:env) e
+      return (t :-> t2)
+    f env (Bind b t (Sc e)) = do
+      Prop <- f (t:env) e
+      return Prop
diff --git a/src/MP.hs b/src/MP.hs
--- a/src/MP.hs
+++ b/src/MP.hs
@@ -12,22 +12,38 @@
     ( applyMP
     )
     where
-import Expr
+import P
+import IL
+import Translation (catToType)
 
 applyMP :: Expr -> Expr
 -- MP1
 -- MP4
-applyMP (Const tv) | tv `elem` ["find","lose","eat","love"] =
-    lambda "p" $ lambda "x" $
-    FVar "p" <@> (int $ lambda "y" $ Const tv :@ int (lambda "P" $ FVar "P" <@> FVar "y") :@ FVar "x")
+applyMP (Const tv) | fst tv `elem` ["find","lose","eat","love"] =
+    lambda p $ lambda x $
+    FVar p <@> (int $ lambda y $ int (Const tv') <@> FVar y :@ FVar x)
+  where
+    tv' = (fst tv ++ "*", E :-> E :-> Prop)
+    p = ("p", S ((S (E :-> Prop)) :-> Prop))
+    x = ("x", E)
+    y = ("y", E)
 -- MP8
-applyMP (Const "in") =
-    lambda "p" $ lambda "P" $ lambda "x" $
-    FVar "p" <@> (int $ lambda "y" $ Const "in" :@ int (lambda "z" $ FVar "z" <@> FVar "y") :@ FVar "P" :@ FVar "x")
+applyMP (Const ("in",_)) =
+    lambda p $ lambda pp $ lambda x $
+    FVar p <@> (int $ lambda y $ int (Const in') <@> FVar y :@ FVar pp :@ FVar x)
+  where
+    in' = ("in*", E :-> (S (E :-> Prop)) :-> E :-> Prop)
+    p = ("p", S ((S (E :-> Prop)) :-> Prop))
+    pp = ("P", S (E :-> Prop))
+    x = ("x", E)
+    y = ("y", E)
 -- MP9
-applyMP (Const "seek") = lambda "P" $ Const "try" :@ int (find' :@ FVar "P")
-    where find' = applyMP (Const "find")
-applyMP (Bind q (Sc body)) = Bind q (Sc (applyMP body))
+applyMP (Const ("seek",_)) = lambda p $ Const try' :@ int (find' :@ FVar p)
+  where
+    try' = ("try", catToType (IV :// IV))
+    find' = applyMP (Const ("find", catToType (cat :: Cat TV)))
+    p = ("P", S ((S (E :-> Prop)) :-> Prop))
+applyMP (Bind q t (Sc body)) = Bind q t (Sc (applyMP body))
 applyMP (fun :@ arg) = applyMP fun :@ applyMP arg
 applyMP (Op1 op a)   = Op1 op (applyMP a)
 applyMP (Op2 op a b) = Op2 op (applyMP a) (applyMP b)
diff --git a/src/Main.hs b/src/Main.hs
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -11,26 +11,34 @@
 {-# LANGUAGE CPP #-}
 module Main where
 import Report
+import Version
 #ifdef USE_UTF8
-import Prelude hiding (putStr, getLine)
-import System.IO hiding (putStr, getLine)
+import Prelude hiding (putStr, putStrLn, getLine)
+import System.IO (stdout, hSetBuffering, BufferMode (..))
 import System.IO.UTF8
 #else
 import System.IO
 #endif
 
 main :: IO ()
-main =
-    do -- FIXME: バナーを表示
-       hSetBuffering stdout NoBuffering
-       loop
+main = do
+  putStrLn banner
+  hSetBuffering stdout NoBuffering
+  loop
 
+banner :: String
+banner = unlines
+  [ "PTQ version " ++ versionStr
+  , ""
+  , "Type :quit to quit"
+  ]
+
 loop :: IO ()
-loop = 
-    do putStr "PTQ> "
-       s <- getLine
-       case s of
-        "quit" -> return ()
-	_ -> do 
-	    putStr (report s)
-	    loop
+loop = do
+  putStr "PTQ> "
+  s <- getLine
+  case s of
+    ":quit" -> return ()
+    _ -> do
+      putStr (report s)
+      loop
diff --git a/src/P.hs b/src/P.hs
--- a/src/P.hs
+++ b/src/P.hs
@@ -19,33 +19,24 @@
   , (:/)
   , (://)
   , Cat (..)
-  , cat_Sen
-  , cat_IV
-  , cat_CN
-  , cat_Adj
+  , CatType (..) 
   , T
   , TV
   , IAV
-  , cat_T
-  , cat_TV
-  , cat_IAV
   , Det
   , DTV
   , TTV
   , PP
-  , cat_Det
-  , cat_DTV
-  , cat_PP
   , PronounNo
   , P (..)
   , PAny (..)
   , F5
   , F6
-  , F8 (..)
-  , F9 (..)
-  , F10 (..)
+  , F8
+  , F9
+  , F10
+  , catOf
   ) where
-import Expr
 
 -----------------------------------------------------------------------------
 
@@ -68,26 +59,39 @@
     Adj   :: Cat Adj
     (:/)  :: Cat a -> Cat b -> Cat (a :/ b)
     (://) :: Cat a -> Cat b -> Cat (a :// b)
-cat_Sen = Sen
-cat_IV  = IV
-cat_CN  = CN
-cat_Adj = Adj
 
+class CatType a where
+  cat :: Cat a
+instance CatType Sen where
+  cat = Sen
+instance CatType IV where
+  cat = IV
+instance CatType CN where
+  cat = CN
+instance CatType Adj where
+  cat = Adj
+instance (CatType a, CatType b) => CatType (a :/ b) where
+  cat = cat :/ cat
+instance (CatType a, CatType b) => CatType (a :// b) where
+  cat = cat :// cat
+
+instance Show (Cat a) where
+  showsPrec _ Sen = showString "t"
+  showsPrec _ IV = showString "IV"
+  showsPrec _ CN = showString "CN"
+  showsPrec _ Adj = showString "Adj"
+  showsPrec d (a :/ b) = showParen (d > 0) $ showsPrec 1 a . showString " / " . showsPrec 1 b
+  showsPrec d (a :// b) = showParen (d > 0) $ showsPrec 1 a . showString " // " . showsPrec 1 b
+
 type T   = Sen :/ IV -- 名詞句, 固有名詞: John, he
 type TV  = IV :/ T   -- 他動詞(句): find
 type IAV = IV :/ IV  -- 動詞句修飾の副詞(句): slowly
-cat_T   = cat_Sen :/ cat_IV
-cat_TV  = cat_IV :/ cat_T
-cat_IAV = cat_IV :/ cat_IV
 
 -- FIXME: 定義が載っていなかった範疇
 type Det = T  :/ CN -- 冠詞
 type DTV = TV :/ T  -- ditransitive verb : 名詞句を２つ取る他動詞
 type TTV = TV :/ T  -- to transitive verb : DTVと名詞句の順序が逆?
 type PP  = IV :/ TV -- prepositional phrase?: by John
-cat_Det = cat_T  :/ cat_CN
-cat_DTV = cat_TV :/ cat_T
-cat_PP  = cat_IV :/ cat_TV
 
 -----------------------------------------------------------------------------
 
@@ -127,29 +131,32 @@
     F25 :: P TV -> P Adj
 
 data PAny where
-    PAny :: P a -> PAny
+    PAny :: CatType c => P c -> PAny
 
-class F5 c 
+class CatType c => F5 c 
 instance F5 IV  -- T5
 instance F5 IAV -- T6
 
-class F6 c a
+class (CatType c, CatType a) => F6 c a
 instance F6 Sen Sen -- T9
 instance F6 IV Adj  -- T18
 
-class F8 c where f8 :: Cat c
-instance F8 Sen where f8 = cat_Sen
-instance F8 IV where f8 = cat_IV
+class CatType c => F8 c
+instance F8 Sen
+instance F8 IV
 
-class F9 c where f9 :: Cat c
-instance F9 Sen where f9 = cat_Sen
-instance F9 IV where f9 = cat_IV
-instance F9 T where f9 = cat_T
+class CatType c => F9 c
+instance F9 Sen
+instance F9 IV
+instance F9 T
 
-class F10 c where f10 :: Cat c
-instance F10 Sen where f10 = cat_Sen
-instance F10 CN where f10 = cat_CN
-instance F10 IV where f10 = cat_IV
+class CatType c => F10 c
+instance F10 Sen
+instance F10 CN
+instance F10 IV
+
+catOf :: CatType c => P c -> Cat c
+catOf _ = cat
 
 -----------------------------------------------------------------------------
 
diff --git a/src/Parser.hs b/src/Parser.hs
--- a/src/Parser.hs
+++ b/src/Parser.hs
@@ -15,7 +15,7 @@
 import Control.Monad
 import qualified Data.IntSet as IS
 
-import P hiding (f8,f9,f10)
+import P
 
 -----------------------------------------------------------------------------
 -- パーサのコア部分
@@ -146,10 +146,10 @@
     do s <- getF10State
        putF10State []
        (x,a) <- localS3 ([(n,g) | (n,g,_,_)<-s]++) p
-       x <- introF10s x
+       x' <- introF10s x
        s' <- getF10State
        putF10State (s'++s)
-       return (x,a)
+       return (x',a)
 
 introF10 :: F10 c => P c -> Parser (P c)
 introF10 x =
@@ -209,12 +209,11 @@
 parseAny :: String -> [PAny]
 parseAny s = concat $
   [ f p_Det, f (liftM fst p_CN), f p_IAV_T, f p_t_t, f p_t, f p_Adj, f p_PP
-  , f p_IAV, f p_PP_T ] ++
-  [ f (p_T x) | x <- [Subject, Object] ] ++
+  , f p_IAV, f p_PP_T, f (p_T [Subject, Object]) ] ++
   [ concat [ f (p_IV x), f (p_TV x), f (p_IV__IV x), f (p_DTV x), f (p_IV_t x)
            , f (p_IV_Adj x)] | x <- vfs ]
   where
-    f :: Parser (P a) -> [PAny]
+    f :: CatType a => Parser (P a) -> [PAny]
     f p = map PAny (parse' p s)
     vfs :: [VerbForm]
     vfs = [VFOrig, VFPastParticiple] ++ [f True | f <- [VFPresent, VFFuture, VFPerfect]]
@@ -241,7 +240,7 @@
 p_Det :: Parser (P Det)
 p_Det =
     do x@(B _ s) <- s1_Det
-       let x' = if s=="an" then B cat_Det "a" else x -- XXX
+       let x' = if s=="an" then B (cat :: Cat Det) "a" else x -- XXX
        -- FIXME: anの場合には次の語が母音で始まるかチェック
        return $ x'
 
@@ -252,25 +251,27 @@
        return (zeta,g)
 
 -- FIXME: 全ての組み合わせを網羅している?
-p_T :: Case -> Parser (P T)
-p_T c = chainr1 (p <|> he_n c) f9 -- S13
+p_T :: [Case] -> Parser (P T)
+p_T cs = chainr1 (p <|> he_n cs) f9 -- S13
     where p = do (x,g) <- s1_T <|> s2
                  return x <|> asPronoun g x
 
 -- He_n
-he_n :: Case -> Parser (P T)
-he_n c =
-    do g <- case c of
-            Subject -> 
-                msum [ token "he"  >> return Masculine
-                     , token "she" >> return Feminine
-                     , token "it"  >> return Neuter
-                     ]
-            Object ->
-                msum [ token "him" >> return Masculine
-                     , token "her" >> return Feminine
-                     , token "it"  >> return Neuter
-                     ]
+he_n :: [Case] -> Parser (P T)
+he_n cs =
+    do g <- mplus
+            (if Subject `elem` cs
+             then msum [ token "he"  >> return Masculine
+                       , token "she" >> return Feminine
+                       , token "it"  >> return Neuter
+                       ]
+             else mzero)
+            (if Object `elem` cs
+             then msum [ token "him" >> return Masculine
+                       , token "her" >> return Feminine
+                       , token "it"  >> return Neuter
+                       ]
+             else mzero)
        xs <- getF10State
        ys <- askS3
        let ns = [(n,g') | (n, g', _, _) <- xs] ++ ys
@@ -409,8 +410,8 @@
     | VFPerfect !Bool  -- 三人称単数現在完了系とその否定形
 
 {-# INLINE verbParser #-}
-verbParser :: Cat c -> [VerbEntry] -> VerbForm -> Parser (P c)
-verbParser cat dict vf =
+verbParser :: CatType c => [VerbEntry] -> VerbForm -> Parser (P c)
+verbParser dict vf =
     do s <- verbParser' dict vf
        return (B cat s)
 
@@ -475,12 +476,12 @@
     ]
 
 {-# INLINE nounParser #-}
-nounParser :: Cat c -> [NounEntry] -> Parser (P c, Gender)
-nounParser c dict =
+nounParser :: CatType c => [NounEntry] -> Parser (P c, Gender)
+nounParser dict =
     do x <- anyToken
        case lookup x dict of
          Nothing -> mzero
-         Just g  -> return (B c x, g)
+         Just g  -> return (B cat x, g)
 
 -----------------------------------------------------------------------------
 -- それ以外の基本表現の辞書とパーサ
@@ -509,8 +510,8 @@
 dict_PP_T = ["by"]
 
 {-# INLINE dictParser #-}
-dictParser :: Cat c -> [String] -> Parser (P c)
-dictParser cat dict =
+dictParser :: CatType c => [String] -> Parser (P c)
+dictParser dict =
     do x <- anyToken
        guard $ x `elem` dict
        return $ B cat x
@@ -519,43 +520,43 @@
 -- 各統語規則のパーサ
 
 s1_IV :: VerbForm -> Parser (P IV)
-s1_IV = verbParser cat_IV dict_IV
+s1_IV = verbParser dict_IV
 
 s1_TV :: VerbForm -> Parser (P TV)
-s1_TV = verbParser cat_TV dict_TV
+s1_TV = verbParser dict_TV
 
 s1_IV_t :: VerbForm -> Parser (P (IV :/ Sen))
-s1_IV_t = verbParser (cat_IV :/ cat_Sen) dict_IV_t
+s1_IV_t = verbParser dict_IV_t
 
 s1_IV__IV :: VerbForm -> Parser (P (IV :// IV))
-s1_IV__IV = verbParser (cat_IV :// cat_IV) dict_IV__IV
+s1_IV__IV = verbParser dict_IV__IV
 
 s1_IV_Adj :: VerbForm -> Parser (P (IV :/ Adj))
-s1_IV_Adj = verbParser (cat_IV :/ cat_Adj) dict_IV_Adj
+s1_IV_Adj = verbParser dict_IV_Adj
 
 s1_T :: Parser (P T, Gender)
-s1_T = nounParser cat_T dict_T
+s1_T = nounParser dict_T
 
 s1_CN :: Parser (P CN, Gender)
-s1_CN = nounParser cat_CN dict_CN
+s1_CN = nounParser dict_CN
 
 s1_IAV :: Parser (P IAV)
-s1_IAV = dictParser cat_IAV dict_IAV
+s1_IAV = dictParser dict_IAV
 
 s1_t_t :: Parser (P (Sen :/ Sen)) 
-s1_t_t = dictParser (cat_Sen :/ cat_Sen) dict_t_t
+s1_t_t = dictParser dict_t_t
 
 s1_IAV_T :: Parser (P (IAV :/ T))
-s1_IAV_T = dictParser (cat_IAV :/ cat_T) dict_IAV_T
+s1_IAV_T = dictParser dict_IAV_T
 
 s1_Adj :: Parser (P Adj)
-s1_Adj = dictParser cat_Adj dict_Adj
+s1_Adj = dictParser dict_Adj
 
 s1_Det :: Parser (P Det)
-s1_Det = dictParser cat_Det dict_Det
+s1_Det = dictParser dict_Det
 
 s1_PP_T :: Parser (P (PP :/ T))
-s1_PP_T = dictParser (cat_PP :/ cat_T) dict_PP_T
+s1_PP_T = dictParser dict_PP_T
 
 s2 :: Parser (P T, Gender)
 s2 =
@@ -579,7 +580,7 @@
 
 s4_or_s17 :: Parser (P Sen)
 s4_or_s17 =
-    do alpha <- p_T Subject
+    do alpha <- p_T [Subject]
        msum [ do delta <- p_IV (VFPresent True)
                  return (F4 alpha delta) -- 三人称単数現在形 (S4)
             , do delta <- p_IV (VFPresent False) 
@@ -597,13 +598,13 @@
 s5 :: VerbForm -> Parser (P IV)
 s5 vf =
     do delta <- p_TV vf
-       beta  <- p_T Object
+       beta  <- p_T [Object]
        return (F5 delta beta)
 
 s6 :: Parser (P IAV)
 s6 =
     do delta <- p_IAV_T
-       beta <- p_T Object
+       beta <- p_T [Object]
        return (F5 delta beta)
 
 s7 :: VerbForm -> Parser (P IV)
@@ -656,13 +657,13 @@
 s20 vf =
     do delta <- p_DTV vf
        token "to"
-       beta <- p_T Object
+       beta <- p_T [Object]
        return (F20 delta beta)
 
 s21 :: VerbForm -> Parser (P TV)
 s21 vf =
     do delta <- p_DTV vf
-       beta <- p_T Object
+       beta <- p_T [Object]
        return (F21 delta beta)
 
 -- FIXME: この規則はどこからも使われていないけど良いのだろうか?
@@ -683,7 +684,7 @@
 s24 :: Parser (P PP)
 s24 =
     do alpha <- p_PP_T
-       beta <- p_T Object
+       beta <- p_T [Object]
        return (F24 alpha beta)
 
 s25 :: Parser (P Adj)
diff --git a/src/Report.hs b/src/Report.hs
--- a/src/Report.hs
+++ b/src/Report.hs
@@ -9,12 +9,12 @@
 -- Portability :  portable
 
 module Report (report) where
-import Expr
+import IL
 import P
 import Parser
 import MP
 import Translation
-import List (intersperse)
+import Data.List (intersperse)
 
 report :: String -> String
 report s = unlines $
@@ -26,20 +26,26 @@
 f (PAny p) = 
     [ "Parsed:"
     , "  " ++ show p
+    , "  : " ++ show c
     , ""
     , "Translation:"
     , "  " ++ show e
+    , "  : " ++ show t
     , ""
     , "Translation (simplified):"
     , "  " ++ show e'
+    , "  : " ++ show t
     , ""
     , "Translation (MP applied):"
     , "  " ++ show e''
+    , "  : " ++ show t
     ]
     where
       e   = translate p
       e'  = normalize e
       e'' = normalize $ applyMP $ e'
+      c = catOf p
+      t = catToType c
 
 sep :: String
 sep = "------------------------------------------------------"
diff --git a/src/ReportHTML.hs b/src/ReportHTML.hs
new file mode 100644
--- /dev/null
+++ b/src/ReportHTML.hs
@@ -0,0 +1,76 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  ReportHTML
+-- Copyright   :  (c) Masahiro Sakai 2009
+-- License     :  BSD3-style (see LICENSE)
+-- 
+-- Maintainer:    masahiro.sakai@gmail.com
+-- Stability   :  experimental
+-- Portability :  portable
+
+module ReportHTML (report) where
+import IL
+import P
+import Parser
+import MP
+import Translation
+import Data.List (intersperse)
+import Text.XML.Light
+
+report :: String -> String
+report s = showTopElement $ html [hd (title ("Result of \"" ++ s ++ "\"")), body b]
+  where
+    b = case parseAny s of
+          [] -> [p "(parse error)"]
+          ps -> intersperse sep (map f ps)
+
+f :: PAny -> Element
+f (PAny p) = dl
+    [ dt "Parsed"
+    , dd (show p ++ " : " ++ show c)
+    , dt "Translation"
+    , dd (show e ++ " : " ++ show t)
+    , dt "Translation (simplified)"
+    , dd (show e' ++ " : " ++ show t)
+    , dt "Translation (MP applied)"
+    , dd (show e'' ++ " : " ++ show t)
+    ]
+    where
+      e   = translate p
+      e'  = normalize e
+      e'' = normalize $ applyMP $ e'
+      c = catOf p
+      t = catToType c
+
+html :: Node t => t -> Element
+html c = add_attr (Attr xmlns ns) $ node QName{ qName = "html", qURI = Just ns, qPrefix = Nothing } c
+
+xmlns :: QName
+xmlns = QName{ qName = "xmlns", qURI = Nothing, qPrefix = Nothing}
+
+ns :: String
+ns = "http://www.w3.org/1999/xhtml"
+
+hd :: Node t => t -> Element
+hd = node QName{ qName = "head", qURI = Just ns, qPrefix = Nothing }
+
+title :: Node t => t -> Element
+title = node QName{ qName = "title", qURI = Just ns, qPrefix = Nothing }
+
+body :: Node t => t -> Element
+body = node QName{ qName = "body", qURI = Just ns, qPrefix = Nothing }
+
+p :: Node t => t -> Element
+p = node QName{ qName = "p", qURI = Just ns, qPrefix = Nothing }
+
+dl :: Node t => t -> Element
+dl = node QName{ qName = "dl", qURI = Just ns, qPrefix = Nothing }
+
+dt :: Node t => t -> Element
+dt = node QName{ qName = "dt", qURI = Just ns, qPrefix = Nothing }
+
+dd :: Node t => t -> Element
+dd = node QName{ qName = "dd", qURI = Just ns, qPrefix = Nothing }
+
+sep :: Element
+sep = node QName{ qName = "hr", qURI = Just ns, qPrefix = Nothing } ()
diff --git a/src/Translation.hs b/src/Translation.hs
--- a/src/Translation.hs
+++ b/src/Translation.hs
@@ -10,29 +10,32 @@
 
 {-# LANGUAGE TypeOperators, GADTs, TypeSynonymInstances, ScopedTypeVariables #-}
 
-module Translation (translate) where
+module Translation (translate, catToType) where
 
-import Expr
+import IL
 import P
 
 -----------------------------------------------------------------------------
--- Exprも型付きにしたいなぁ
 
 {-
-data E    -- e
-data S    -- s
-data Prop -- t
--- 関数型はHaskellの -> をそのまま使う
-
 -- 範疇から型への対応
 type family Translate x
 type instance Translate Sen = Prop
 type instance Translate IV = E -> Prop
 type instance Translate CN = E -> Prop
+type instance Translate Adj = E -> Prop
 type instance Translate (a :/ b) = ((S -> Translate b) -> Translate a)
 type instance Translate (a :// b) = ((S -> Translate b) -> Translate a)
 -}
 
+catToType :: Cat c ->  Type
+catToType Sen = Prop
+catToType IV = E :-> Prop
+catToType CN = E :-> Prop
+catToType Adj = E :-> Prop -- これで本当にあっている?
+catToType (a :/ b) = (S (catToType b)) :-> catToType a
+catToType (a :// b) = (S (catToType b)) :-> catToType a
+
 -----------------------------------------------------------------------------
 
 translate :: forall c. P c -> Expr
@@ -41,16 +44,24 @@
 --- 2. be → λp.λx. p{f^λy.[x = y]}.
 ---    ここで，変数pのタイプは<s, <<s, <e, t>>, t>>.
 translate (B (IV :/ (Sen :/ IV)){- TV -} "be") =
-    lambda "p" $ lambda "x" $ 
-    FVar "p" <@>
-    int (lambda "y" $ Op2 Id (FVar "x") (FVar "y"))
+  lambda p $ lambda x $ 
+    FVar p <@> int (lambda y $ Op2 Id (FVar x) (FVar y))
+  where
+    p = ("p", S (S (E :-> Prop) :-> Prop))
+    x = ("x", E)
+    y = ("y", E)
 --- 3. necessarily → λp[□ext p]. ここで，p のタイプは<s, t>とする．
-translate (B (Sen :/ Sen) "necessarily") = lambda "p" $ Op1 Box (ext (FVar "p"))
+translate (B (Sen :/ Sen) "necessarily") = lambda p $ Op1 Box (ext (FVar p))
+  where
+    p = ("p", S Prop)
 --- 4. j, m, b はタイプがe の定数記号，変数P のタイプは<s, <e, t>>とする．
-translate (B (Sen :/ IV){- T -} x) = lambda "p" $ FVar "p" <@> Const x
+translate (B (Sen :/ IV){- T -} x) = lambda p $ FVar p <@> Const (x, E)
+  where
+    p = ("p", S (catToType IV))
 --- 5. he_n → λP. P {x_n}．x_ はタイプe の変数．
-translate (He n) = lambda "p" $ FVar "p" <@> FVar (xn n)
-
+translate (He n) = lambda p $ FVar p <@> FVar (xn n)
+  where
+    p = ("p", S (E :-> Prop))
 translate (F2 delta zeta) = trApp delta zeta -- T2
 translate (F3 n zeta phi) = -- T3
     lambda (xn n) $ Op2 And (translate zeta :@ FVar (xn n)) (translate phi)
@@ -62,20 +73,26 @@
 translate (F6 delta beta)  = trApp delta beta  -- T9
 translate (F7 delta beta)  = trApp delta beta  -- T10
 translate (F8 phi psi) =
-  case f8 :: Cat c of
+  case cat :: Cat c of
     Sen -> Op2 And (translate phi) (translate psi) -- T11a
-    IV -> lambda "x" $ Op2 And (translate phi :@ FVar "x") (translate psi :@ FVar "x") -- T12a
+    IV -> lambda x $ Op2 And (translate phi :@ FVar x) (translate psi :@ FVar x) -- T12a
+  where
+    x = ("x", E)
 translate (F9 phi psi) =
-  case f9 :: Cat c of
+  case cat :: Cat c of
     Sen -> Op2 Or (translate phi) (translate psi) -- T11b
-    IV -> lambda "x" $ Op2 Or (translate phi :@ FVar "x") (translate psi :@ FVar "x") -- T12b
-    Sen :/ IV -> lambda "P" $ Op2 Or (translate phi :@ FVar "P") (translate psi :@ FVar "P") -- T13
+    IV -> lambda x $ Op2 Or (translate phi :@ FVar x) (translate psi :@ FVar x) -- T12b
+      where x = ("x", E)
+    Sen :/ IV -> lambda p $ Op2 Or (translate phi :@ FVar p) (translate psi :@ FVar p) -- T13
+      where p = ("P", S (E :-> Prop))
 -- T14 (講義資料はx_nになるべきところがxになっている)
 translate (F10 n alpha phi) =
-  case f10 :: Cat c of
+  case cat :: Cat c of
     Sen -> translate alpha :@ (int $ lambda (xn n) (translate phi)) -- T14
-    CN -> lambda "y" $ translate alpha :@ int (lambda (xn n) (translate phi :@ FVar "y")) -- T15
-    IV -> lambda "y" $ translate alpha :@ int (lambda (xn n) (translate phi :@ FVar "y")) -- T16
+    CN -> lambda y $ translate alpha :@ int (lambda (xn n) (translate phi :@ FVar y)) -- T15
+    IV -> lambda y $ translate alpha :@ int (lambda (xn n) (translate phi :@ FVar y)) -- T16
+  where
+    y = ("y", E)
 -- T17
 translate (F11 alpha delta) = Op1 Not         $ trApp alpha delta
 translate (F12 alpha delta) =           Op1 F $ trApp alpha delta
@@ -83,56 +100,78 @@
 translate (F14 alpha delta) =           Op1 H $ trApp alpha delta
 translate (F15 alpha delta) = Op1 Not $ Op1 H $ trApp alpha delta
 -- T18 (beの扱い以外はT9と同じ)
-translate (B (IV :/ Adj) "be") =
-    lambda "P" $ lambda "x" $ FVar "P" <@> FVar "x"
+translate (B (IV :/ Adj) "be") = lambda p $ lambda x $ FVar p <@> FVar x
+  where
+    p = ("P", S (E :-> Prop))
+    x = ("x", E)
 -- T19
 translate (F19 delta) =
-    lambda "x" $ exists "y" $
-           translate delta :@
-             int (lambda "P" (FVar "P" <@> FVar "y")) :@
-             FVar "x"
+  lambda x $ exists y $
+    translate delta :@ int (lambda p (FVar p <@> FVar y)) :@ FVar x
+  where
+    x = ("x", E)
+    p = ("P", S (E :-> Prop))
+    y = ("y", E)
 translate (F20 delta beta) = trApp delta beta -- T20
 translate (F21 delta beta) = trApp delta beta -- T21 (講義資料ではF20を誤って使っている)
 -- T22
 translate (F22 delta) =
-    lambda "P" $ lambda "Q" $ lambda "x" $
-    translate delta :@ FVar "Q" :@ FVar "P" :@ FVar "x"
+  lambda p $ lambda q $ lambda x $
+    translate delta :@ FVar q :@ FVar p :@ FVar x
+  where
+    p = ("P", S (catToType (cat :: Cat T)))
+    q = ("Q", S (catToType (cat :: Cat T)))
+    x = ("x", E)
 translate (F23 alpha delta) = trApp alpha delta -- T23
 translate (F24 alpha beta)  = trApp alpha beta  -- T24
 -- 講義資料のByの解釈は誤り? (型が一致しない)
 translate (B (IV :/ (IV :/ (Sen :/ IV)) :/ (Sen :/ IV)){- PP/T -} "by") = 
-    lambda "P" $ lambda "R" $ lambda "x" $
-        FVar "P" <@>
-        (int $ lambda "y" $
-         FVar "R" <@> int (lambda "Q" $ FVar "Q" <@> FVar "x") :@ FVar "y")
+  lambda p $ lambda r $ lambda x $
+    FVar p <@>
+      (int $ lambda y $ FVar r <@> int (lambda q $ FVar q <@> FVar x) :@ FVar y)
+  where
+    p = ("P", S (catToType (Sen :/ IV)))
+    r = ("R", S (catToType (IV :/ (Sen :/ IV))))
+    x = ("x", E)
+    y = ("y", E)
+    q = ("Q", S (catToType IV))
 -- T25
 translate (F25 delta) =
-    lambda "x" $ exists "y" $ Op1 H $
-        translate delta :@
-        int (lambda "P" $ FVar "P" <@> FVar "x") :@
-        (FVar "y")
+  lambda x $ exists y $ Op1 H $
+    translate delta :@
+      int (lambda p $ FVar p <@> FVar x) :@
+      (FVar y)
+  where
+    x = ("x", E)
+    y = ("y", E)
+    p = ("P", S (catToType IV))
 
 -- Det
 translate (B (Sen :/ IV :/ CN) s) =
-    case s of
+  case s of
     "a"   ->
-        lambda "p" $ lambda "q" $ exists "x" $
-        Op2 And (FVar "p" <@> FVar "x") (FVar "q" <@> FVar "x")
+      lambda p $ lambda q $ exists x $
+        Op2 And (FVar p <@> FVar x) (FVar q <@> FVar x)
     "the" ->
-        lambda "p" $ lambda "q" $ exists "y" $ forall "x" $
+      lambda p $ lambda q $ exists y $ 
         Op2 And
-          (Op2 Equiv (FVar "p" <@> FVar "x") (Op2 Id (FVar "x") (FVar "y")))
-          (FVar "q" <@> FVar "x")
+          (forall x $ Op2 Equiv (FVar p <@> FVar x) (Op2 Id (FVar x) (FVar y)))
+          (FVar q <@> FVar y)
     "every" ->
-        lambda "p" $ lambda "q" $ forall "x" $
-        Op2 Imply (FVar "p" <@> FVar "x") (FVar "q" <@> FVar "x")
+      lambda p $ lambda q $ forall x $
+        Op2 Imply (FVar p <@> FVar x) (FVar q <@> FVar x)
     "no" ->
-        lambda "p" $ lambda "q" $ forall "x" $
-        Op1 Not (Op2 And (FVar "p" <@> FVar "x") (FVar "q" <@> FVar "x"))
-    _ -> Const s
+      lambda p $ lambda q $ forall x $
+        Op1 Not (Op2 And (FVar p <@> FVar x) (FVar q <@> FVar x))
+    _ -> Const (s, catToType (cat :: Cat Det))
+  where
+    p = ("p", S (E :-> Prop))
+    q = ("q", S (E :-> Prop))
+    x = ("x", E)
+    y = ("y", E)
 
 -- それ以外
-translate (B _ x) = Const x
+translate (B c x) = Const (x, catToType c)
 
 -- ユーティリティ
 trApp :: P (b :/ a) -> P a -> Expr
@@ -141,5 +180,5 @@
 trApp' f a = translate f :@ (int (translate a))
 
 xn :: Int -> Name
-xn n = "he_"++show n
+xn n = ("he_"++show n, E)
 
diff --git a/src/Version.hs b/src/Version.hs
new file mode 100644
--- /dev/null
+++ b/src/Version.hs
@@ -0,0 +1,4 @@
+module Version where
+
+versionStr :: String
+versionStr = "0.0.5"