diff --git a/FVL/Algebra.hs b/FVL/Algebra.hs
new file mode 100644
--- /dev/null
+++ b/FVL/Algebra.hs
@@ -0,0 +1,37 @@
+{-# LANGUAGE FlexibleInstances #-}
+
+module FVL.Algebra
+( Algebra
+, MAlgebra
+, Fix(..)
+, LazyFix(..)
+, cata
+, lazyCata
+, mcata
+, lazyMCata
+) where
+
+type Algebra f a = f a -> a
+type MAlgebra m f a = f (m a) -> m a
+
+newtype Fix f = Fx (f (Fix f))
+newtype LazyFix f = Fx' (f (LazyFix f) (LazyFix f))
+
+unFix :: Fix f -> f (Fix f)
+unFix (Fx x) = x
+
+lazyUnFix :: LazyFix f -> f (LazyFix f) (LazyFix f)
+lazyUnFix (Fx' x) = x
+
+cata :: Functor f => Algebra f a -> Fix f -> a
+cata alg = alg . fmap (cata alg) . unFix
+
+lazyCata :: Functor (f (LazyFix f)) => Algebra (f (LazyFix f)) a -> LazyFix f -> a
+lazyCata alg = alg . fmap (lazyCata alg) . lazyUnFix
+
+mcata :: Functor f => MAlgebra m f a -> Fix f -> m a
+mcata alg = alg . fmap (mcata alg) . unFix
+
+lazyMCata :: Functor (f (LazyFix f)) => MAlgebra m (f (LazyFix f)) a -> LazyFix f -> m a
+lazyMCata alg = alg . fmap (lazyMCata alg) . lazyUnFix
+
diff --git a/FVL/EF.hs b/FVL/EF.hs
new file mode 100644
--- /dev/null
+++ b/FVL/EF.hs
@@ -0,0 +1,116 @@
+module FVL.EF
+( F.Result(..)
+, Expr(..)
+, showTranslation
+, run
+, ParseError
+, parseRun
+, parseFileRun
+) where
+
+import FVL.Algebra
+import qualified FVL.FAST as FAST
+import qualified FVL.F as F
+import FVL.EFAST
+import FVL.Parser
+
+argument :: String -> [String] -> Bool
+argument s [] = False
+argument s (x:xs) = if x == s then True else argument s xs
+
+recursiveAlg :: String -> Algebra FAST.Expr Bool
+recursiveAlg _ (FAST.CInt n) = False
+recursiveAlg _ (FAST.CBool b) = False
+recursiveAlg s (FAST.CVar s') = if s' == s then True else False
+recursiveAlg _ (FAST.Add x y) = x || y
+recursiveAlg _ (FAST.Sub x y) = x || y
+recursiveAlg _ (FAST.Mul x y) = x || y
+recursiveAlg _ (FAST.Div x y) = x || y
+recursiveAlg _ (FAST.And x y) = x || y
+recursiveAlg _ (FAST.Or x y) = x || y
+recursiveAlg _ (FAST.Not x) = x
+recursiveAlg _ (FAST.Equal x y) = x || y
+recursiveAlg _ (FAST.Less x y) = x || y
+recursiveAlg _ FAST.Empty = False
+recursiveAlg _ (FAST.Cons x y) = x || y
+recursiveAlg _ (FAST.If p x y) = p || x || y
+recursiveAlg s (FAST.Function s' p) = if s' == s then False else p
+recursiveAlg _ (FAST.Appl f x) = f || x
+recursiveAlg s (FAST.LetRec f x p e) = if f == s
+    then False
+    else if x == s then p else p || e
+recursiveAlg _ (FAST.Case p x _ _ y) = p || x || y
+
+recursive :: String -> Fix FAST.Expr -> Bool
+recursive s = cata $ recursiveAlg s
+
+createWrapper :: [String] -> Fix FAST.Expr -> Fix FAST.Expr
+createWrapper [] e = e
+createWrapper (x:xs) e = Fx $ FAST.Function x (createWrapper xs e)
+
+letTransform :: String -> Fix FAST.Expr -> Fix FAST.Expr -> Fix FAST.Expr
+letTransform s x y = Fx $ FAST.Appl (Fx $ FAST.Function s y) x
+
+modTransform :: Fix FAST.Expr -> Fix FAST.Expr -> Fix FAST.Expr
+modTransform x y = let y' = Fx $ FAST.Mul y (Fx $ FAST.Div x y)
+    in Fx $ FAST.Sub x y'
+
+lteTransform :: Fix FAST.Expr -> Fix FAST.Expr -> Fix FAST.Expr
+lteTransform x y = Fx $ FAST.Or (Fx $ FAST.Less x y) (Fx $ FAST.Equal x y)
+
+gtTransform :: Fix FAST.Expr -> Fix FAST.Expr -> Fix FAST.Expr
+gtTransform x y = Fx . FAST.Not $ lteTransform x y
+
+gteTransform :: Fix FAST.Expr -> Fix FAST.Expr -> Fix FAST.Expr
+gteTransform x y = Fx . FAST.Not . Fx $ FAST.Less x y
+
+alg :: Algebra Expr (Fix FAST.Expr)
+alg (CInt n) = Fx $ FAST.CInt n
+alg (CBool b) = Fx $ FAST.CBool b
+alg (CVar s) = Fx $ FAST.CVar s
+alg (Add x y) = Fx $ FAST.Add x y
+alg (Sub x y) = Fx $ FAST.Sub x y
+alg (Mul x y) = Fx $ FAST.Mul x y
+alg (Div x y) = Fx $ FAST.Div x y
+alg (Mod x y) = modTransform x y
+alg (And x y) = Fx $ FAST.And x y
+alg (Or x y) = Fx $ FAST.Or x y
+alg (Not x) = Fx $ FAST.Not x
+alg (Equal x y) = Fx $ FAST.Equal x y
+alg (Less x y) = Fx $ FAST.Less x y
+alg (LessEq x y) = lteTransform x y
+alg (Great x y) = gtTransform x y
+alg (GreatEq x y) = gteTransform x y
+alg Empty = Fx FAST.Empty
+alg (Cons x y) = Fx $ FAST.Cons x y
+alg (If p x y) = Fx $ FAST.If p x y
+alg (Function s p) = Fx $ FAST.Function s p
+alg (Appl f x) = Fx $ FAST.Appl f x
+alg (Let f [] p e) = letTransform f p e
+alg (Let f (a:as) p e) = if recursive f p
+    then Fx $ FAST.LetRec f a (createWrapper as p) e
+    else letTransform f (createWrapper (a:as) p) e
+alg (Semi x y) = Fx $ FAST.Appl (Fx $ FAST.Function "_" y) x
+alg (Case p x s t y) = Fx $ FAST.Case p x s t y
+
+translate :: Fix Expr -> Fix FAST.Expr
+translate = cata alg
+
+showTranslation :: Fix Expr -> String
+showTranslation = show . translate
+
+run :: Fix Expr -> F.Result
+run = F.run . translate
+
+parseRun :: String -> Either ParseError F.Result
+parseRun s = case parseString s of
+    Left e -> Left e
+    Right e -> Right $ run e
+
+parseFileRun :: FilePath -> IO (Either ParseError F.Result)
+parseFileRun p = do
+    r <- parseFile p
+    case r of
+        Left e -> return $ Left e
+        Right e -> return . Right $ run e
+
diff --git a/FVL/EFAST.hs b/FVL/EFAST.hs
new file mode 100644
--- /dev/null
+++ b/FVL/EFAST.hs
@@ -0,0 +1,86 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE DeriveFunctor #-}
+
+module FVL.EFAST
+( Expr(..)
+) where
+
+import FVL.Algebra
+
+data Expr a
+    = CInt Integer
+    | CBool Bool
+    | CVar String
+    | Add a a 
+    | Sub a a 
+    | Mul a a 
+    | Div a a 
+    | Mod a a
+    | And a a 
+    | Or a a 
+    | Not a
+    | Equal a a 
+    | Less a a
+    | LessEq a a
+    | Great a a
+    | GreatEq a a
+    | Empty
+    | Cons a a
+    | If a a a 
+    | Function String a
+    | Appl a a 
+    | Let String [String] a a 
+    | Semi a a
+    | Case a a String String a
+    deriving Functor
+
+showCons' :: Fix Expr -> [Fix Expr]
+showCons' (Fx (x `Cons` y)) = x : showCons' y
+showCons' e = [e]
+
+showCons :: Fix Expr -> Fix Expr -> String
+showCons x y = "[" ++ (foldr combine (show x) (showCons' y)) ++ "]"
+    where combine (Fx Empty) b = b
+          combine a b = b ++ ", " ++ show a
+
+instance Show (Fix Expr) where
+    show (Fx (CInt n)) = show n
+    show (Fx (CBool b)) = show b
+    show (Fx (CVar s)) = s
+    show (Fx (x `Add` y)) = show x ++ " + " ++ show y
+    show (Fx (x `Sub` y)) = show x ++ " - " ++ show y
+    show (Fx (x `Mul` y)) = show x ++ " * " ++ show y
+    show (Fx (x `Div` y)) = show x ++ " / " ++ show y
+    show (Fx (x `Mod` y)) = show x ++ " % " ++ show y
+    show (Fx (x `And` y)) = show x ++ " && " ++ show y
+    show (Fx (x `Or` y)) = show x ++ " || " ++ show y
+    show (Fx (Not x)) = "!" ++ (case x of
+        (Fx (CBool b)) -> show b
+        (Fx (CVar s)) -> s
+        _ -> "(" ++ show x ++ ")")
+    show (Fx (x `Equal` y)) = show x ++ " = " ++ show y
+    show (Fx (x `Less` y)) = show x ++ " < " ++ show y
+    show (Fx (x `LessEq` y)) = show x ++ " <= " ++ show y
+    show (Fx (x `Great` y)) = show x ++ " > " ++ show y
+    show (Fx (x `GreatEq` y)) = show x ++ " >= " ++ show y
+    show (Fx Empty) = "[]"
+    show (Fx (x `Cons` y)) = showCons x y
+    show (Fx (If p x y)) = "If " ++ show p ++ " Then " ++ show x ++ " Else " ++ show y
+    show (Fx (Function x p)) = "Function " ++ x ++ " -> " ++ show p
+    show (Fx (Appl f x)) = (case f of
+        (Fx (CInt n)) -> show n ++ " "
+        (Fx (CBool b)) -> show b ++ " "
+        (Fx (CVar s)) -> s ++ " "
+        (Fx (Appl _ _)) -> show f ++ " "
+        _ -> "(" ++ show f ++ ") ") ++ (case x of
+            (Fx (CInt n)) -> show n
+            (Fx (CBool b)) -> show b
+            (Fx (CVar s)) -> s
+            (Fx (Appl _ _)) -> show x
+            _ -> "(" ++ show x ++ ")")
+    show (Fx (Let f a p e))
+        = "Let " ++ f ++ show_args ++ " = " ++ show p ++ " In " ++ show e
+        where show_args = foldr (\x s -> " " ++ x ++ s) "" a
+    show (Fx (Case p x s t y)) = "Case " ++ show x ++ " Of [] -> " ++ show x
+        ++ " | (" ++ s ++ ", " ++ t ++ ") -> " ++ show y
+
diff --git a/FVL/Eval.hs b/FVL/Eval.hs
new file mode 100644
--- /dev/null
+++ b/FVL/Eval.hs
@@ -0,0 +1,101 @@
+module FVL.Eval
+( eval
+) where
+
+import Control.Applicative
+
+import FVL.Algebra
+import FVL.EvalAST
+
+type EvalAlgebra = Algebra (Expr (LazyFix Expr)) (Maybe RVal)
+
+integer_operation :: (Integer -> Integer -> Integer) -> RVal -> RVal -> Maybe RVal
+integer_operation f (RInt x) (RInt y) = Just . RInt $ f x y
+integer_operation _ _ _ = Nothing
+
+boolean_operation :: (Bool -> Bool -> Bool) -> RVal -> RVal -> Maybe RVal
+boolean_operation f (RBool x) (RBool y) = Just . RBool $ f x y
+boolean_operation _ _ _ = Nothing
+
+substitute :: String -> RVal -> LazyFix Expr -> LazyFix Expr
+substitute _ _ (Fx' (CInt n)) = Fx' $ CInt n
+substitute _ _ (Fx' (CBool b)) = Fx' $ CBool b
+substitute s v (Fx' (CVar s')) = if s' == s then valueTransform v else Fx' $ CVar s'
+substitute s v (Fx' (Add x y)) = Fx' $ Add (substitute s v x) (substitute s v y)
+substitute s v (Fx' (Sub x y)) = Fx' $ Sub (substitute s v x) (substitute s v y)
+substitute s v (Fx' (Mul x y)) = Fx' $ Mul (substitute s v x) (substitute s v y)
+substitute s v (Fx' (Div x y)) = Fx' $ Div (substitute s v x) (substitute s v y)
+substitute s v (Fx' (And x y)) = Fx' $ And (substitute s v x) (substitute s v y)
+substitute s v (Fx' (Or x y)) = Fx' $ Or (substitute s v x) (substitute s v y)
+substitute s v (Fx' (Not x)) = Fx' . Not $ substitute s v x
+substitute s v (Fx' (Equal x y)) = Fx' $ Equal (substitute s v x) (substitute s v y)
+substitute s v (Fx' (Less x y)) = Fx' $ Less (substitute s v x) (substitute s v y)
+substitute _ _ (Fx' Empty) = Fx' Empty
+substitute s v (Fx' (Cons x y)) = Fx' $ Cons (substitute s v x) (substitute s v y)
+substitute s v (Fx' (If p x y))
+    = Fx' $ If (substitute s v p) (substitute s v x) (substitute s v y)
+substitute s v (Fx' (Function x p)) = Fx' $ if x == s
+    then Function x p
+    else Function x (substitute s v p)
+substitute s v (Fx' (Appl f x)) = Fx' $ Appl (substitute s v f) (substitute s v x)
+substitute s v (Fx' (LetRec f x p e)) = Fx' $ if f == s
+    then LetRec f x p e
+    else if x == s
+        then LetRec f x p (substitute s v e)
+        else LetRec f x (substitute s v p) (substitute s v e)
+substitute s v (Fx' (Case p x l l' y)) = if l == s || l' == s
+    then Fx' $ Case (substitute s v p) (substitute s v x) l l' y
+    else Fx' $ Case (substitute s v p) (substitute s v x) l l' (substitute s v y)
+
+apply :: RVal -> LazyFix Expr -> Maybe RVal
+apply (RFunction x p) e = eval e >>= \v -> eval $ substitute x v p
+apply _ _ = Nothing
+
+toList :: RVal -> Maybe [RVal]
+toList REmpty = Just []
+toList (RCons x y) = toList y >>= \l -> Just $ x : l
+toList _ = Nothing
+
+toCons :: [RVal] -> RVal
+toCons [] = REmpty
+toCons (x:xs) = RCons x $ toCons xs
+
+alg :: EvalAlgebra
+alg (CInt n) = Just $ RInt n
+alg (CBool b) = Just $ RBool b
+alg (CVar s) = Nothing
+alg (x `Add` y) = x >>= \x' -> y >>= \y' -> integer_operation (+) x' y'
+alg (x `Sub` y) = x >>= \x' -> y >>= \y' -> integer_operation (-) x' y'
+alg (x `Mul` y) = x >>= \x' -> y >>= \y' -> integer_operation (*) x' y'
+alg (x `Div` y) = x >>= \x' -> y >>= \y' -> case y' of
+    (RInt 0) -> Nothing
+    _ -> integer_operation quot x' y'
+alg (x `And` y) = x >>= \x' -> y >>= \y' -> boolean_operation (&&) x' y'
+alg (x `Or` y) = x >>= \x' -> y >>= \y' -> boolean_operation (||) x' y'
+alg (Not x) = x >>= \x' -> case x' of
+    RBool b -> Just . RBool $ not b
+    _ -> Nothing
+alg (x `Equal` y) = x >>= \x' -> y >>= \y' -> case (x', y') of
+    (RInt m, RInt n) -> Just . RBool $ m == n
+    _ -> Nothing
+alg (x `Less` y) = x >>= \x' -> y >>= \y' -> case (x', y') of
+    (RInt m, RInt n) -> Just . RBool $ m < n
+    _ -> Nothing
+alg Empty = Just REmpty
+alg (x `Cons` y) = x >>= \x' -> y >>= \y' -> Just $ RCons x' y'
+alg (If p e1 e2) = p >>= \p' -> case p' of
+    RBool r -> if r then eval e1 else eval e2
+    _ -> Nothing
+alg (Function x p) = Just $ RFunction x p
+alg (Appl f x) = f >>= \f' -> apply f' x
+alg (LetRec f x p e) =
+    let e' = Fx' $ LetRec f x p (Fx' $ Appl (Fx' $ CVar f) (Fx' $ CVar x)) in
+    let r = RFunction x (Fx' $ LetRec f x p e') in
+    let r' = substitute f r p in eval $ substitute f (RFunction x r') e
+alg (Case p x s t y) = p >>= \p' -> toList p' >>= \r -> case r of
+    [] -> eval x
+    (l:ls) -> let y' = substitute s l $ substitute t (toCons ls) y in eval y'
+
+eval :: LazyFix Expr -> Maybe RVal
+eval = lazyCata alg
+
diff --git a/FVL/EvalAST.hs b/FVL/EvalAST.hs
new file mode 100644
--- /dev/null
+++ b/FVL/EvalAST.hs
@@ -0,0 +1,121 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE DeriveFunctor #-}
+
+module FVL.EvalAST
+( Expr(..)
+, RVal(..)
+, valueTransform
+, showCons
+, evalTransform
+) where
+
+import FVL.Algebra
+import qualified FVL.FAST as FAST
+
+data Expr a b
+    = CInt Integer
+    | CBool Bool
+    | CVar String
+    | Add b b
+    | Sub b b
+    | Mul b b
+    | Div b b
+    | And b b
+    | Or b b
+    | Not b
+    | Equal b b
+    | Less b b
+    | Empty
+    | Cons b b
+    | If b a a
+    | Function String a
+    | Appl b a
+    | LetRec String String a a
+    | Case b a String String a
+    deriving Functor
+
+showCons' :: LazyFix Expr -> [LazyFix Expr]
+showCons' (Fx' (x `Cons` y)) = x : showCons' y
+showCons' e = [e]
+
+showCons :: LazyFix Expr -> String
+showCons e = "[" ++ (foldr combine "\b\b" (showCons' e)) ++ "]"
+    where combine (Fx' Empty) b = b
+          combine a b = show a ++ ", " ++ b
+
+instance Show (LazyFix Expr) where
+    show (Fx' (CInt n)) = show n
+    show (Fx' (CBool b)) = show b
+    show (Fx' (CVar s)) = s
+    show (Fx' (x `Add` y)) = show x ++ " + " ++ show y
+    show (Fx' (x `Sub` y)) = show x ++ " - " ++ show y
+    show (Fx' (x `Mul` y)) = show x ++ " * " ++ show y
+    show (Fx' (x `Div` y)) = show x ++ " / " ++ show y
+    show (Fx' (x `And` y)) = show x ++ " && " ++ show y
+    show (Fx' (x `Or` y)) = show x ++ " || " ++ show y
+    show (Fx' (Not x)) = "!" ++ (case x of
+        (Fx' (CBool b)) -> show b
+        (Fx' (CVar s)) -> s
+        _ -> "(" ++ show x ++ ")")
+    show (Fx' (x `Equal` y)) = show x ++ " = " ++ show y
+    show (Fx' (x `Less` y)) = show x ++ " < " ++ show y
+    show (Fx' Empty) = "[]"
+    show (Fx' (x `Cons` y)) = showCons . Fx' $ x `Cons` y
+    show (Fx' (If p x y)) = "If " ++ show p ++ " Then " ++ show x ++ " Else " ++ show y
+    show (Fx' (Function x p)) = "Function " ++ x ++ " -> " ++ show p
+    show (Fx' (Appl f x)) = (case f of
+        (Fx' (CInt n)) -> show n ++ " "
+        (Fx' (CBool b)) -> show b ++ " "
+        (Fx' (CVar s)) -> s ++ " "
+        (Fx' (Appl _ _)) -> show f ++ " "
+        _ -> "(" ++ show f ++ ") ") ++ (case x of
+            (Fx' (CInt n)) -> show n
+            (Fx' (CBool b)) -> show b
+            (Fx' (CVar s)) -> s
+            (Fx' (Appl _ _)) -> show x
+            _ -> "(" ++ show x ++ ")")
+    show (Fx' (LetRec f x p e))
+        = "Let Rec " ++ f ++ " " ++ x ++ " = " ++ show p ++ " In " ++ show e
+    show (Fx' (Case p x s t y)) = "Case " ++ show x ++ " Of [] -> " ++ show x
+        ++ " | (" ++ s ++ ", " ++ t ++ ") -> " ++ show y
+
+data RVal = RInt Integer
+          | RBool Bool
+          | RFunction String (LazyFix Expr)
+          | REmpty
+          | RCons RVal RVal
+
+valueTransform :: RVal -> LazyFix Expr
+valueTransform (RInt n) = Fx' $ CInt n
+valueTransform (RBool b) = Fx' $ CBool b
+valueTransform (RFunction s p) = Fx' $ Function s p
+valueTransform REmpty = Fx' $ Empty
+valueTransform (RCons x y) = Fx' $ Cons (valueTransform x) (valueTransform y)
+
+instance Show RVal where
+    show = show . valueTransform
+
+alg :: Algebra FAST.Expr (LazyFix Expr)
+alg (FAST.CInt n) = Fx' $ CInt n
+alg (FAST.CBool b) = Fx' $ CBool b
+alg (FAST.CVar s) = Fx' $ CVar s
+alg (FAST.Add x y) = Fx' $ Add x y
+alg (FAST.Sub x y) = Fx' $ Sub x y
+alg (FAST.Mul x y) = Fx' $ Mul x y
+alg (FAST.Div x y) = Fx' $ Div x y
+alg (FAST.And x y) = Fx' $ And x y
+alg (FAST.Or x y) = Fx' $ Or x y
+alg (FAST.Not x) = Fx' $ Not x
+alg (FAST.Equal x y) = Fx' $ Equal x y
+alg (FAST.Less x y) = Fx' $ Less x y
+alg (FAST.Empty) = Fx' $ Empty
+alg (FAST.Cons x y) = Fx' $ Cons x y
+alg (FAST.If p x y) = Fx' $ If p x y
+alg (FAST.Function s p) = Fx' $ Function s p
+alg (FAST.Appl f x) = Fx' $ Appl f x
+alg (FAST.LetRec f x p e) = Fx' $ LetRec f x p e
+alg (FAST.Case p x s t y) = Fx' $ Case p x s t y
+
+evalTransform :: Fix FAST.Expr -> LazyFix Expr
+evalTransform = cata alg
+
diff --git a/FVL/F.hs b/FVL/F.hs
new file mode 100644
--- /dev/null
+++ b/FVL/F.hs
@@ -0,0 +1,34 @@
+{-# LANGUAGE FlexibleInstances #-}
+
+module FVL.F
+( run_eval
+, run_typecheck
+, Result(..)
+, run
+) where
+
+import FVL.FAST
+import FVL.EvalAST (evalTransform, RVal)
+import FVL.TypeAST (typeTransform, FType)
+import FVL.Algebra
+import FVL.Type
+import FVL.Eval
+
+instance Show (Fix Expr) where
+    show = show . evalTransform
+
+run_eval :: Fix Expr -> Maybe RVal
+run_eval = eval . evalTransform
+
+run_typecheck :: Fix Expr -> Maybe FType
+run_typecheck = typecheck . typeTransform
+
+data Result = Result (RVal, FType) | TypeMismatch | InconsistentTypes deriving Show
+
+run :: Fix Expr -> Result
+run e = case run_typecheck e of
+    Nothing -> InconsistentTypes
+    Just t -> case run_eval e of
+        Nothing -> TypeMismatch
+        Just v -> Result (v, t)
+
diff --git a/FVL/FAST.hs b/FVL/FAST.hs
new file mode 100644
--- /dev/null
+++ b/FVL/FAST.hs
@@ -0,0 +1,30 @@
+{-# LANGUAGE DeriveFunctor #-}
+
+module FVL.FAST
+( Expr(..)
+) where
+
+import FVL.Algebra
+
+data Expr a
+    = CInt Integer
+    | CBool Bool
+    | CVar String
+    | Add a a
+    | Sub a a
+    | Mul a a
+    | Div a a
+    | And a a
+    | Or a a
+    | Not a
+    | Equal a a
+    | Less a a
+    | Empty
+    | Cons a a
+    | If a a a
+    | Function String a
+    | Appl a a
+    | LetRec String String a a
+    | Case a a String String a
+    deriving Functor
+
diff --git a/FVL/Lexer.hs b/FVL/Lexer.hs
new file mode 100644
--- /dev/null
+++ b/FVL/Lexer.hs
@@ -0,0 +1,41 @@
+module FVL.Lexer
+( names
+, opNames
+, identifier
+, symbol
+, reserved
+, reservedOp
+, parens
+, brackets
+, commaSep
+, integer
+, whiteSpace
+) where
+
+import Text.Parsec
+import qualified Text.Parsec.Token as Token
+import Text.Parsec.Language
+
+names = words "True False Function If Then Else Let In Case Of"
+opNames = words "-> && || ! + - * / % = ; < <= > >= :"
+
+lexer = Token.makeTokenParser emptyDef
+    { Token.commentStart = "/*"
+    , Token.commentEnd = "*/"
+    , Token.commentLine = "#"
+    , Token.identStart = letter
+    , Token.identLetter = alphaNum <|> char '_' <|> char '\''
+    , Token.reservedNames = names
+    , Token.reservedOpNames = opNames
+    }
+
+identifier = Token.identifier lexer
+symbol     = Token.symbol lexer
+reserved   = Token.reserved lexer
+reservedOp = Token.reservedOp lexer
+parens     = Token.parens lexer
+brackets   = Token.brackets lexer
+commaSep   = Token.commaSep lexer
+integer    = Token.integer lexer
+whiteSpace = Token.whiteSpace lexer
+
diff --git a/FVL/Parser.hs b/FVL/Parser.hs
new file mode 100644
--- /dev/null
+++ b/FVL/Parser.hs
@@ -0,0 +1,117 @@
+module FVL.Parser
+( ParseError
+, parseString
+, parseFile
+) where
+
+import Text.Parsec hiding (Empty)
+import Text.Parsec.String
+import Text.Parsec.Expr
+import Control.Monad
+import Control.Applicative ((<$>), (<$), (<*>), (<*), (*>))
+
+import FVL.Algebra
+import FVL.EFAST
+import FVL.Lexer
+
+type ExprParser = Parser (Fix Expr)
+
+cint :: ExprParser
+cint = Fx . CInt <$> integer
+
+cbool :: Parser (Fix Expr)
+cbool = Fx (CBool True) <$ reserved "True"
+    <|> Fx (CBool False) <$ reserved "False"
+
+cvar :: ExprParser
+cvar = Fx . CVar <$> identifier
+
+prefix n f = Prefix (reservedOp n *> return (Fx . f))
+binary n f a = Infix (reservedOp n *> return (\x -> Fx . f x)) a
+
+opTable = [ [ prefix "!" Not ]
+          , [ appl ]
+          , [ binary "*" Mul AssocLeft
+            , binary "/" Div AssocLeft
+            , binary "%" Mod AssocLeft ]
+          , [ binary "+" Add AssocLeft
+            , binary "-" Sub AssocLeft
+            ]
+          , [ binary "=" Equal AssocLeft
+            , binary "<" Less AssocLeft
+            , binary "<=" LessEq AssocLeft
+            , binary ">" Great AssocLeft
+            , binary ">=" GreatEq AssocLeft
+            ]
+          , [ binary "&&" And AssocLeft ]
+          , [ binary "||" Or AssocLeft ]
+          , [ binary ":" Cons AssocRight ]
+          , [ binary ";" Semi AssocLeft ]
+          ]
+
+opExpr :: ExprParser
+opExpr = buildExpressionParser opTable term
+
+list :: ExprParser
+list = toCons <$> brackets (commaSep expr)
+    where toCons [] = Fx Empty
+          toCons (x:xs) = Fx $ Cons x (toCons xs)
+
+ifExpr :: ExprParser
+ifExpr = reserved "If" *> ((\x y -> Fx . If x y)
+    <$> expr <*> (reserved "Then" *> expr) <*> (reserved "Else" *> expr))
+
+function :: ExprParser
+function = reserved "Function" *> ((\x -> Fx . Function x)
+    <$> identifier <*> (reservedOp "->" *> expr))
+
+appl = Infix space AssocLeft
+    where space = whiteSpace
+            *> notFollowedBy (choice . map reservedOp $ opNames)
+            *> return (\x y -> Fx $ Appl x y)
+
+letExpr :: ExprParser
+letExpr = reserved "Let" *> do
+    s <- sepBy1 identifier whiteSpace
+    reservedOp "="
+    e <- expr
+    reserved "In"
+    e' <- expr
+    case s of (x:xs) -> return . Fx $ Let x xs e e'
+
+caseExpr :: ExprParser
+caseExpr = reserved "Case" *> do
+    p <- expr
+    reserved "Of" *> symbol "[]" *> reservedOp "->"
+    x <- expr
+    reservedOp "|"
+    (s, t) <- parens $ do{ s' <- identifier
+                         ; reservedOp ":"
+                         ; t' <- identifier
+                         ; return (s', t')
+                         }
+    reservedOp "->"
+    y <- expr
+    return . Fx $ Case p x s t y
+
+term :: ExprParser
+term =  cint
+    <|> cbool
+    <|> cvar
+    <|> list
+    <|> parens expr
+
+expr :: ExprParser
+expr =  function
+    <|> letExpr
+    <|> ifExpr
+    <|> caseExpr
+    <|> opExpr
+    <|> term
+
+parseString :: String -> Either ParseError (Fix Expr)
+parseString s = parse (expr <* eof) "" s
+
+parseFile :: FilePath -> IO (Either ParseError (Fix Expr))
+parseFile f = parseFromFile (expr <* eof) f
+
diff --git a/FVL/Type.hs b/FVL/Type.hs
new file mode 100644
--- /dev/null
+++ b/FVL/Type.hs
@@ -0,0 +1,148 @@
+module FVL.Type
+( typecheck
+) where
+
+import Prelude hiding (lookup)
+import qualified Data.Set as Set
+import Control.Monad.State
+import Control.Applicative
+
+import FVL.Algebra
+import FVL.TypeAST
+
+type Equation = (FType, FType)
+type Equations = Set.Set Equation
+data Updates = Updates Equations Bool
+
+(=>>) :: Updates -> (Equations -> Updates) -> Updates
+(=>>) (Updates e True) f = let (Updates e' _) = f e in Updates e' True
+(=>>) (Updates e _) f = f e
+
+addEquation' :: Equation -> Equations -> Updates
+addEquation' eq e = if Set.member eq e then Updates e False else Updates (Set.insert eq e) True
+
+addEquation :: Equation -> Equations -> Updates
+addEquation (x, y) e = addEquation' (x, y) e =>> addEquation' (y, x)
+
+addTransitives :: Equations -> Updates
+addTransitives e = Set.fold check_element (Updates e False) e
+    where check_element eq u = u =>> Set.fold (run_through eq) u
+          run_through (x, y) (x', y') u = if x' == y
+              then u =>> addEquation (x, y')
+              else u
+
+addArrowsAndLists :: Equations -> Updates
+addArrowsAndLists e = Set.fold check_element (Updates e False) e
+    where check_element (FArrow x y, FArrow x' y') u
+              = u =>> addEquation (x, x') =>> addEquation (y, y')
+          check_element (FList x, FList y) u
+              = u =>> addEquation (x, y) =>> addEquation (y, x)
+          check_element _ u = u
+
+close :: Equations -> Equations
+close e = let Updates e' r = addTransitives e =>> addArrowsAndLists in if r
+    then close e' 
+    else e'
+
+inconsistent :: Equations -> Bool
+inconsistent e = Set.fold check False e
+    where check (FInt, FBool) _ = True
+          check (FInt, FArrow _ _) _ = True
+          check (FInt, FList _) _ = True
+          check (FBool, FArrow _ _) _ = True
+          check (FBool, FList _) _ = True
+          check (FArrow _ _, FList _) _ = True
+          check (FNotClosed, _) _ = True
+          check _ r = r
+
+choose :: Int -> Equations -> Equation -> FType -> FType
+choose _ _ _ FInt = FInt
+choose _ _ _ FBool = FBool
+choose n e (FVar n', FArrow x y) (FVar n'') = if n' == n
+    then FArrow (substitute x e) (substitute y e)
+    else FVar n''
+choose n e (FVar n', FList t) r = if n == n'
+    then FList (substitute t e)
+    else r
+choose n _ (FVar n', y) (FVar n'') = if n /= n' then FVar n'' else case y of
+    FInt -> FInt
+    FBool -> FBool
+    FVar n' -> if n' < n
+        then if n'' < n' then FVar n'' else FVar n'
+        else if n'' < n then FVar n'' else FVar n
+choose _ _ _ r = r
+
+substitute :: FType -> Equations -> FType
+substitute FInt _ = FInt
+substitute FBool _ = FBool
+substitute (FVar n) e = Set.fold (choose n e) (FVar n) e
+substitute (FArrow x y) e = FArrow (substitute x e) (substitute y e)
+substitute (FList t) e = FList $ substitute t e
+
+add :: Equation -> Equations -> Equations
+add (x, y) e = Set.insert (x, y) (Set.insert (y, x) e)
+
+twoAdd :: Equation -> Equation -> Equations -> Equations -> Equations
+twoAdd eq eq' e e' = add eq $ add eq' (Set.union e e')
+
+threeAdd :: Equation -> Equation -> Equation -> Equations -> Equations -> Equations -> Equations
+threeAdd eq eq' eq'' e e' e'' = add eq $ Set.union e (twoAdd eq' eq'' e' e'')
+
+type Counter = State Int
+
+doNothing :: Counter Int
+doNothing = state (\i -> (i, i))
+
+newHandle :: Counter Int
+newHandle = state (\i -> (i, i + 1))
+
+type Hypotheses = [(String, FType)]
+
+lookup :: String -> Hypotheses -> Maybe FType
+lookup s [] = Nothing
+lookup s ((s', t):xs) = if s' == s then Just t else lookup s xs
+
+type TypeResult = (FType, Equations)
+type TypeMAlgebra = MAlgebra Counter (Expr (LazyFix Expr)) TypeResult
+
+alg :: Hypotheses -> TypeMAlgebra
+alg _ (CInt _) = (\_ -> (FInt, Set.empty)) <$> doNothing
+alg _ (CBool _) = (\_ -> (FBool, Set.empty)) <$> doNothing
+alg g (CVar s) = (\_ -> let r = lookup s g in case r of
+    Nothing -> (FNotClosed, Set.insert (FNotClosed, FNotClosed) Set.empty)
+    Just t -> (t, Set.empty)) <$> doNothing
+alg _ (x `Add` y) = (\(t, e) (t', e') -> (FInt, twoAdd (t, FInt) (t', FInt) e e')) <$> x <*> y
+alg _ (x `Sub` y) = (\(t, e) (t', e') -> (FInt, twoAdd (t, FInt) (t', FInt) e e')) <$> x <*> y
+alg _ (x `Mul` y) = (\(t, e) (t', e') -> (FInt, twoAdd (t, FInt) (t', FInt) e e')) <$> x <*> y
+alg _ (x `Div` y) = (\(t, e) (t', e') -> (FInt, twoAdd (t, FInt) (t', FInt) e e')) <$> x <*> y
+alg _ (x `And` y) = (\(t, e) (t', e') -> (FBool, twoAdd (t, FBool) (t', FBool) e e')) <$> x <*> y
+alg _ (x `Or` y) = (\(t, e) (t', e') -> (FBool, twoAdd (t, FBool) (t', FBool) e e')) <$> x <*> y
+alg _ (x `Equal` y) = (\(t, e) (t', e') -> (FBool, twoAdd (t, FInt) (t', FInt) e e')) <$> x <*> y
+alg _ (x `Less` y) = (\(t, e) (t', e') -> (FBool, twoAdd (t, FInt) (t', FInt) e e')) <$> x <*> y
+alg _ Empty = (\n -> let h = FVar n in (FList h, Set.empty)) <$> newHandle
+alg _ (x `Cons` y) = (\n (t, e) (t', e') -> let h = FVar n in
+    (FList h, twoAdd (t, h) (t', FList h) e e')) <$> newHandle <*> x <*> y
+alg _ (Not x) = (\(t, e) -> (FBool, add (t, FBool) e)) <$> x
+alg _ (If p x y) = (\n (t, e) (t', e') (t'', e'') -> let h = FVar n in
+    (h, threeAdd (t, FBool) (t', t'') (t'', h) e e' e'')) <$> newHandle <*> p <*> x <*> y
+alg g (Function x p) = newHandle >>= \n -> let h = FVar n in
+    typecheck' ((x, h) : g) p >>= \(t, e) -> return (FArrow h t, e)
+alg _ (Appl f x) = (\n (t, e) (t', e') -> let h = FVar n in
+    (h, add (t, FArrow t' h) (Set.union e e'))) <$> newHandle <*> f <*> x
+alg g (LetRec f x p r) = newHandle >>= \n -> newHandle >>= \n' ->
+    let h = FVar n in let h' = FVar n' in
+    typecheck' ((f, h) : (x, h') : g) p >>= \(t, e) ->
+    typecheck' ((f, h) : g) r >>= \(t', e') ->
+    return (t', add (h, FArrow h' t) (Set.union e e'))
+alg g (Case p x s s' y) = newHandle >>= \n -> let h = FVar n in p >>= \(t, e) ->
+    x >>= \(t', e') -> typecheck' ((s, h) : (s', FList h) : g) y >>= \(t'', e'') ->
+    return (t', twoAdd (t, FList h) (t', t'') e (Set.union e' e''))
+
+typecheck' :: Hypotheses -> LazyFix Expr -> Counter TypeResult
+typecheck' g e = lazyMCata (alg g) e
+
+typecheck :: LazyFix Expr -> Maybe FType
+typecheck e = let (t, e') = evalState (typecheck' [] e) 0
+    in let e'' = close e'
+    in if inconsistent e'' then Nothing else Just (substitute t e'')
+
diff --git a/FVL/TypeAST.hs b/FVL/TypeAST.hs
new file mode 100644
--- /dev/null
+++ b/FVL/TypeAST.hs
@@ -0,0 +1,73 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE DeriveFunctor #-}
+
+module FVL.TypeAST
+( Expr(..)
+, FType(..)
+, typeTransform
+) where
+
+import FVL.Algebra
+import qualified FVL.FAST as FAST
+
+data Expr a b
+    = CInt Integer
+    | CBool Bool
+    | CVar String
+    | Add b b
+    | Sub b b
+    | Mul b b
+    | Div b b
+    | And b b
+    | Or b b
+    | Not b
+    | Equal b b
+    | Less b b
+    | Empty
+    | Cons b b
+    | If b b b
+    | Function String a
+    | Appl b b
+    | LetRec String String a a
+    | Case b b String String a
+    deriving Functor
+
+data FType = FInt
+           | FBool
+           | FVar Int
+           | FArrow FType FType
+           | FList FType
+           | FNotClosed deriving (Eq, Ord)
+
+instance Show FType where
+    show FInt = "Int"
+    show FBool = "Bool"
+    show (FVar n) = "'a" ++ show n
+    show (FArrow x y) = show x ++ " -> " ++ show y
+    show (FList t) = "[" ++ show t ++ "]"
+    show _ = ""
+
+alg :: Algebra FAST.Expr (LazyFix Expr)
+alg (FAST.CInt n) = Fx' $ CInt n
+alg (FAST.CBool b) = Fx' $ CBool b
+alg (FAST.CVar s) = Fx' $ CVar s
+alg (FAST.Add x y) = Fx' $ Add x y
+alg (FAST.Sub x y) = Fx' $ Sub x y
+alg (FAST.Mul x y) = Fx' $ Mul x y
+alg (FAST.Div x y) = Fx' $ Div x y
+alg (FAST.And x y) = Fx' $ And x y
+alg (FAST.Or x y) = Fx' $ Or x y
+alg (FAST.Not x) = Fx' $ Not x
+alg (FAST.Equal x y) = Fx' $ Equal x y
+alg (FAST.Less x y) = Fx' $ Less x y
+alg FAST.Empty = Fx' $ Empty
+alg (FAST.Cons x y) = Fx' $ Cons x y
+alg (FAST.If p x y) = Fx' $ If p x y
+alg (FAST.Function s p) = Fx' $ Function s p
+alg (FAST.Appl f x) = Fx' $ Appl f x
+alg (FAST.LetRec f x p e) = Fx' $ LetRec f x p e
+alg (FAST.Case p x s t y) = Fx' $ Case p x s t y
+
+typeTransform :: Fix FAST.Expr -> LazyFix Expr
+typeTransform = cata alg
+
diff --git a/Feval.cabal b/Feval.cabal
--- a/Feval.cabal
+++ b/Feval.cabal
@@ -10,7 +10,7 @@
 -- PVP summary:      +-+------- breaking API changes
 --                   | | +----- non-breaking API additions
 --                   | | | +--- code changes with no API change
-version:             1.0.0.0
+version:             1.0.0.1
 
 -- A short (one-line) description of the package.
 synopsis:            Evaluation using F-Algebras
@@ -59,9 +59,20 @@
 executable Feval
   -- .hs or .lhs file containing the Main module.
   main-is:             feval.hs
-  
+
   -- Modules included in this executable, other than Main.
-  -- other-modules:       
+  other-modules:
+      FVL.Algebra
+      FVL.EFAST
+      FVL.EF
+      FVL.EvalAST
+      FVL.Eval
+      FVL.FAST
+      FVL.F
+      FVL.Lexer
+      FVL.Parser
+      FVL.TypeAST
+      FVL.Type
   
   -- Other library packages from which modules are imported.
   build-depends:       base ==4.6.*, parsec ==3.1.*, containers ==0.5.*, mtl ==2.1.*
@@ -71,7 +82,18 @@
   main-is:             examples.hs
   
   -- Modules included in this executable, other than Main.
-  -- other-modules:       
+  other-modules:
+      FVL.Algebra
+      FVL.EFAST
+      FVL.EF
+      FVL.EvalAST
+      FVL.Eval
+      FVL.FAST
+      FVL.F
+      FVL.Lexer
+      FVL.Parser
+      FVL.TypeAST
+      FVL.Type
   
   if flag(buildExamples)
       -- Other library packages from which modules are imported.