diff --git a/flake.nix b/flake.nix
index eeada23..d55c8fd 100644
--- a/flake.nix
+++ b/flake.nix
@@ -23,7 +23,7 @@
         # The "main" project. You can have multiple projects, but this template
         # has only one.
         haskellProjects.main = {
-          packages.lambda.root = ./.; # Auto-discovered by haskell-flake
+          packages.typed-lambda.root = ./.; # Auto-discovered by haskell-flake
           overrides = self: super: { };
           devShell = {
             tools = hp: {
@@ -87,7 +87,7 @@
         };
 
         # Default package.
-        packages.default = self'.packages.main-lambda;
+        packages.default = self'.packages.main-typed-lambda;
 
         # Default shell.
         devShells.default =
diff --git a/src/Compilation/Compiler.hs b/src/Compilation/Compiler.hs
new file mode 100644
index 0000000..02321c1
--- /dev/null
+++ b/src/Compilation/Compiler.hs
@@ -0,0 +1,16 @@
+module Compilation.Compiler where
+
+import Compilation.Lift (lift)
+import Language.Declarations (Declaration)
+import Parsing.Parser (parseFile)
+import System.IO (IOMode (ReadMode), hGetContents, openFile)
+
+runCompiler :: String -> IO ()
+runCompiler file = do
+  -- parse file
+  handle <- openFile file ReadMode
+  content <- hGetContents handle
+  case parseFile file content of
+    Left err -> print err
+    Right decls -> do
+      mapM_ print $ lift decls
\ No newline at end of file
diff --git a/src/Compilation/Lift.hs b/src/Compilation/Lift.hs
new file mode 100644
index 0000000..6f7291a
--- /dev/null
+++ b/src/Compilation/Lift.hs
@@ -0,0 +1,53 @@
+module Compilation.Lift where
+
+import Control.Monad.State (State, execState, gets, modify, runState)
+import Language.Declarations (Declaration (..))
+import Language.Terms
+
+funNames :: [String]
+funNames = ["anon$" ++ show n | n <- [0 ..]]
+
+data LiftState = LiftState
+  { anonCounter :: Int
+  , anonDeclarations :: [Declaration]
+  }
+
+type LiftMonad = State LiftState
+
+lift :: [Declaration] -> [Declaration]
+lift decls = newDecls ++ anonDeclarations endState
+  where
+    (newDecls, endState) = runState liftDecls (LiftState 0 [])
+    liftDecls :: LiftMonad [Declaration]
+    liftDecls = mapM liftDecl decls
+
+liftDecl :: Declaration -> LiftMonad Declaration
+liftDecl (Declaration name typ (Abs x t)) = do
+  newTerm <- liftTerm t
+  return $ Declaration name typ (Abs x newTerm)
+liftDecl (Declaration name typ term) = do
+  newTerm <- liftTerm term
+  return $ Declaration name typ newTerm
+
+liftTerm :: Term -> LiftMonad Term
+liftTerm t@(Var _) = return t
+liftTerm (App t1 t2) = do
+  t1' <- liftTerm t1
+  t2' <- liftTerm t2
+  return $ App t1' t2'
+liftTerm (Abs x t) = do
+  -- first lift all terms in t
+  t' <- liftTerm t
+  -- add global declaration for lambda
+  newName <- getAnonName
+  let decl = Declaration newName Nothing t'
+  anonDecls <- gets anonDeclarations
+  modify (\s -> s {anonDeclarations = decl : anonDecls})
+
+  return $ Var newName
+
+getAnonName :: LiftMonad String
+getAnonName = do
+  count <- gets anonCounter
+  modify (\s -> s {anonCounter = count + 1})
+  return $ "anon$" ++ show count
\ No newline at end of file
diff --git a/src/Compilation/ToImmediate.hs b/src/Compilation/ToImmediate.hs
new file mode 100644
index 0000000..778a70c
--- /dev/null
+++ b/src/Compilation/ToImmediate.hs
@@ -0,0 +1,56 @@
+module Compilation.ToImmediate where
+
+import Control.Monad.State
+import Language.Declarations
+import Language.Immediate
+import Language.Terms
+
+-- Transforms a list of declarations to a list of immediate statements
+
+-- state for lambda lifting
+data LiftState = LiftState
+  { anonCounter :: Int
+  , anonDeclarations :: [ImmediateDeclaration]
+  }
+
+type LiftMonad = State LiftState
+
+lift :: [Declaration] -> [ImmediateDeclaration]
+lift decls = newDecls ++ anonDeclarations endState
+  where
+    (newDecls, endState) = runState liftDecls (LiftState 0 [])
+    liftDecls :: LiftMonad [ImmediateDeclaration]
+    liftDecls = mapM liftDecl decls
+
+liftDecl :: Declaration -> LiftMonad ImmediateDeclaration
+liftDecl (Declaration name typ term) = do
+  newTerm <- liftTerm term
+  return $ ImmediateDeclaration name newTerm
+
+buildFunction :: Term -> LiftMonad Immediate
+buildFunction (Abs x t) = do
+  t' <- buildFunction t
+  return $ case t' of
+    (IVar v) -> IFunction [x] (IVar v)
+    (IApp i1 i2) -> IFunction [x] (IApp i1 i2)
+    (IFunction xs i) -> IFunction (x : xs) i
+buildFunction t = liftTerm t
+
+liftTerm :: Term -> LiftMonad Immediate
+liftTerm (Abs x t) = do
+  -- first lift all terms in t
+  t' <- liftTerm t
+  -- add global declaration for lambda
+  newName <- getAnonName
+  -- TODO
+  let decl = Declaration newName Nothing t'
+  anonDecls <- gets anonDeclarations
+  modify (\s -> s {anonDeclarations = decl : anonDecls})
+
+  return $ Var newName
+
+getAnonName :: LiftMonad String
+getAnonName = do
+  count <- gets anonCounter
+  modify (\s -> s {anonCounter = count + 1})
+  return $ "anon$" ++ show count
\ No newline at end of file
diff --git a/src/Reduction.hs b/src/Interpretation/Reduction.hs
similarity index 83%
rename from src/Reduction.hs
rename to src/Interpretation/Reduction.hs
index 5df6c3a..e6c3aa0 100644
--- a/src/Reduction.hs
+++ b/src/Interpretation/Reduction.hs
@@ -1,4 +1,4 @@
-module Reduction (reduce) where
+module Interpretation.Reduction (reduce) where
 
 import Control.Monad (when)
 import Data.Char (toLower)
@@ -9,7 +9,7 @@ import Data.Maybe (fromMaybe)
 import Data.Maybe qualified as Maybe
 import Data.Set (Set)
 import Data.Set qualified as Set
-import Syntax (Substitution, Term (..), Var)
+import Language.Terms (Substitution, Term (..), Var)
 
 -- a stock of variablenames that is used for getting fresh variables
 vars :: [Var]
@@ -73,24 +73,27 @@ showResult :: Map String Term -> Term -> IO ()
 showResult globals t = do
   putStr "result: "
   print t
-  case parseChurchNumeral t of
-    Nothing -> return ()
-    Just x -> putStr "as church-numeral: " >> print x
-  case parseChurchBoolean t of
-    Nothing -> return ()
-    Just x -> putStr "as church-boolean: " >> putStrLn (map toLower $ show x)
-  case parseFoldList t of
-    Nothing -> return ()
-    Just x -> do
-      let numeralList = mapM parseChurchNumeral x
-      case numeralList of
-        Nothing -> return ()
-        Just x -> putStr "as fold-list (numeral):" >> print x
-      let booleanList = mapM parseChurchBoolean x
-      case booleanList of
-        Nothing -> return ()
-        Just x -> putStr "as fold-list (boolean):" >> print x
-  putStrLn ""
+
+{-
+case parseChurchNumeral t of
+  Nothing -> return ()
+  Just x -> putStr "as church-numeral: " >> print x
+case parseChurchBoolean t of
+  Nothing -> return ()
+  Just x -> putStr "as church-boolean: " >> putStrLn (map toLower $ show x)
+case parseFoldList t of
+  Nothing -> return ()
+  Just x -> do
+    let numeralList = mapM parseChurchNumeral x
+    case numeralList of
+      Nothing -> return ()
+      Just x -> putStr "as fold-list (numeral):" >> print x
+    let booleanList = mapM parseChurchBoolean x
+    case booleanList of
+      Nothing -> return ()
+      Just x -> putStr "as fold-list (boolean):" >> print x
+putStrLn ""
+-}
 
 parseChurchNumeral :: Term -> Maybe Int
 parseChurchNumeral (Abs f (Abs a (Var a'))) | a == a' = Just 0
diff --git a/src/Interpretation/Repl.hs b/src/Interpretation/Repl.hs
new file mode 100644
index 0000000..9a4cfc0
--- /dev/null
+++ b/src/Interpretation/Repl.hs
@@ -0,0 +1,76 @@
+module Interpretation.Repl (runInterpreter) where
+
+import Control.Exception (SomeException (SomeException), catch)
+import Control.Monad.State (
+  MonadIO (liftIO),
+  MonadTrans (lift),
+  StateT,
+  evalStateT,
+  gets,
+  lift,
+  modify,
+ )
+import Data.Functor (($>))
+import Data.Map.Strict (Map)
+import Data.Map.Strict qualified as Map
+import Data.Maybe (fromJust)
+import Interpretation.Reduction (reduce)
+import Language.Declarations (Declaration (..))
+import Language.Terms (Term)
+import Parsing.Parser (parseLine, parsePrelude, readP)
+import System.Console.Haskeline (
+  InputT,
+  defaultSettings,
+  getInputLine,
+  runInputT,
+ )
+import System.IO (IOMode (ReadMode), hGetContents, openFile)
+
+-- REPL
+newtype ReplState = ReplState {declarations :: Map String Term}
+insertDeclaration :: Declaration -> ReplM ()
+insertDeclaration (Declaration name typ term) = modify (\state -> state {declarations = Map.insert name term (declarations state)})
+type ReplM = StateT ReplState IO
+initialState :: ReplState
+initialState = ReplState . Map.fromList $ map (\(Declaration name typ term) -> (name, term)) []
+
+runInterpreter :: IO ()
+runInterpreter = evalStateT (readPrelude >> runInputT defaultSettings repl) initialState
+  where
+    repl :: InputT ReplM ()
+    repl = do
+      minput <- getInputLine "λ "
+      case minput of
+        Nothing -> return ()
+        Just line -> do
+          lift $ evalLine line
+          repl
+
+-- Try reading prelude definitions from prelude.lmd
+readPrelude :: ReplM ()
+readPrelude = do
+  decls <- liftIO $ catch getDecls handleException
+  mapM_ insertDeclaration decls
+  where
+    getDecls :: IO [Declaration]
+    getDecls = do
+      handle <- liftIO $ openFile "prelude.lmd" ReadMode
+      content <- liftIO $ hGetContents handle
+      let declsE = parsePrelude content
+      case declsE of
+        Left err -> putStrLn ("Error while parsing prelude:\n" ++ show err) $> []
+        Right decls -> putStrLn "Prelude successfully read from prelude.lmd!" $> decls
+    handleException :: SomeException -> IO [Declaration]
+    handleException e = putStrLn "Couldn't read file prelude.lmd so no prelude was loaded." >> return []
+
+-- evaluate a single line from stdin
+evalLine :: String -> ReplM ()
+evalLine "" = return ()
+evalLine line = either (liftIO . print) computeLine $ parseLine line
+
+-- do computations for a single line
+computeLine :: Either Declaration Term -> ReplM ()
+computeLine (Left decl) = insertDeclaration decl
+computeLine (Right term) = do
+  decls <- gets declarations
+  liftIO $ reduce 0 False decls term
diff --git a/src/Language/Declarations.hs b/src/Language/Declarations.hs
new file mode 100644
index 0000000..af62acc
--- /dev/null
+++ b/src/Language/Declarations.hs
@@ -0,0 +1,10 @@
+module Language.Declarations where
+
+import Language.Terms (Term)
+import Language.Types (Type)
+
+data Declaration = Declaration String (Maybe Type) Term
+instance Show Declaration where
+  show :: Declaration -> String
+  show (Declaration name (Just typ) term) = name ++ " :: " ++ show typ ++ " := " ++ show term
+  show (Declaration name Nothing term) = name ++ " := " ++ show term
\ No newline at end of file
diff --git a/src/Language/Immediate.hs b/src/Language/Immediate.hs
new file mode 100644
index 0000000..5af0f30
--- /dev/null
+++ b/src/Language/Immediate.hs
@@ -0,0 +1,21 @@
+module Language.Immediate where
+
+data Immediate
+  = IVar String
+  | IApp Immediate Immediate
+  | IFunction [String] Immediate
+  deriving (Eq, Ord)
+
+instance Show Immediate where
+  show :: Immediate -> String
+  show (IVar v) = v
+  show (IApp i1 i2) = showHelper i1 False ++ " " ++ showHelper i2 True
+    where
+      showHelper :: Immediate -> Bool -> String
+      showHelper (IVar v) True = v
+      showHelper (IApp i1 i2) True = "(" ++ showHelper i1 False ++ " " ++ showHelper i2 True ++ ")"
+      showHelper (IFunction params i) True = "(" ++ show params ++ " -> " ++ show i ++ ")"
+  show (IFunction params i) = show params ++ " -> " ++ show i
+
+data ImmediateDeclaration = ImmediateDeclaration String Immediate
+  deriving (Eq, Ord, Show)
\ No newline at end of file
diff --git a/src/Syntax.hs b/src/Language/Terms.hs
similarity index 82%
rename from src/Syntax.hs
rename to src/Language/Terms.hs
index 273ac1a..4fef13a 100644
--- a/src/Syntax.hs
+++ b/src/Language/Terms.hs
@@ -1,10 +1,8 @@
-module Syntax where
+module Language.Terms where
 
 type Var = String
 type Substitution = Var -> Term
 
-data Declaration = Declaration String Term
-
 data Term
   = Var Var
   | App Term Term
@@ -27,7 +25,3 @@ instance Show Term where
       absHelper (Abs v t) True = "(\\" ++ v ++ "." ++ absHelper t False ++ ")"
       absHelper (Abs v t) False = "\\" ++ v ++ "." ++ absHelper t False
       absHelper t _ = show t
-
-instance Show Declaration where
-  show :: Declaration -> String
-  show (Declaration name term) = name ++ " = " ++ show term
diff --git a/src/Language/Types.hs b/src/Language/Types.hs
new file mode 100644
index 0000000..1ae28b0
--- /dev/null
+++ b/src/Language/Types.hs
@@ -0,0 +1,50 @@
+{-# LANGUAGE InstanceSigs #-}
+
+module Language.Types where
+
+import Data.List (intercalate)
+import Data.Map (Map)
+import Data.Map.Strict qualified as Map
+
+import Language.Terms (Term)
+
+-- Types
+data Type
+  = TypeVar String
+  | BaseType String
+  | Arrow Type Type
+  deriving (Eq, Ord)
+instance Show Type where
+  show :: Type -> String
+  show (TypeVar v) = v
+  show (BaseType b) = b
+  show (Arrow t1 t2) = go t1 ++ " -> " ++ show t2
+    where
+      go (Arrow t3 t4) = "(" ++ go t3 ++ " -> " ++ show t4 ++ ")"
+      go t = show t
+
+-- type variables occuring in type
+typeVars :: Type -> [String]
+typeVars (TypeVar v) = [v]
+typeVars (BaseType _) = []
+typeVars (Arrow t1 t2) = typeVars t1 ++ typeVars t2
+
+-- substitute a type for a type variable
+typeSubst :: Type -> String -> Type -> Type
+typeSubst tp@(TypeVar x) y sp = if x == y then sp else tp
+typeSubst tp@(BaseType _) _ _ = tp
+typeSubst (Arrow tp1 tp2) y tp3 = Arrow (typeSubst tp1 y tp3) (typeSubst tp2 y tp3)
+
+-- Contexts
+type Context = Map String Type
+showContext :: Context -> String
+showContext ctx | Map.null ctx = ""
+showContext ctx = "[" ++ intercalate ", " (map (\(name, tp) -> name ++ " : " ++ show tp) $ Map.toList ctx) ++ "]"
+emptyContext :: Context
+emptyContext = Map.empty
+
+-- Term in Context
+data TermInContext = TermInContext Context Term Type
+instance Show TermInContext where
+  show :: TermInContext -> String
+  show (TermInContext ctx term tp) = showContext ctx ++ " |- " ++ show term ++ " : " ++ show tp
\ No newline at end of file
diff --git a/src/Main.hs b/src/Main.hs
index fb35e1a..c78e8a6 100644
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -1,75 +1,7 @@
 module Main where
 
-import Control.Exception (SomeException (SomeException), catch)
-import Control.Monad.State (
-  MonadIO (liftIO),
-  MonadTrans (lift),
-  StateT,
-  evalStateT,
-  gets,
-  lift,
-  modify,
- )
-import Data.Functor (($>))
-import Data.Map.Strict (Map)
-import Data.Map.Strict qualified as Map
-import Data.Maybe (fromJust)
-import Parser (parseLine, parsePrelude, readP)
-import Reduction (reduce)
-import Syntax (Declaration (..), Term)
-import System.Console.Haskeline (
-  InputT,
-  defaultSettings,
-  getInputLine,
-  runInputT,
- )
-import System.IO (IOMode (ReadMode), hGetContents, openFile)
-
--- REPL
-newtype ReplState = ReplState {declarations :: Map String Term}
-insertDeclaration :: Declaration -> ReplM ()
-insertDeclaration (Declaration name term) = modify (\state -> state {declarations = Map.insert name term (declarations state)})
-type ReplM = StateT ReplState IO
-initialState :: ReplState
-initialState = ReplState . Map.fromList $ map (\(Declaration name term) -> (name, term)) []
+import Compilation.Compiler (runCompiler)
+import Interpretation.Repl (runInterpreter)
 
 main :: IO ()
-main = evalStateT (readPrelude >> runInputT defaultSettings repl) initialState
-  where
-    repl :: InputT ReplM ()
-    repl = do
-      minput <- getInputLine "λ "
-      case minput of
-        Nothing -> return ()
-        Just line -> do
-          lift $ evalLine line
-          repl
-
--- Try reading prelude definitions from prelude.lmd
-readPrelude :: ReplM ()
-readPrelude = do
-  decls <- liftIO $ catch getDecls handleException
-  mapM_ insertDeclaration decls
-  where
-    getDecls :: IO [Declaration]
-    getDecls = do
-      handle <- liftIO $ openFile "prelude.lmd" ReadMode
-      content <- liftIO $ hGetContents handle
-      let declsE = parsePrelude content
-      case declsE of
-        Left err -> putStrLn ("Error while parsing prelude:\n" ++ show err) $> []
-        Right decls -> putStrLn "Prelude successfully read from prelude.lmd!" $> decls
-    handleException :: SomeException -> IO [Declaration]
-    handleException e = putStrLn "Couldn't read file prelude.lmd so no prelude was loaded." >> return []
-
--- evaluate a single line from stdin
-evalLine :: String -> ReplM ()
-evalLine "" = return ()
-evalLine line = either (liftIO . print) computeLine $ parseLine line
-
--- do computations for a single line
-computeLine :: Either Declaration Term -> ReplM ()
-computeLine (Left decl) = insertDeclaration decl
-computeLine (Right term) = do
-  decls <- gets declarations
-  liftIO $ reduce 0 False decls term
+main = runCompiler "test.lmd"
\ No newline at end of file
diff --git a/src/Lexer.hs b/src/Parsing/Lexer.hs
similarity index 87%
rename from src/Lexer.hs
rename to src/Parsing/Lexer.hs
index 964d725..5e24531 100644
--- a/src/Lexer.hs
+++ b/src/Parsing/Lexer.hs
@@ -1,6 +1,6 @@
 {-# LANGUAGE ImportQualifiedPost #-}
 
-module Lexer where
+module Parsing.Lexer where
 
 import Text.Parsec.Char (alphaNum, letter, oneOf)
 import Text.Parsec.Language (emptyDef)
@@ -10,14 +10,15 @@ import Text.Parsec.Token qualified as Tok
 lexer :: Tok.TokenParser ()
 lexer = Tok.makeTokenParser style
   where
-    ops = ["\\", "="]
+    ops = ["\\", ":=", "::", "->"]
     names = []
     style =
       emptyDef
         { Tok.commentLine = "#"
         , Tok.reservedOpNames = ops
         , Tok.reservedNames = names
-        , Tok.opLetter = oneOf "\\=."
+        , Tok.opStart = oneOf "\\=:-"
+        , Tok.opLetter = oneOf "\\=>:"
         , Tok.identStart = letter
         , Tok.identLetter = alphaNum
         }
diff --git a/src/Parser.hs b/src/Parsing/Parser.hs
similarity index 64%
rename from src/Parser.hs
rename to src/Parsing/Parser.hs
index 4597174..baa1127 100644
--- a/src/Parser.hs
+++ b/src/Parsing/Parser.hs
@@ -1,8 +1,11 @@
-module Parser (parseLine, readP, parsePrelude) where
+module Parsing.Parser (parseLine, readP, parsePrelude, parseFile) where
 
+import Data.Char (isUpper)
 import Data.Either.Extra (eitherToMaybe)
-import Lexer (digit, dot, identifier, parens, reservedOp, semi, whiteSpace)
-import Syntax (Declaration (..), Term (..))
+import Language.Declarations (Declaration (..))
+import Language.Terms (Term (..))
+import Language.Types (Type (Arrow, BaseType, TypeVar))
+import Parsing.Lexer (digit, dot, identifier, parens, reservedOp, semi, whiteSpace)
 import Text.Parsec (
   ParseError,
   endBy,
@@ -10,8 +13,10 @@ import Text.Parsec (
   many,
   many1,
   newline,
+  optionMaybe,
   parse,
   sepBy,
+  sepBy1,
   try,
   (<?>),
   (<|>),
@@ -26,7 +31,8 @@ declaration :: Parser Declaration
 declaration =
   Declaration
     <$> identifier
-    <*> (reservedOp "=" *> term)
+    <*> optionMaybe (reservedOp "::" *> typ)
+    <*> (reservedOp ":=" *> term)
     <?> "declaration"
 
 term :: Parser Term
@@ -61,6 +67,20 @@ abs =
     <*> (dot *> term)
     <?> "lambda abstraction"
 
+typ :: Parser Type
+typ = arrow <?> "type"
+
+arrow :: Parser Type
+arrow = foldr1 Arrow <$> sepBy1 atomicType (reservedOp "->")
+
+atomicType :: Parser Type
+atomicType = do
+  ident <- identifier
+  return $
+    if isUpper (head ident)
+      then BaseType ident
+      else TypeVar ident
+
 -- runners
 contents :: Parser a -> Parser a
 contents p = do
@@ -75,5 +95,8 @@ parseLine = Text.Parsec.parse (contents line) "stdin"
 parsePrelude :: String -> Either ParseError [Declaration]
 parsePrelude = Text.Parsec.parse (contents (declaration `endBy` semi)) "prelude.lmd"
 
+parseFile :: String -> String -> Either ParseError [Declaration]
+parseFile = Text.Parsec.parse (contents (declaration `endBy` semi))
+
 readP :: String -> Maybe Term
 readP line = eitherToMaybe (Text.Parsec.parse (contents term) "sourcefile" line)
diff --git a/src/Typechecking/TypeInference.hs b/src/Typechecking/TypeInference.hs
new file mode 100644
index 0000000..17f3530
--- /dev/null
+++ b/src/Typechecking/TypeInference.hs
@@ -0,0 +1,48 @@
+module Typechecking.TypeInference where
+
+import Control.Monad.State.Strict (
+  State,
+  evalState,
+  gets,
+  modify,
+ )
+import Data.Map.Strict qualified as Map
+
+import Language.Terms (Term (..))
+import Language.Types (Context, TermInContext (..), Type (Arrow, TypeVar))
+import Typechecking.Unification (Unifier, applyMgu, unify)
+
+-- state needed for algorithm W
+newtype PTState = PTState
+  { varCount :: Int
+  }
+type PTMonad = State PTState
+
+-- returns a fresh type var in algorithm W
+getNewTypeVar :: PTMonad String
+getNewTypeVar = do
+  count <- gets varCount
+  modify (\s -> s {varCount = count + 1})
+  return $ 'a' : show count
+
+-- implementation of algorithm W, this builds a list of terms to be unified in the next step
+pt :: Context -> Term -> Type -> PTMonad Unifier
+pt gamma (Var x) alpha = return [(alpha, gamma Map.! x)]
+pt gamma (Abs x t) alpha = do
+  a <- TypeVar <$> getNewTypeVar
+  b <- TypeVar <$> getNewTypeVar
+  result <- pt (Map.insert x a gamma) t b
+  return $ result ++ [(Arrow a b, alpha)]
+pt gamma (App t s) alpha = do
+  a <- TypeVar <$> getNewTypeVar
+  result1 <- pt gamma t (Arrow a alpha)
+  result2 <- pt gamma s a
+  return $ result1 ++ result2
+
+-- infer the type of a term in context (if any)
+inferType :: Context -> Term -> Maybe TermInContext
+inferType ctx term = do
+  let unificationProblem = evalState (pt ctx term (TypeVar "a0")) (PTState 1)
+  mgu <- unify unificationProblem
+  let principalType = applyMgu (TypeVar "a0") mgu
+  return $ TermInContext ctx term principalType
\ No newline at end of file
diff --git a/src/Typechecking/Unification.hs b/src/Typechecking/Unification.hs
new file mode 100644
index 0000000..c8f089c
--- /dev/null
+++ b/src/Typechecking/Unification.hs
@@ -0,0 +1,35 @@
+module Typechecking.Unification where
+
+import Language.Types (Type (..), typeSubst, typeVars)
+
+type Unifier = [(Type, Type)]
+
+-- unification algorithm of martelli montanari
+unify :: Unifier -> Maybe Unifier
+unify [] = Just []
+-- (delete)
+unify ((TypeVar x, TypeVar y) : rest) | x == y = unify rest
+-- (decomp)
+unify ((Arrow t1 t2, Arrow t1' t2') : rest) = unify $ [(t1, t1'), (t2, t2')] ++ rest
+unify ((BaseType b1, BaseType b2) : rest) | b1 == b2 = unify rest
+-- (conflict)
+unify ((BaseType b1, BaseType b2) : _) | b1 /= b2 = Nothing
+-- (orient)
+unify ((Arrow t1 t2, TypeVar x) : rest) = unify $ (TypeVar x, Arrow t1 t2) : rest
+unify ((BaseType b, TypeVar x) : rest) = unify $ (TypeVar x, BaseType b) : rest
+-- (occurs)
+unify ((TypeVar x, t) : _) | x `elem` typeVars t && TypeVar x /= t = Nothing
+-- (elim)
+unify ((TypeVar x, t) : rest) | notElem x (typeVars t) && x `elem` concatMap (\(t1, t2) -> typeVars t1 ++ typeVars t2) rest = unify $ (TypeVar x, t) : map (\(t1, t2) -> (typeSubst t1 x t, typeSubst t2 x t)) rest
+-- descent
+unify ((t, s) : rest) = do
+  rest' <- unify rest
+  return $ (t, s) : rest'
+
+-- apply a mgu to some type
+applyMgu :: Type -> Unifier -> Type
+applyMgu (TypeVar x) [] = TypeVar x
+applyMgu (TypeVar x) ((TypeVar y, tp) : rest) = if x == y then tp else applyMgu (TypeVar x) rest
+applyMgu (BaseType b) _ = BaseType b
+applyMgu (Arrow t1 t2) mgu = Arrow (applyMgu t1 mgu) (applyMgu t2 mgu)
+applyMgu _ (tp : _) = error $ "Non primitive type '" ++ show tp ++ "' on left side of mgu"
\ No newline at end of file
diff --git a/test.lmd b/test.lmd
new file mode 100644
index 0000000..7d45305
--- /dev/null
+++ b/test.lmd
@@ -0,0 +1 @@
+k :: Nat -> Nat -> Nat := \x.\y.x;
\ No newline at end of file
diff --git a/lambda.cabal b/typed-lambda.cabal
similarity index 66%
rename from lambda.cabal
rename to typed-lambda.cabal
index 4f8339b..c9f8cfe 100644
--- a/lambda.cabal
+++ b/typed-lambda.cabal
@@ -1,5 +1,5 @@
 cabal-version:      2.4
-name:               lambda
+name:               typed-lambda
 version:            0.1.0.0
 license:            MIT
 author:             Leon Vatthauer
@@ -28,7 +28,15 @@ executable lambda
   import:        shared
   main-is:       Main.hs
   other-modules:
-    Lexer
-    Parser
-    Reduction
-    Syntax
+    Parsing.Lexer
+    Parsing.Parser
+    Interpretation.Reduction
+    Interpretation.Repl
+    Language.Terms
+    Language.Types
+    Language.Declarations
+    Language.Immediate
+    Typechecking.Unification
+    Typechecking.TypeInference
+    Compilation.Lift
+    Compilation.Compiler