diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,25 @@
+Copyright (C) 2010, Matthias Reisner
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without modification, are permitted
+provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright notice, this list of conditions
+      and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above copyright notice, this list of
+      conditions and the following disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of the copyright holders nor the names of the contributors may be used to
+      endorse or promote products derived from this software without specific prior written
+      permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS “AS IS” AND ANY EXPRESS OR
+IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
+FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS OR
+CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER
+IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF
+THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/Prelude.tp b/Prelude.tp
new file mode 100644
--- /dev/null
+++ b/Prelude.tp
@@ -0,0 +1,89 @@
+-- ------------------------
+--    The Tempus Prelude
+-- ------------------------
+
+
+-- * Functions
+
+-- id : a -> a
+value id = \ x . x
+
+-- curry : (a * b -> c) -> a -> b -> c
+value curry = \ f . \ x . \ y . f (x, y)
+
+-- uncurry : (a -> b -> c) -> a * b -> c
+value uncurry = \ f . \ p . f (first p) (second p)
+
+
+-- * Tuples
+
+-- pair : a -> b -> a * b
+value pair = \ x . \ y . (x, y)
+
+-- normalize : (a * b) * c -> a * b * c
+value normalize = \ p . (first (first p), second (first p), second p)
+
+-- onFirst : (a -> b) -> (a * c) -> (b * c)
+value onFirst = \ f . \ p . (f (first p), second p)
+
+-- onSecond : (a -> b) -> (c * a) -> (c * b)
+value onSecond = \ f . \ p . (first p, f (second p))
+
+
+-- * Booleans
+
+type Bool = 1 + 1
+
+-- false : Bool
+value false = left ()
+
+-- true : Bool
+value true = right ()
+
+-- branch : a -> a -> Bool -> a
+value branch = \ x . \ y . case (\ _ . x) (\ _ . y)
+
+-- not : Bool -> Bool
+value not = branch true false
+
+-- and : Bool -> Bool -> Bool
+value and = branch (\ _ . false) id
+
+-- or : Bool -> Bool -> Bool
+value or = branch id (\ _ . true)
+
+-- xor : Bool -> Bool -> Bool
+value xor = branch id not
+
+
+-- * Extended behaviors
+
+type Behavior a = a * behavior a
+
+-- Behavior : a -> behavior a -> Behavior a
+value Behavior = pair
+
+-- head : Behavior a -> a
+value head = first
+
+-- tail : Behavior a -> behavior a
+value tail = second
+
+-- cut : Behavior a -> event b -> event (Behavior a * b)
+value cut = \ b . \ e . const pair <*> expand (tail b) <.> e
+
+
+-- * Extended events
+
+type Event a = a + event a
+
+-- now : a -> Event a
+value now = left
+
+-- later : event a -> Event a
+value later = right
+
+
+-- * Event streams
+
+type EventStream a = nu s . event (a * s)
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,6 @@
+module Main (main) where
+
+import Distribution.Simple
+
+main :: IO ()
+main = defaultMain
diff --git a/Tempus/Evaluation.hs b/Tempus/Evaluation.hs
new file mode 100644
--- /dev/null
+++ b/Tempus/Evaluation.hs
@@ -0,0 +1,306 @@
+-- | Evaluation of Tempus expressions.
+module Tempus.Evaluation (
+    EvalEnv,
+    Value (..),
+
+    evalExpr
+) where
+
+
+import Tempus.Syntax
+import Tempus.TypeCheck
+
+import Data.List
+
+-- | Representation of evaluation environments as a list of pairs of a variable with its expression.
+type EvalEnv = [(Var, Expr)]
+
+-- | Internal format for the value of an expression.
+data Value = Natural Integer
+           | Unit
+           | Function (Value -> Value)
+           | Pair Value Value
+           | ChoiceLeft Value
+           | ChoiceRight Value
+           | Behavior (RelTime -> Value)
+           | Event RelTime Value
+
+-- | Number of time steps with corresponding values to include when showing a bahavior.
+behaviorShowFuture :: Integer
+behaviorShowFuture = 7
+
+-- | Number of time steps to look ahead when deciding if to show an event as never occuring or not.
+eventShowLookAhead :: Integer
+eventShowLookAhead = 100
+
+-- TODO: make length of behavior future scalable
+-- TODO: make mu/nu expression depth scalable
+instance Show Value where
+    showsPrec _ (Natural i) = shows i
+    showsPrec _ (Unit) = showString "()"
+    showsPrec _ (Function _) = showString "<function>"
+    showsPrec p (Pair e1 e2) = showParen (p > 0) $
+        showsPrec 1 e1 . showString " , " . showsPrec 0 e2
+    showsPrec p (ChoiceLeft e) = showParen (p > 3) $
+        showString "left " . showsPrec 4 e
+    showsPrec p (ChoiceRight e) = showParen (p > 3) $
+        showString "right " . showsPrec 4 e
+    showsPrec p (Behavior f) = showParen (True) $ showString $ (
+        concat . intersperse "; "
+        . map (\ps -> case ps of
+                          [(v, t)] -> "@" ++ show (fromTime t) ++ ": " ++ v
+                          ps -> "@" ++ (let ps' = map snd ps in
+                                    show (head ps') ++ ".." ++ show (last ps')) ++ ": " ++ fst (head ps))
+        . groupBy (\x y -> fst x == fst y) . map (\t -> (show $ f t, t)) $
+              map fromInteger [1..behaviorShowFuture]) ++ "; ..."
+    showsPrec p (Event t e) = showParen (p > 3) $
+        if t > fromInteger eventShowLookAhead
+            then showString "?"
+            else showString "@" . shows t . showString ": " . shows e
+
+-- | Time representation for events and behaviors
+data RelTime = One
+             | Succ RelTime
+             deriving (Eq)
+
+-- | A 'RelTime' value for an infinite number of time steps.
+infinite :: RelTime
+infinite = Succ infinite
+
+instance Show RelTime where
+    show t = show $ fromTime t
+
+-- | Conversion from 'RelTime' values to 'Integer' values
+fromTime :: RelTime -> Integer
+fromTime One      = 1
+fromTime (Succ t) = 1 + fromTime t
+
+instance Ord RelTime where
+    compare One       One       = EQ
+    compare One       _         = LT
+    compare (Succ t1) (Succ t2) = compare t1 t2
+    compare (Succ _)  _         = GT
+
+    min One      t'        = One
+    min t        One       = One
+    min (Succ t) (Succ t') = Succ $ min t t'
+
+instance Num RelTime where
+    t + t' = Succ $ case t of
+                        One    -> t'
+                        Succ t -> t + t'
+
+    Succ t - One     = t
+    Succ t - Succ t' = t - t'
+    _      - _       = error "undefined value for RelTime"
+
+    fromInteger = genericIndex (iterate Succ One) . pred
+
+    (*) = undefined
+    abs = undefined
+    signum = undefined
+
+{- |
+    @evalExpr sEnv tEnv eEnv e@ evaluates an expression @e@ given 
+
+        [@sEnv@] the list of type synonyms,
+
+        [@tEnv@] the list of global variables with their types, and
+
+        [@eEnv@] the list of global variables with their expressions.
+-}
+evalExpr :: TypeSynEnv -> TypeEnv -> EvalEnv -> Expr -> Value
+evalExpr = eval []
+
+{- |
+    Helper function for 'evalExpr'. @eval lEnv sEnv tEnv eEnv e@ evaluates an expression @e@
+    given
+
+        [@lEnv@] the list of local variables with their values,
+
+        [@sEnv@] the list of type synonyms,
+
+        [@tEnv@] the list of global variables with their types, and
+
+        [@eEnv@] the list of global variables with their expressions.
+-}
+eval :: [(Var, Value)] -> TypeSynEnv -> TypeEnv -> EvalEnv -> Expr -> Value
+eval lEnv sEnv tEnv eEnv expr = let eval' = eval lEnv sEnv tEnv eEnv in case expr of
+    ExPair e1 e2 -> Pair (eval' e1) (eval' e2)
+    ExNatLit i -> Natural i
+    ExUnit -> Unit
+    ExLeft -> Function $ \v -> ChoiceLeft v
+    ExRight -> Function $ \v -> ChoiceRight v
+    ExNull -> Function $ \_ -> error "eval: received value of type 0"
+    ExFst -> Function $ \p -> case p of
+                                  Pair l _ -> l
+                                  _ -> error "eval: argument to ExFst not a pair"
+    ExSnd -> Function $ \p -> case p of
+                                  Pair _ r -> r
+                                  _ -> error "eval: argument to ExSnd not a pair"
+    ExCase -> Function $ \(Function l) -> Function $ \(Function r) -> Function $ \c -> case c of
+        ChoiceLeft e -> l e
+        ChoiceRight e -> r e
+        _ -> error "third argument to case not left/right"
+
+    ExVar (Var "add") -> withNat $ \i -> withNat $ \j -> Natural $ i + j
+    ExVar (Var "mult") -> withNat $ \i -> withNat $ \j -> Natural $ i * j
+    ExVar v -> case lookup v lEnv of
+                   Just x -> x
+                   Nothing -> maybe (error $ "eval: undefined var `" ++ show (SrcCode v) ++ "'")
+                                  eval' $ lookup v eEnv
+
+    ExLam v e -> Function (\x -> eval (replVar v x lEnv) sEnv tEnv eEnv e)
+    ExApp f x -> case eval' f of
+                     Function fun -> fun $ eval' x
+                     _ -> error "eval: first argument to ExApp not a function"
+
+    ExBehav f -> case eval' f of
+                     Function f -> Behavior (f . Natural . fromTime)
+                     _ -> error "first argument to ExBehav not a function"
+    ExEvent t e -> case eval' t of
+                       Natural i -> Event (fromInteger i) $ eval' e
+                       _ -> error "first argument to ExEvent not a positive"
+    ExNever -> Event infinite $ error "secret value of type 0"
+    ExConst e -> Behavior $ \_ -> eval' e
+    ExLiftAppB f b -> case (eval' f, eval' b) of
+        (Behavior f, Behavior g) -> Behavior $ \t -> case f t of
+            Function f -> f (g t)
+            _ -> error "wrong argument type(s) to ExLiftAppB"
+        _ -> error "wrong argument type(s) to ExLiftAppB"
+    ExLiftAppE f e -> case (eval' f, eval' e) of
+        (Behavior f, Event t v) -> Event t $ case f t of
+            Function f -> f v
+            _ -> error "wrong argument type(s) to ExLiftAppE"
+        _ -> error "wrong argument type(s) to ExLiftAppE"
+    ExRace -> Function $ \e1 -> case e1 of
+        Event t1 v1 -> Function $ \e2 -> case e2 of
+            Event t2 v2 -> Event (min t1 t2) $ case compare t1 t2 of
+                LT -> ChoiceRight $ ChoiceLeft $ Pair v1 (Event (t2 - t1) v2)
+                EQ -> ChoiceLeft $ Pair v1 v2
+                GT -> ChoiceRight $ ChoiceRight $ Pair v2 (Event (t1 - t2) v1)
+            _ -> error "second argument to ExRace not an event"
+        _ -> error "first argument to ExRace not an event"
+    ExExpand -> Function $ \e -> case e of
+        Behavior f -> Behavior $ \t -> Pair (f t) (Behavior $ \t' -> f $ t + t')
+        _ -> error "first argument to ExExpand not a behavior"
+    ExPack _ -> Function id
+    ExUnpack _ -> Function id
+    ExReflect -> Function $ \v -> let nat 1 = ChoiceLeft Unit
+                                      nat n = ChoiceRight $ nat (n-1)
+                                  in case v of
+                                         Natural n -> nat n
+                                         _ -> error "eval: argument to ExReflect not a positive"
+
+    -- fold :: (Functor shape) => (shape accu -> accu) -> Fix shape -> accu
+    -- fold fun = fun . fmap (fold fun) . unFix
+    ExFold mu f ->
+        let Right (MuType var t) = expandMuType sEnv mu
+            fold fun = fun . genmap CoVariant sEnv var t (fold fun)
+        in case eval' f of
+               Function fun -> Function $ fold fun
+               _ -> error "eval: first argument to ExFold not a function"
+
+    -- unfold :: (Functor shape) => (accu -> shape accu) -> accu -> Fix shape
+    -- unfold fun = Fix . fmap (unfold fun) . fun
+    ExUnfold nu f ->
+        let Right (NuType var t) = expandNuType sEnv nu
+            unfold fun = genmap CoVariant sEnv var t (unfold fun) . fun
+        in case eval' f of
+               Function fun -> Function $ unfold fun
+               _ -> error "eval: first argument to ExUnfold not a function"
+
+    ExUJump ->
+        let jump e = case e of
+                Event t v ->
+                    let (t', v') = case v of
+                                       ChoiceLeft v'  -> (One, v')
+                                       ChoiceRight e' -> jump e'
+                                       _ -> error "eval: inner argument to ExUJump not a choice"
+                    in (t + t', v')
+                _ -> error "eval: argument to ExUJump not an event"
+        in Function $ \e -> let (Succ t, v) = jump e in Event t v
+
+    ExUSwitch ->
+        let switch p = case p of
+                Pair (Behavior f) (Event t ~(Pair v p')) -> \t' -> case compare t' t of
+                    LT -> f t'
+                    EQ -> v
+                    GT -> switch p' (t' - t)
+                _ -> error "wrong argument type(s) to ExUSwitch"
+        in Function $ \p -> let f = switch p in Behavior f
+
+
+{- |
+    @genmap var sEnv v t f@ generates a generic comap\/contramap function for a type @t@ that
+    applies a function @f@ to values of a type @t@. If @var == CoVariant@ a comap function will be
+    produced, a contramap function for @var == ContraVariant@, where @v@ is the type variable the
+    map is generated for and @sEnv@ the list of type synonyms.
+-}
+genmap :: Variance -> TypeSynEnv -> Var -> Type -> (Value -> Value) -> Value -> Value
+genmap var sEnv v t f = case t of
+    TyZero -> id
+    TyUnit -> id
+    TyNat -> id
+
+    TyBehav t -> \e -> case e of
+        Behavior g -> Behavior $ genmap var sEnv v t f . g
+        _ -> error "genmap: value of type TyBehav is not a behavior"
+        
+    TyEvent t -> \e -> case e of
+        Event n e' -> Event n $ genmap var sEnv v t f e'
+        _ -> error "genmap: value of type TyBehav is not a behavior"
+
+    TyPair t1 t2 -> \e -> case e of
+        Pair e1 e2 -> Pair (genmap var sEnv v t1 f e1) (genmap var sEnv v t2 f e2)
+        _ -> error "genmap: value of type TyPair is not a pair"
+
+    TyPlus t1 t2 -> \e -> case e of
+        ChoiceLeft e'  -> ChoiceLeft $ genmap var sEnv v t1 f e'
+        ChoiceRight e' -> ChoiceRight $ genmap var sEnv v t2 f e'
+        _ -> error "genmap: value of type TyPlus is not a choice"
+
+    TyFun t1 t2 -> \e -> case e of
+{-
+        -- comap f function = comap f . function . contramap f
+        (Function g, CoVariant) -> Function $
+            genmap CoVariant sEnv rEnv t2 . g . genmap ContraVariant sEnv rEnv t1
+        -- contramap f function = contramap f . function . comap f
+        (Function g, ContraVariant) -> Function $
+            genmap ContraVariant sEnv rEnv t2 . g . genmap CoVariant sEnv rEnv t1
+-}
+        Function g -> Function $ genmap var sEnv v t2 f
+                                 . g . genmap (invertVariance var) sEnv v t1 f
+        _ -> error "genmap: value of type TyFun not a function"
+
+    TyApp v' [] | v' == v -> f
+    TyApp v' ts -> case expandTypeSyn sEnv v' ts of
+                       Left _  -> id
+                       Right t -> genmap var sEnv v t f
+
+    TyMu (MuType v' t') ->
+        -- TODO: TyUnit here assures we get the subtrees as they are. That is a type error but 
+        --       shouldn't be a problem for evaluation (only if v is mapped to a type including v
+        --       itself, which shouldn't happen). Should be thoroughly thought through, though :-)
+        let temp = TyUnit
+        in genmap var sEnv v (substVar v' temp t') f
+           . genmap var sEnv v' t' (genmap var sEnv v t f)
+
+    TyNu (NuType v' t') ->
+        -- TODO: see above
+        let temp = TyUnit
+        in genmap var sEnv v (substVar v' temp t') f
+           . genmap var sEnv v' t' (genmap var sEnv v t f)
+
+    TyVar _ -> error "genmap: called with TyVar"
+    TyCon _ -> error "genmap: called with TyCon"
+
+
+withNat :: (Integer -> Value) -> Value
+withNat f = Function $ \x -> case x of
+    Natural n -> f n
+    _ -> error "eval: function argument type mismatches expected type positive"
+
+-- | @replVar v val@ adds a new variable @v@ with a value @var@ to a list of variable-value-pairs,
+-- replacing the old value of @v@ if @v@ is already present.
+replVar v v' = ((v, v') :) . filter ((/= v) . fst)
diff --git a/Tempus/Examples/lightbulb.tp b/Tempus/Examples/lightbulb.tp
new file mode 100644
--- /dev/null
+++ b/Tempus/Examples/lightbulb.tp
@@ -0,0 +1,65 @@
+
+-- * Preparation
+
+    -- allNot : Behavior Bool → Behavior Bool
+    value allNot = λ b . Behavior (not (head b)) (const not ⊛ tail b)
+
+    -- allXor : Behavior Bool → Behavior Bool
+    value allXor = λ b₁ . λ b₂ . Behavior (xor (head b₁) (head b₂)) (const xor ⊛ tail b₁ ⊛ tail b₂)
+
+    type Ticks = ν σ . event σ
+
+    -- dropDummies : EventStream 1 → Ticks
+    value dropDummies = unfold [Ticks] (λ s . (const second) ⊙ (unpack [EventStream 1] s))
+
+    type Segments = ν σ . Behavior Bool × event σ
+
+    -- flip : Behavior Bool × event α → event (Behavior Bool × α)
+    value flip = λ p . const (onFirst allNot) ⊙ cut (first p) (second p)
+
+    -- step : Behavior Bool × Ticks → Behavior Bool × event (Behavior Bool × Ticks)
+    value step = λ p . (first p, flip (onSecond (unpack [Ticks]) p))
+
+    -- alternate : Behavior Bool → Ticks → Segments
+    value alternate = curry (unfold [Segments] step)
+
+    type UltraswitchArg = ν σ . behavior Bool × event (Bool × σ)
+
+    -- shiftRecPoints : behavior Bool × event Segments → UltraswitchArg
+    value shiftRecPoints = unfold [UltraswitchArg]
+                                  (onSecond (λ e . const (λ s . normalize (unpack [Segments] s)) ⊙ e))
+
+    -- ultraswitchArg : Segments → UltraswitchArg
+    value ultraswitchArg = λ s . shiftRecPoints (tail (first (unpack [Segments] s)),
+                                                 second (unpack [Segments] s))
+
+    -- prepareUltraswitch : Behavior Bool → EventStream 1 → nu s . behavior Bool × event (Bool × s)
+    value prepareUltraswitch = λ b . λ s . ultraswitchArg (alternate b (dropDummies s))
+
+-- * Actual example
+
+    -- control : Behavior Bool → EventStream 1 → Behavior Bool
+    value control = λ b . λ s . Behavior (head b) (ultraswitch (prepareUltraswitch b s))
+
+    -- init : Bool
+    value init = false
+
+    -- one : EventStream 1 → Behavior Bool
+    value one = control (Behavior init (const init))
+
+    -- two : EventStream 1 → EventStream 1 → Behavior Bool
+    value two = λ s₁ . λ s₂ . allXor (one s₁) (one s₂)
+
+-- * Test cases
+
+    -- s₁ : EventStream 1
+    value s₁ = pack [EventStream 1] (event 2 ((),
+               pack [EventStream 1] (const ? ⊙ never)))
+
+    -- s₂ : EventStream 1
+    value s₂ = pack [EventStream 1] (event 4 ((),
+               pack [EventStream 1] (event 1 ((),
+               pack [EventStream 1] (const ? ⊙ never)))))
+
+    -- test : Behavior Bool
+    value test = two s₁ s₂
diff --git a/Tempus/Interpreter.hs b/Tempus/Interpreter.hs
new file mode 100644
--- /dev/null
+++ b/Tempus/Interpreter.hs
@@ -0,0 +1,293 @@
+-- | The interpreter REPL.
+module Tempus.Interpreter (
+    repl
+) where
+
+
+import Control.Arrow
+import Control.Monad
+import Control.Monad.Trans
+
+import Data.Char
+import Data.List
+import Data.Maybe
+
+import           System.Console.Haskeline
+import           System.Directory
+import           System.FilePath
+import qualified System.IO.UTF8 as BU
+
+import Tempus.Loc
+import Tempus.Syntax
+import Tempus.Parser
+import Tempus.TypeCheck
+import Tempus.Evaluation
+
+
+version :: String
+version = "0.1.0"
+
+executableName :: String
+executableName = "tempus"
+
+-- | The state of the interpreter.
+data IState = IState {
+                  -- | The path of the file the current module was loaded from, or @Nothing@ if no
+                  -- one is loaded.
+                  modulePath :: Maybe FilePath,
+
+                  -- TODO: merge typeEnv and evalEnv
+                  -- | A list of all global variables from the currently loaded module and added
+                  -- interactively with their corresponding inferred type.
+                  typeEnv :: TypeEnv,
+
+                  -- | A list of all type synonyms from the currently loaded module and added
+                  -- interactively.
+                  synEnv :: TypeSynEnv,
+
+                  -- | Like @typeEnv@ but with the expressions of the variables.
+                  evalEnv :: EvalEnv,
+
+                  -- | A triple with the same lists as @typeEnv@, @synEnv@, and @evalEnv@ but only
+                  -- including variables and types from the Prelude module.
+                  preludeEnvs :: (TypeEnv, TypeSynEnv, EvalEnv)
+              }
+
+-- | Initial interpreter state with empty lists and no module path.
+initIState :: IState
+initIState = IState {
+        modulePath = Nothing,
+        typeEnv = [],
+        synEnv  = [],
+        evalEnv = [],
+        preludeEnvs = ([], [], [])
+    }
+
+mergedTypeEnv st@IState { preludeEnvs = (vs, _, _) } = vs ++ typeEnv st
+mergedSynEnv  st@IState { preludeEnvs = (_, ts, _) } = ts ++ synEnv st
+mergedEvalEnv st@IState { preludeEnvs = (_, _, es) } = es ++ evalEnv st
+
+
+-- TODO: Allow redeclaration of values/types
+-- TODO: Catch Ctrl-C
+-- | The main interpreter REPL loop with an optional path to a Prelude file that is loaded at
+-- the start.
+repl :: Maybe FilePath -> IO ()
+repl preludePath = runInputT defaultSettings $ do
+    outputStrLn $ "This is " ++ executableName ++ " version " ++ version
+
+    mbInitSt <- maybe (return Nothing) (loadModule [] [] False) preludePath
+    case mbInitSt of
+        Nothing -> do
+            outputStrLn "Warning: Loading the Prelude module failed!"
+            loop initIState
+        Just (vs, ts, es) -> do
+            outputStrLn $ "Loaded Prelude module from file `" ++ fromJust preludePath ++ "'."
+            loop $ initIState { preludeEnvs = (vs, ts, es) }
+
+    where
+      loop st = do
+        let moduleName = maybe "" takeBaseName $ modulePath st
+        input <- getInputLine $ moduleName ++ "> "
+        case input >>= parseAction of
+            Just (Command "?" _) -> do
+                mapM_ outputStrLn helpLines
+                loop st
+
+            Just (Command "q" _) -> do
+                outputStrLn $ "Leaving " ++ executableName ++ "."
+
+            Just (Command "l" []) -> do
+                outputStrLn $ "Unloading module."
+                loop st { modulePath = Nothing, typeEnv = [], synEnv = [], evalEnv = [] }
+
+            Just (Command "l" [path]) -> do
+                let (tEnv, sEnv, _) = preludeEnvs st
+                mbSt <- loadModule tEnv sEnv True path
+                case mbSt of
+                    Nothing           -> loop st
+                    Just (vs, ts, es) -> loop st { modulePath = Just path,
+                                                   typeEnv = vs,
+                                                   synEnv  = ts,
+                                                   evalEnv = es }
+
+            Just (Command "v" []) -> do
+                showEnvironments (typeEnv st, synEnv st, evalEnv st)
+                loop st
+
+            Just (Command "p" []) -> do
+                showEnvironments $ preludeEnvs st
+                loop st
+
+            Just (Command "t" [s]) -> do
+                case parseExpr s of
+                    Left (Loc loc err) -> do
+                        outputStrLn $ "*** parse error: " ++ show loc ++ ": " ++ err
+                    Right expr -> do
+                        case getType (mergedTypeEnv st) (mergedSynEnv st) (Loc (0,0) expr) of
+                            Left (Loc _ err) -> outputStrLn $ "*** type error: " ++ showTypeErr err
+                            Right t          -> do
+                                outputStrLn $ "  " ++ show (SrcCode expr)
+                                outputStrLn $ "    : " ++ show (SrcCode t)
+                loop st
+
+            Just (Expression s) -> do
+                case parseExpr s of
+                    Left (Loc loc err) -> do
+                        outputStrLn $ "*** parse error: " ++ show loc ++ ": " ++ err
+                    Right expr -> do
+                        case getType (mergedTypeEnv st) (mergedSynEnv st) (Loc (0,0) expr) of
+                            Left (Loc _ err) -> outputStrLn $ "*** type error: " ++ showTypeErr err
+                            Right t          -> liftIO $ putStrLn $ show $
+                                evalExpr (mergedSynEnv st) (mergedTypeEnv st) (mergedEvalEnv st) expr
+                loop st
+
+            Just (Declaration s) -> do
+                case parseDecl s of
+                    Left (Loc loc err) -> do
+                        outputStrLn $ "*** parse error: " ++ show loc ++ ": " ++ err
+                        loop st
+                    Right decl -> do
+                        let tEnv = mergedTypeEnv st
+                            sEnv = mergedSynEnv st
+                        case checkProgram tEnv sEnv [decl] of
+                            Left (Loc loc err) -> do
+                                outputStrLn $
+                                    "*** type error: " ++ show loc ++ ": " ++ showTypeErr err
+                                loop st
+                            -- DeclVal
+                            Right (vs@[(v, (_,t))], []) -> do
+                                outputStrLn $ "  " ++ show (SrcCode v) ++ " : " ++ show (SrcCode t)
+                                loop st { typeEnv = typeEnv st ++ vs,
+                                          evalEnv = evalEnv st ++
+                                                        [(v, let DeclVal _ _ e = decl in e )] }
+                            -- DeclType
+                            Right ([], ts@[_]) -> do
+                                outputStrLn $ "  " ++ show (SrcCode decl)
+                                loop st { synEnv = synEnv st ++ ts }
+
+            _ -> do
+                outputStrLn $ "Unknown command, try :? for help."
+                loop st
+
+
+-- | The list of lines to be displayed on @:?@.
+helpLines :: [String]
+helpLines = [
+     -- "|                                                                              |"
+        "  Available commands:", 
+        "    :?                 Show this help",
+        "    :q                 Quit",
+        "    :l                 Unload the current loaded module",
+        "    :l <file>          Load the module in file <file>",
+        "    :v                 Show types of all currently loaded module variables",
+        "    :p                 Show types of all Prelude variables",
+        "    :t <expr>          Show the type of expression <expr>",
+        "    <decl>             Depending on the declaration <decl>, bring a new value",
+        "                       or type synonym into scope",
+        "    <expr>             Evaluate the expression <expr>"
+    ]
+
+-- | Produces an error message string for the given context error.
+showTypeErr :: ContextError -> String
+showTypeErr err = case err of
+    UndefinedVariable v -> "undefined variable `" ++ show (SrcCode v) ++ "'"
+    DuplicateVariable v -> "variable `" ++ show (SrcCode v) ++ "' already defined"
+    DuplicateType v -> "type `" ++ show (SrcCode v) ++ "' already defined"
+    OccursCheck t1 t2 -> "cannot construct the infinite type " ++ show (SrcCode t1)
+                              ++ " = " ++ show (SrcCode t2)
+    SymbolClash t1 t2 -> "cannot match type " ++ show (SrcCode t1) ++ " with " ++ show (SrcCode t2)
+    IncorrectVariances t -> "incorrect variances in type " ++ show (SrcCode t)
+    UndefinedType v -> "undefiend type variable `" ++ show (SrcCode v) ++ "'"
+    TypeArgsMismatch v -> "wrong number of arguments to type synonym `" ++ show (SrcCode v) ++ "'"
+    NoMuType t -> "type " ++ show (SrcCode t) ++ " is not a mu type"
+    NoNuType t -> "type " ++ show (SrcCode t) ++ " is not a nu type"
+    NoRecType t -> "type " ++ show (SrcCode t) ++ " is neither a mu nor a nu type"
+
+
+{- |
+    Reads an UTF8 encoded file and returns the file content. This function prevents that a file
+    is read lazily and is so being kept in a locked state if a parser error occurs before the
+    complete file was processed.
+-}
+seqReadFile :: FilePath -> IO String
+seqReadFile = fmap (\s -> length s `seq` s) . BU.readFile
+
+
+{- |
+    @loadModule tEnv sEnv verbose path@ reads a Tempus module from @path@ and parses and typechecks
+    all definitions where the types from @tEnv@ and @tSyn@ can be used. The result are the lists
+    of all variables with types, type synonyms and variables with expression from that module.
+    If @verbose == True@ all type synonyms and variables with the inferred types are printed.
+-}
+loadModule :: TypeEnv -> TypeSynEnv -> Bool -> FilePath
+           -> InputT IO (Maybe (TypeEnv, TypeSynEnv, EvalEnv))
+loadModule tEnv sEnv verbose path = do
+    exists <- liftIO $ doesFileExist path
+    if exists
+        then do
+            s <- liftIO $ seqReadFile path
+            case parseProgram s of
+                Left (Loc loc err) -> do
+                    outputStrLn $ "*** parse error: " ++ show loc ++ ": " ++ err
+                    return Nothing
+
+                Right prog -> case checkProgram tEnv sEnv prog of
+                    Left (Loc loc err) -> do
+                        outputStrLn $ "*** type error: " ++ show loc ++ ": " ++ showTypeErr err
+                        return Nothing
+
+                    Right (vs, ts) -> do
+                        when verbose $ do
+                            forM_ ts $ \(v, (vs, t)) ->
+                                outputStrLn $ "  " ++ show (SrcCode $ DeclType (0,0) v vs t)
+                            forM_ vs $ \(v, (_, t)) ->
+                                outputStrLn $ "  " ++ show (SrcCode v) ++ " : " ++ show (SrcCode t)
+                        return $ Just (vs, ts, zip (map fst vs) [e | DeclVal _ _ e <- prog])
+        else do
+            outputStrLn $ "File not found: " ++ path
+            return Nothing
+
+-- | Prints a list of type synonyms and variables with their types.
+showEnvironments :: (TypeEnv, TypeSynEnv, EvalEnv) -> InputT IO ()
+showEnvironments (tEnv, sEnv, eEnv) = do
+    case zipWith (\(v, (_, t)) (_, e) -> (v, e, t)) tEnv eEnv of
+        []  -> outputStrLn $ "No variables loaded."
+        env -> do
+            outputStrLn $ "Loaded variables: "
+            forM_ env $ \(v, e, t) -> outputStrLn $
+                "  " ++ show (SrcCode v) ++
+                -- " = " ++ show (SrcCode e) ++
+                " : " ++ show (SrcCode t)
+
+    case sEnv of
+        []  -> outputStrLn $ "No type synonyms loaded."
+        env -> do
+            outputStrLn $ "Loaded type synonyms: "
+            forM_ env $ \(v, (vs, t)) -> outputStrLn $
+                "  " ++ show (SrcCode $ DeclType (0,0) v vs t)
+    
+-- | An interpreter action.
+data Action = Command String [String]
+              -- ^ A generic command with the list of parameters.
+            | Expression String
+              -- ^ An expression.
+            | Declaration String
+              -- ^ A type or value definition.
+
+-- TODO: parse filenames with spaces correctly
+-- TODO: better type/value parsing
+-- | Parses a string command to an interpreter action or returns @Nothing@ if the parsing failed.
+parseAction :: String -> Maybe Action
+parseAction (':':'t':c:cs)
+    | isSpace c = Just $ Command "t" [cs]
+parseAction (':':cmd) = case words cmd of
+                            []     -> Nothing
+                            (c:cs) -> Just $ Command c cs
+parseAction s
+    | "value " `isPrefixOf` s = Just $ Declaration s
+    | "type " `isPrefixOf` s = Just $ Declaration s
+parseAction s@(c:cs)
+    | isSpace c = parseAction $ dropWhile isSpace cs
+    | otherwise = Just $ Expression s
+parseAction _ = Nothing
diff --git a/Tempus/Lexer.hs b/Tempus/Lexer.hs
new file mode 100644
--- /dev/null
+++ b/Tempus/Lexer.hs
@@ -0,0 +1,326 @@
+-- | Tokenizing of Tempus source code.
+module Tempus.Lexer (
+    Token (..),
+    showToken,
+    lex,
+    tokenize,
+
+    Parser (..),
+    ParseResult,
+    initParser
+) where
+
+
+import Prelude hiding (lex)
+
+import Control.Applicative
+import Control.Monad.State
+
+import Data.Char
+import Data.List (unfoldr)
+import Data.Maybe (fromMaybe)
+
+import Tempus.Loc
+
+
+-- * Tokens
+
+-- | The input tokens for a Tempus parser.
+data Token = EOF
+           | Variable String
+           | NatLit Integer
+           | Equals
+           | ArrowRight
+           | Plus
+           | Times
+           | ParenOpen
+           | ParenClose
+           | Zero
+           | One
+           | Mu
+           | Nu
+           | Dot
+           | Comma
+           | Lambda
+           | SquareOpen
+           | SquareClose
+           | AngleOpen
+           | AngleClose
+           | CircledAsterisk
+           | CircledDot
+           | QuestionMark
+
+           | KWBehavior
+           | KWCase
+           | KWConst
+           | KWEvent
+           | KWExpand
+           | KWFirst
+           | KWFold
+           | KWLeft
+           | KWNever
+           | KWPack
+           | KWPositive
+           | KWRace
+           | KWReflect
+           | KWRight
+           | KWSecond
+           | KWUltraswitch
+           | KWType
+           | KWUltrajump
+           | KWUnfold
+           | KWUnpack
+           | KWValue
+           deriving (Show, Eq)
+
+
+-- TODO: support unicode output
+-- | Return the ASCII symbol or keyword, or a descriptive text for a token.
+showToken :: Token -> String
+showToken tok = case tok of
+    EOF             -> "end of file"
+    Variable v      -> v
+    NatLit i        -> show i
+    Equals          -> "="
+    ArrowRight      -> "->"
+    Plus            -> "+"
+    Times           -> "*"
+    ParenOpen       -> "("
+    ParenClose      -> ")"
+    Zero            -> "0"
+    One             -> "1"
+    Mu              -> "mu"
+    Nu              -> "nu"
+    Dot             -> "."
+    Comma           -> ","
+    Lambda          -> "\\"
+    SquareOpen      -> "["
+    SquareClose     -> "]"
+    AngleOpen       -> "opening angle bracket"
+    AngleClose      -> "closing angle bracket"
+    CircledAsterisk -> "<*>"
+    CircledDot      -> "<.>"
+    QuestionMark    -> "?"
+    KWBehavior      -> "behavior"
+    KWCase          -> "case"
+    KWConst         -> "const"
+    KWEvent         -> "event"
+    KWExpand        -> "expand"
+    KWFirst         -> "first"
+    KWFold          -> "fold"
+    KWLeft          -> "left"
+    KWNever         -> "never"
+    KWPack          -> "pack"
+    KWPositive      -> "positive"
+    KWRace          -> "race"
+    KWReflect       -> "reflect"
+    KWRight         -> "right"
+    KWSecond        -> "second"
+    KWUltraswitch   -> "ultraswitch"
+    KWType          -> "type"
+    KWUltrajump     -> "ultrajump"
+    KWUnfold        -> "unfold"
+    KWUnpack        -> "unpack"
+    KWValue         -> "value"
+
+
+-- | The list of keyword and symbol strings with their corresponding token.
+reserved :: [(String, Token)]
+reserved = [
+        -- keywords
+        ("type", KWType),
+        ("value", KWValue),
+        ("behavior", KWBehavior),
+        ("event", KWEvent),
+        ("expand", KWExpand),
+        ("positive", KWPositive),
+        ("\x2115\x208A", KWPositive),
+        ("fold", KWFold),
+        ("unfold", KWUnfold),
+        ("const", KWConst),
+        ("left", KWLeft),
+        ("right", KWRight),
+        ("case", KWCase),
+        ("first", KWFirst),
+        ("second", KWSecond),
+        ("never", KWNever),
+        ("race", KWRace),
+        ("reflect", KWReflect),
+        ("pack", KWPack),
+        ("unpack", KWUnpack),
+        ("ultraswitch", KWUltraswitch),
+        ("ultrajump", KWUltrajump),
+
+        -- symbols
+        ("\x03BC", Mu),
+        ("mu", Mu),
+        ("\x03BD", Nu),
+        ("nu", Nu),
+        ("\x2192", ArrowRight),
+        ("->", ArrowRight),
+        ("+", Plus),
+        ("\xD7", Times),
+        ("*", Times),
+        ("\x03BB", Lambda),
+        ("\\", Lambda),
+        ("\x229B", CircledAsterisk),
+        ("<*>", CircledAsterisk),
+        ("\x2299", CircledDot),
+        ("<.>", CircledDot),
+        ("=", Equals),
+        (".", Dot),
+        ("?", QuestionMark)
+    ]
+
+-- | The list of brackets with a special meaning and their corresponding token.
+brackets :: [(Char, Token)]
+brackets = [
+        ('(', ParenOpen),
+        (')', ParenClose),
+        ('[', SquareOpen),
+        (']', SquareClose),
+        ('\x27E8', AngleOpen),
+        ('\x27E9', AngleClose)
+    ]
+
+
+
+-- * Lexer
+
+-- | The lexer monad.
+type Lexer a = State LexerState a
+
+-- | The lexer state.
+data LexerState = LexerState {
+                      input :: String,
+                      -- ^ The residual input string.
+                      loc :: SrcLoc
+                      -- ^ The current location in the original input string.
+                  }
+                  deriving (Show, Eq)
+
+
+-- ** Primitive lexers
+
+-- | Modify the input string of the current lexer state by the function.
+modifyInput :: (String -> String) -> Lexer ()
+modifyInput f = modify (\st -> st { input = f $ input st })
+
+-- | Modify the location of the current lexer state.
+modifyLoc :: (Int -> Int, Int -> Int) -> Lexer ()
+modifyLoc (fl, fc) = modify (\st -> st { loc = let (l, c) = loc st in (fl l, fc c) })
+
+-- | Discard the first @n@ characters of the current input string.
+discard :: Int -> Lexer ()
+discard n = modifyInput (drop n) >> modifyLoc (id, (+ n))
+
+
+-- | Read all subsequent characters satisfying a certain predicate from the input string and
+-- return the read characters.
+lexWhile :: (Char -> Bool) -> Lexer String
+lexWhile p = do
+    s <- gets input
+    let (s', rest) = span p s
+    modifyInput (const rest)
+    modifyLoc (id, (+ length s'))
+    return s'
+
+
+-- ** Tempus token lexers
+
+-- | Lexes a single token discarding all whitespace before that token.
+lexInput :: Lexer (Maybe Token)
+lexInput = do
+    s <- gets input
+    case s of
+        [] -> return $ Just EOF
+        _  -> Just <$> lexToken >>= \t -> lexWhitespace >> return t
+
+-- | Lexes all whitespace, including single line comments.
+lexWhitespace :: Lexer ()
+lexWhitespace = do
+    s <- gets input
+    case s of
+        '-':'-':c:_ | isSpace c -> lexWhile (/= '\n') >> lexWhitespace
+        '\n':_ -> discard 1 >> modifyLoc (succ, const 1) >> lexWhitespace
+        c:_ | isSpace c -> discard 1 >> lexWhitespace
+        _ -> return ()
+
+-- | Returns true iff the symbol is a bracket, i.e. has the general Unicode category
+-- @OpenPunctuation@ or @ClosePunctuation@.
+isBracket :: Char -> Bool
+isBracket c = generalCategory c `elem` [OpenPunctuation, ClosePunctuation]
+
+-- | Converts the string representation of a decimal number to an @Integer@.
+stringToNat :: String -> Integer
+stringToNat = foldl (\a -> (10*a +) . toInteger . digitToInt) 0
+
+-- | Lexes a single token.
+lexToken :: Lexer Token
+lexToken = do
+    s <- gets input
+    case s of
+        -- make whitespace around commas optional
+        ',':_ -> discard 1 >> return Comma
+
+            -- brackets
+        c:_ | isBracket c -> do
+                discard 1
+                return $ fromMaybe (Variable [c]) $ lookup c brackets
+
+            -- all other identifiers
+            | otherwise -> do
+                ids <- lexWhile (\c -> not $ isSpace c || isBracket c || c == ',')
+                case ids of
+                    "0" -> return Zero
+                    "1" -> return One
+                    _ | all isDigit ids -> let n = stringToNat ids
+                                           in return $ if n == 0 then Variable ids
+                                                                 else NatLit n
+                    _ -> return $ fromMaybe (Variable ids) $ lookup ids reserved
+
+        _ -> fail $ "lexToken: interal error"
+
+
+{- |
+    Runs a lexer inside the parser monad. A new parser is constructed that runs the lexer,
+    applies the read token to the passed continuation and runs the resulting parser of the
+    continuation with the new input string and location.
+-}
+lex :: (Loc Token -> Parser a) -> Parser a
+lex cont = Parser $ \s loc ->
+    case runState lexInput $ LexerState s loc of
+        (Nothing, _) -> Left $ Loc loc $ "lexer error at " ++ showSrcLoc loc
+        (Just t, LexerState s' loc') -> runParser (cont (Loc loc t)) s' loc'
+
+-- | Tokenizes a string to a list of @Token@ values with their corresponding locations. This
+-- function can be used for testing purposes.
+tokenize :: String -> [Loc Token]
+tokenize s = run . snd . runState lexWhitespace $ LexerState s (1,1)
+    where
+        run st = case runState lexInput st of
+            (Nothing, _)    -> []
+            (Just EOF, _)   -> []
+            (Just tok, st') -> Loc (loc st) tok : run st'
+
+
+-- * Parser monad
+
+-- | Parser result which is either an error message with the location the error occured or a value.
+type ParseResult a = Either (Loc String) a
+
+-- | Type for the parser monad.
+newtype Parser a = Parser { runParser :: String -> SrcLoc -> ParseResult a }
+
+instance Monad Parser where
+    return a = Parser $ \_ _   -> Right a
+    p >>= f  = Parser $ \s loc -> case runParser p s loc of
+                                      Left e  -> Left e
+                                      Right a -> runParser (f a) s loc
+    fail s   = Parser $ \_ loc -> Left $ Loc loc s
+
+
+-- | Initializes a parser by lexing all whitespace before the first token.
+initParser :: Parser a -> String -> ParseResult a
+initParser p s = let (_, LexerState s' loc') = runState lexWhitespace $ LexerState s (1,1)
+                 in runParser p s' loc'
diff --git a/Tempus/Loc.hs b/Tempus/Loc.hs
new file mode 100644
--- /dev/null
+++ b/Tempus/Loc.hs
@@ -0,0 +1,23 @@
+-- | Support for source locations.
+module Tempus.Loc (
+    SrcLoc,
+    showSrcLoc,
+
+    Loc (..),
+    unLoc
+) where
+
+
+-- | A source location, where the first value indicates the line and the second the column number
+type SrcLoc = (Int, Int)
+
+-- | Converts a source location to a string.
+showSrcLoc :: SrcLoc -> String
+showSrcLoc (l, c) = concat [show l, ":", show c]
+
+-- | A value together with a source location.
+data Loc a = Loc SrcLoc a deriving (Show, Eq)
+
+-- | Unwraps the value and discards the location.
+unLoc :: Loc a -> a
+unLoc (Loc _ a) = a
diff --git a/Tempus/Main.hs b/Tempus/Main.hs
new file mode 100644
--- /dev/null
+++ b/Tempus/Main.hs
@@ -0,0 +1,20 @@
+module Main (main) where
+
+import Paths_tempus
+
+import Control.Monad
+
+import System.Environment.Executable
+import System.Directory
+import System.FilePath
+
+import Tempus.Interpreter
+
+
+main :: IO ()
+main = do
+    (path1, _) <- splitExecutablePath
+    path2 <- getDataDir
+    files <- filterM doesFileExist . map (</> "Prelude.tp") $ [".", path1, path2]
+
+    repl $ head $ take 1 (map Just files) ++ [Nothing]
diff --git a/Tempus/Parser.y b/Tempus/Parser.y
new file mode 100644
--- /dev/null
+++ b/Tempus/Parser.y
@@ -0,0 +1,226 @@
+{
+{-# OPTIONS_GHC -w #-}
+module Tempus.Parser (
+    parseProgram,
+    parseDecl,
+    parseType,
+    parseExpr
+) where
+
+import Prelude hiding (lex)
+
+import Tempus.Loc
+import Tempus.Lexer
+import Tempus.Syntax
+
+}
+
+%name pparseProgram prog
+%name pparseDecl decl
+%name pparseType type
+%name pparseExpr expr
+
+%tokentype { Loc Token }
+%monad { Parser }
+%lexer { lex } { Loc _ EOF }
+
+%error { parseError }
+%token
+    var             { Loc _ (Variable _) }
+    natlit          { Loc _ (NatLit _) }
+    '='             { Loc $$ Equals }
+    '->'            { Loc $$ ArrowRight }
+    '+'             { Loc $$ Plus }
+    '*'             { Loc $$ Times }
+    '('             { Loc $$ ParenOpen }
+    ')'             { Loc $$ ParenClose }
+    '0'             { Loc $$ Zero }
+    '1'             { Loc $$ One }
+    mu              { Loc $$ Mu }
+    nu              { Loc $$ Nu }
+    '.'             { Loc $$ Dot }
+    ','             { Loc $$ Comma }
+    lam             { Loc $$ Lambda }
+    '['             { Loc $$ SquareOpen }
+    ']'             { Loc $$ SquareClose }
+    langle          { Loc $$ AngleOpen }
+    rangle          { Loc $$ AngleClose }
+    '<*>'           { Loc $$ CircledAsterisk }
+    '<.>'           { Loc $$ CircledDot }
+    '?'             { Loc $$ QuestionMark }
+    'behavior'      { Loc $$ KWBehavior }
+    'case'          { Loc $$ KWCase }
+    'const'         { Loc $$ KWConst }
+    'event'         { Loc $$ KWEvent }
+    'expand'        { Loc $$ KWExpand }
+    'first'         { Loc $$ KWFirst }
+    'fold'          { Loc $$ KWFold }
+    'left'          { Loc $$ KWLeft }
+    'positive'      { Loc $$ KWPositive }
+    'never'         { Loc $$ KWNever }
+    'pack'          { Loc $$ KWPack }
+    'race'          { Loc $$ KWRace }
+    'reflect'       { Loc $$ KWReflect }
+    'right'         { Loc $$ KWRight }
+    'second'        { Loc $$ KWSecond }
+    'ultraswitch'   { Loc $$ KWUltraswitch }
+    'type'          { Loc $$ KWType }
+    'ultrajump'     { Loc $$ KWUltrajump }
+    'unfold'        { Loc $$ KWUnfold }
+    'unpack'        { Loc $$ KWUnpack }
+    'value'         { Loc $$ KWValue }
+
+%%
+
+prog        :: { Program }
+prog        : decls                             { reverse $1 }
+
+decls       :: { [Decl] }
+decls       :                                   { [] }
+            | decls decl                        { $2 : $1 }
+
+decl        :: { Decl }
+decl        : typedecl                          { $1 }
+            | valdecl                           { $1 }
+
+typedecl    :: { Decl }
+typedecl    : 'type' var formalargs '=' type    { DeclType $1 (var $2) (reverse $3) $5 }
+
+formalargs  :: { [Var] }
+formalargs  :                                   { [] }
+            | formalargs var                    { var $2 : $1 }
+
+valdecl     :: { Decl }
+valdecl     : 'value' var '=' expr              { DeclVal $1 (var $2) $4 }
+
+type        :: { Type }
+type        : type0                             { $1 }
+
+type0       :: { Type }
+type0       : mutype                            { TyMu $1 }
+            | nutype                            { TyNu $1 }
+            | type1                             { $1 }
+
+type1       :: { Type }
+type1       : type2 '->' type1                  { TyFun $1 $3 }
+            | type2                             { $1 }
+
+type2       :: { Type }
+type2       : type3 '+' type2                   { TyPlus $1 $3 }
+            | type3                             { $1 }
+
+type3       :: { Type }
+type3       : type4 '*' type3                   { TyPair $1 $3 }
+            | type4                             { $1 }
+
+type4       :: { Type }
+type4       : var typeargs                      { TyApp (var $1) $2 }
+            | 'behavior' type5                  { TyBehav $2 }
+            | 'event' type5                     { TyEvent $2 }
+            | type5                             { $1 }
+
+type5       :: { Type }
+type5       : var                               { TyApp (var $1) [] }
+            | 'positive'                        { TyNat }
+            | '(' type0 ')'                     { $2 }
+            | '0'                               { TyZero }
+            | '1'                               { TyUnit }
+
+typeargs    :: { [Type] }
+typeargs    : type5                             { [$1] }
+            | typeargs type5                    { $2 : $1 }
+
+mutype      :: { MuType }
+mutype      : mu var '.' type0                  { MuType (var $2) $4 }
+
+nutype      :: { NuType }
+nutype      : nu var '.' type0                  { NuType (var $2) $4 }
+
+expr        :: { Expr }
+expr        : expr0                             { $1 }
+
+expr0       :: { Expr }
+expr0       : expr1 ',' expr0                   { ExPair $1 $3 }
+            | expr1                             { $1 }
+
+expr1       :: { Expr }
+expr1       : lam var '.' expr1                 { ExLam (var $2) $4 }
+            | expr2                             { $1 }
+
+expr2       :: { Expr }
+expr2       : expr2 '<*>' expr3                 { ExLiftAppB $1 $3 }
+            | expr2 '<.>' expr3                 { ExLiftAppE $1 $3 }
+            | expr3                             { $1 }
+
+expr3       :: { Expr }
+expr3       : expr3 expr4                       { ExApp $1 $2 }
+            | 'const' expr4                     { ExConst $2 }
+            | 'behavior' expr4                  { ExBehav $2 }
+            | 'event' expr4 expr4               { ExEvent $2 $3 }
+            | foldvals '[' type ']' expr4       { $1 $3 $5 }
+            | expr4                             { $1 }
+
+expr4       :: { Expr }
+expr4       : var                               { ExVar $ var $1 }
+            | '1'                               { ExNatLit 1 }
+            | natlit                            { ExNatLit $ nat $1 }
+            | '(' expr0 ')'                     { $2 }
+            | '?'                               { ExNull }
+            | langle rangle                     { ExUnit }
+            | '(' ')'                           { ExUnit }
+            | packvals '[' type ']'             { $1 $3 }
+            | baseval                           { $1 }
+
+foldvals    :: { Type -> Expr -> Expr }
+foldvals    : 'fold'                            { ExFold }
+            | 'unfold'                          { ExUnfold }
+
+packvals    :: { Type -> Expr }
+packvals    : 'pack'                            { ExPack }
+            | 'unpack'                          { ExUnpack }
+
+baseval     :: { Expr }
+baseval     : 'left'                            { ExLeft }
+            | 'right'                           { ExRight }
+            | 'case'                            { ExCase }
+            | 'first'                           { ExFst }
+            | 'second'                          { ExSnd }
+            | 'expand'                          { ExExpand }
+            | 'never'                           { ExNever }
+            | 'race'                            { ExRace }
+            | 'reflect'                         { ExReflect }
+            | 'ultraswitch'                     { ExUSwitch }
+            | 'ultrajump'                       { ExUJump }
+
+
+{
+
+-- | Parses a complete Tempus program.
+parseProgram :: String -> ParseResult Program
+parseProgram = initParser pparseProgram
+
+-- | Parses a single Tempus type or value declaration.
+parseDecl :: String -> ParseResult Decl
+parseDecl = initParser pparseDecl
+
+-- | Parses a Tempus type expression.
+parseType :: String -> ParseResult Type
+parseType = initParser pparseType
+
+-- | Parses a Tempus expression.
+parseExpr :: String -> ParseResult Expr
+parseExpr = initParser pparseExpr
+
+
+var :: Loc Token -> Var
+var (Loc _ (Variable v)) = Var v
+var _ = error "internal parser error: unexpected token in var"
+
+nat :: Loc Token -> Integer
+nat (Loc _ (NatLit i)) = i
+nat _ = error "internal parser error: unexpected token in nat"
+
+parseError :: Loc Token -> Parser a
+parseError (Loc loc tok) = fail $ "error parsing token `" ++ showToken tok ++ "' at " ++ show loc
+
+}
diff --git a/Tempus/Syntax.hs b/Tempus/Syntax.hs
new file mode 100644
--- /dev/null
+++ b/Tempus/Syntax.hs
@@ -0,0 +1,186 @@
+{-# LANGUAGE DeriveDataTypeable, FlexibleInstances #-}
+
+-- | Tempus abstract syntax tree types.
+module Tempus.Syntax (
+    Program,
+    Decl (..),
+    Type (..),
+    MuType (..),
+    NuType (..),
+    Expr (..),
+    Var (..),
+
+    SrcCode (..)
+) where
+
+import Data.Data
+import Data.Generics.Uniplate.Data ()
+import Data.List
+
+import Tempus.Loc
+
+
+-- | A Tempus program as a list of definitions.
+type Program = [Decl]
+
+-- | A Tempus type or value definition.
+data Decl = DeclType SrcLoc Var [Var] Type
+          | DeclVal SrcLoc Var Expr
+          deriving (Eq, Show)
+
+
+-- | A Tempus type.
+data Type = TyMu MuType
+          | TyNu NuType
+          | TyFun Type Type
+          | TyPlus Type Type
+          | TyPair Type Type
+          | TyApp Var [Type]
+          | TyBehav Type
+          | TyEvent Type
+          | TyNat
+          | TyZero
+          | TyUnit
+
+          -- only used for type checking
+          | TyVar Integer
+          | TyCon Integer
+          deriving (Eq, Show, Data, Typeable)
+
+
+-- | A mu type.
+data MuType = MuType Var Type
+            deriving (Eq, Show, Data, Typeable)
+
+
+-- | A nu type.
+data NuType = NuType Var Type
+            deriving (Eq, Show, Data, Typeable)
+
+
+-- | A Tempus expression.
+data Expr = ExPair Expr Expr
+          | ExLam Var Expr
+          | ExLiftAppB Expr Expr
+          | ExLiftAppE Expr Expr
+          | ExApp Expr Expr
+          | ExConst Expr
+          | ExVar Var
+          | ExNatLit Integer
+          | ExBehav Expr
+          | ExEvent Expr Expr
+          | ExNull
+          | ExUnit
+          | ExLeft
+          | ExRight
+          | ExCase
+          | ExExpand
+          | ExFst
+          | ExSnd
+          | ExNever
+          | ExRace
+          | ExReflect
+          | ExFold Type Expr
+          | ExUnfold Type Expr
+          | ExPack Type
+          | ExUnpack Type
+          | ExUJump
+          | ExUSwitch
+          deriving (Eq, Show, Data, Typeable)
+
+
+-- | A variable.
+newtype Var = Var String deriving (Eq, Show, Data, Typeable)
+
+
+-- | Wrapper for displaying values as source code.
+newtype SrcCode a = SrcCode a
+
+instance Show (SrcCode Decl) where
+    showsPrec _ (SrcCode (DeclType _ v vs t)) = 
+        showString "type " . showsVars (map SrcCode (v:vs)) . showString " = " . shows (SrcCode t)
+    showsPrec _ (SrcCode (DeclVal _ v e)) = 
+        showString "value " . shows (SrcCode v) . showString " = " . shows (SrcCode e)
+
+showsVars :: [SrcCode Var] -> ShowS
+showsVars []     = id
+showsVars [v]    = shows v
+showsVars (v:vs) = shows v . showChar ' ' . showsVars vs
+
+instance Show (SrcCode Expr) where
+    showsPrec p (SrcCode (ExPair e1 e2)) = showParen (p > 0) $
+        showsPrec 1 (SrcCode e1) . showString " , " . showsPrec 0 (SrcCode e2)
+    showsPrec p (SrcCode (ExLam v e)) = showParen (p > 1) $
+        showString "\\ " . shows (SrcCode v) . showString " . " . showsPrec 1 (SrcCode e)
+    showsPrec p (SrcCode (ExLiftAppB e1 e2)) = showParen (p > 2) $
+        showsPrec 2 (SrcCode e1) . showString " <*> " . showsPrec 3 (SrcCode e2)
+    showsPrec p (SrcCode (ExLiftAppE e1 e2)) = showParen (p > 2) $
+        showsPrec 2 (SrcCode e1) . showString " <.> " . showsPrec 3 (SrcCode e2)
+    showsPrec p (SrcCode (ExApp e1 e2)) = showParen (p > 3) $
+        showsPrec 3 (SrcCode e1) . showChar ' ' . showsPrec 4 (SrcCode e2)
+    showsPrec p (SrcCode (ExConst e)) = showParen (p > 3) $
+        showString "const " . showsPrec 4 (SrcCode e)
+    showsPrec p (SrcCode (ExBehav f)) = showParen (p > 3) $
+        showString "behavior " . showsPrec 4 (SrcCode f)
+    showsPrec p (SrcCode (ExEvent t e)) = showParen (p > 3) $
+        showString "event " . showsPrec 4 (SrcCode t) . showChar ' ' . showsPrec 4 (SrcCode e)
+    showsPrec p (SrcCode (ExFold t f)) = showParen (p > 3) $
+        showString "fold [" . shows (SrcCode t) . showString "] " . showsPrec 4 (SrcCode f)
+    showsPrec p (SrcCode (ExUnfold t f)) = showParen (p > 3) $
+        showString "unfold [" . shows (SrcCode t) . showString "] " . showsPrec 4 (SrcCode f)
+    showsPrec _ (SrcCode (ExVar v)) = shows (SrcCode v)
+    showsPrec _ (SrcCode (ExNatLit i)) = shows i
+    showsPrec _ (SrcCode ExNull) = showChar '?'
+    showsPrec _ (SrcCode ExUnit) = showString "()"
+    showsPrec _ (SrcCode ExLeft) = showString "left"
+    showsPrec _ (SrcCode ExRight) = showString "right"
+    showsPrec _ (SrcCode ExCase) = showString "case"
+    showsPrec _ (SrcCode ExFst) = showString "first"
+    showsPrec _ (SrcCode ExSnd) = showString "second"
+    showsPrec _ (SrcCode ExExpand) = showString "expand"
+    showsPrec _ (SrcCode ExNever) = showString "never"
+    showsPrec _ (SrcCode ExRace) = showString "race"
+    showsPrec _ (SrcCode ExReflect) = showString "reflect"
+    showsPrec _ (SrcCode ExUSwitch) = showString "ultraswitch"
+    showsPrec _ (SrcCode (ExPack t)) = showString "pack [" . shows (SrcCode t) . showChar ']'
+    showsPrec _ (SrcCode (ExUnpack t)) = showString "unpack [" . shows (SrcCode t) . showChar ']'
+    showsPrec _ (SrcCode ExUJump) = showString "ultrajump"
+
+instance Show (SrcCode Type) where
+    showsPrec p (SrcCode (TyMu mu)) = showParen (p > 0) $ shows (SrcCode mu)
+    showsPrec p (SrcCode (TyNu nu)) = showParen (p > 0) $ shows (SrcCode nu)
+    showsPrec p (SrcCode (TyFun t1 t2)) = showParen (p > 1) $
+        showsPrec 2 (SrcCode t1) . showString " -> " . showsPrec 1 (SrcCode t2)
+    showsPrec p (SrcCode (TyPlus t1 t2)) = showParen (p > 2) $
+        showsPrec 3 (SrcCode t1) . showString " + " . showsPrec 2 (SrcCode t2)
+    showsPrec p (SrcCode (TyPair t1 t2)) = showParen (p > 3) $
+        showsPrec 4 (SrcCode t1) . showString " * " . showsPrec 3 (SrcCode t2)
+    showsPrec p (SrcCode (TyApp v [])) = shows (SrcCode v)
+    showsPrec p (SrcCode (TyApp v vs)) = showParen (p > 4) $
+        foldl (\f t -> f . showChar ' ' . (showsPrec 5 . SrcCode $ t)) (shows . SrcCode $ v) vs
+    showsPrec p (SrcCode (TyBehav t)) = showParen (p > 4) $
+        showString "behavior " . showsPrec 5 (SrcCode t)
+    showsPrec p (SrcCode (TyEvent t)) = showParen (p > 4) $
+        showString "event " . showsPrec 5 (SrcCode t)
+    showsPrec _ (SrcCode TyNat) = showString "positive"
+    showsPrec _ (SrcCode TyZero) = showChar '0'
+    showsPrec _ (SrcCode TyUnit) = showChar '1'
+    showsPrec _ (SrcCode (TyVar i)) = showChar '_' . showShortVar ['a'..'z'] 'v' i
+    showsPrec _ (SrcCode (TyCon i)) = showChar '_' . showShortVar ['A'..'Z'] 'T' i
+
+showShortVar :: [Char] -> Char -> Integer -> ShowS
+showShortVar ls c i = if i<26 then showChar $ ls !! (fromInteger i)
+                                  else showChar c . shows (i-26)
+
+instance Show (SrcCode MuType) where
+    showsPrec _ (SrcCode (MuType x t)) =
+        showString "mu " . shows (SrcCode x) . showString " . " . showsPrec 1 (SrcCode t)
+
+
+instance Show (SrcCode NuType) where
+    showsPrec _ (SrcCode (NuType x t)) =
+        showString "nu " . shows (SrcCode x) . showString " . " . showsPrec 1 (SrcCode t)
+
+
+instance Show (SrcCode Var) where
+    showsPrec _ (SrcCode (Var s)) = showString s
diff --git a/Tempus/TypeCheck.hs b/Tempus/TypeCheck.hs
new file mode 100644
--- /dev/null
+++ b/Tempus/TypeCheck.hs
@@ -0,0 +1,468 @@
+-- | Semantical analysis (i.e. type check and variances test) for Tempus expressions.
+module Tempus.TypeCheck (
+    TypeEnv,
+    TypeSynEnv,
+    ContextError (..),
+
+    checkProgram,
+    getType,
+    substVar,
+    expandTypeSyn,
+    expandMuType,
+    expandNuType,
+
+    Variance (..),
+    invertVariance
+) where
+
+
+import Control.Applicative
+import Control.Arrow
+import Control.Monad.Error
+import Control.Monad.State
+
+import Data.Generics.Uniplate.Operations
+import Data.Function
+import Data.List
+import Data.Maybe
+
+import Tempus.Loc
+import Tempus.Syntax
+
+
+-- | Type check monad.
+type T a = ErrorT ContextError (State TState) a
+
+-- | A general context check error.
+data ContextError = UndefinedVariable Var    -- ^ Undefined global variable
+                  | DuplicateVariable Var    -- ^ Variable defined twice
+                  | DuplicateType Var        -- ^ Type defined twice
+                  | OccursCheck Type Type    -- ^ Occurs check failed when trying to unify the types
+                  | SymbolClash Type Type    -- ^ The types cannot be unified due to different
+                                             -- outer-most constructors
+                  | IncorrectVariances Type  -- ^ Incorrect variances
+                  | UndefinedType Var        -- ^ Undefined type synonym or free type variable used
+                  | TypeArgsMismatch Var     -- ^ Wrong number of arguments for the type synonym
+                  | NoMuType Type            -- ^ Type has to be a mu type but isn't
+                  | NoNuType Type            -- ^ Type has to be a nu type but isn't
+                  | NoRecType Type           -- ^ Type has to be a recursive type but isn't
+                  deriving (Show)
+
+
+instance Error ContextError where
+    noMsg      = error "noMsg not implemented for Error ContextError"
+    strMsg msg = error "strMsg not implemented for Error ContextError"
+
+instance Error e => Error (Loc e) where
+    noMsg      = error "noMsg not implemented for Error (Loc e)"
+    strMsg msg = error "stdMsg not implemented for Error (Loc e)"
+
+
+-- | Type check state.
+data TState = TState {
+                  -- | The ID to use for the next fresh type variable.
+                  varID :: Integer,
+                  -- | The ID to use for the next fresh type constructor variable.
+                  conID :: Integer
+              } deriving (Eq, Show)
+
+
+-- | Initial type check state.
+initTState :: TState
+initTState = TState { varID = 0, conID = 0 }
+
+
+{- |
+    Performs a semantical analysis for a module using the given global variables with types and
+    type synonyms. Either a context error with source location or lists with the global variables
+    and their inferred types and type synonyms is returned.
+-}
+checkProgram :: TypeEnv -> TypeSynEnv -> Program
+             -> Either (Loc ContextError) (TypeEnv, TypeSynEnv)
+checkProgram tEnv sEnv prog =
+    fst $ runState (runErrorT $ checkDecls tEnv [] sEnv [] prog) initTState
+
+-- | Helper function for 'checkProgram'.
+checkDecls :: TypeEnv -> TypeEnv -> TypeSynEnv -> TypeSynEnv -> [Decl]
+           -> ErrorT (Loc ContextError) (State TState) (TypeEnv, TypeSynEnv)
+checkDecls _    tEnv' _    sEnv'[] = return (reverse tEnv', reverse sEnv')
+checkDecls tEnv tEnv' sEnv sEnv' (DeclType loc v vs t : ds) = do
+    when (not . null $ filter ((== v) . fst) $ sEnv ++ sEnv') $
+        throwError $ Loc loc $ DuplicateType v
+    checkDecls tEnv tEnv' sEnv ((v, (vs, t)) : sEnv') ds
+checkDecls tEnv tEnv' sEnv sEnv' (DeclVal loc v e : ds) = do
+    let env      = tEnv ++ tEnv'
+        builtIns = map (\v -> (Var v, undefined)) ["add", "mult"]
+    when (not . null $ filter ((== v) . fst) (env ++ builtIns)) $
+        throwError $ Loc loc $ DuplicateVariable v
+    t <- addErrorLoc loc $ checkedTypeExpr env (sEnv ++ sEnv') e
+    checkDecls tEnv ((v, generalize t) : tEnv') sEnv sEnv' ds
+
+
+-- | Infer the most general type for an expression using the types from a list of global variables
+-- and a list of type synonyms.
+getType :: TypeEnv -> TypeSynEnv -> Loc Expr -> Either (Loc ContextError) Type
+getType tEnv sEnv (Loc loc e) =
+    fst $ runState (runErrorT $ addErrorLoc loc $ checkedTypeExpr tEnv sEnv e) initTState
+
+
+-- TODO: Remove type schemes?
+-- | Type schemes.
+type TypeScheme = ([Integer], Type)
+
+-- | A type environment as a list of variables with their types.
+type TypeEnv = [(Var, TypeScheme)]
+
+-- | A substitution as a list of pairs of type variable IDs and the types of the corresponding
+-- type variables.
+type Subst = [(Integer, Type)]
+
+-- | A type synonym environment as a list of pairs of a type synonym name with its parameter
+-- names and type.
+type TypeSynEnv = [(Var, ([Var], Type))]
+
+
+-- | Transforms an error monad by adding a location information to the error type.
+addErrorLoc :: (Error e, Functor m) => SrcLoc -> ErrorT e m a -> ErrorT (Loc e) m a
+addErrorLoc loc = mapErrorT (fmap . left $ Loc loc)
+
+
+-- | Perform a type inference with variance test within the @T@ monad for an expression, using the
+-- given global variables with types and type synonyms.
+checkedTypeExpr :: TypeEnv -> TypeSynEnv -> Expr -> T Type
+checkedTypeExpr tEnv sEnv e = do
+    t <- snd <$> typeExpr tEnv [] sEnv e
+    var <- correctVariances sEnv t
+    when (not $ var) $
+        throwError $ IncorrectVariances t
+    return t
+
+-- | Performs a type inference for an expression. Returns the inferred type with a substitution
+-- for the used type variables.
+typeExpr :: TypeEnv     -- ^ Global type environment
+         -> TypeEnv     -- ^ Local type environment
+         -> TypeSynEnv  -- ^ Type synonym environment
+         -> Expr        -- ^ Expression
+         -> T (Subst, Type)
+typeExpr gamma lambda sEnv e =
+    case e of
+        -- TODO: Put somewhere else
+        ExVar (Var v)
+            | v `elem` ["add", "mult"]
+                -> return ([], TyFun TyNat $ TyFun TyNat TyNat)
+        ExVar v -> case lookup v (lambda ++ gamma) of
+                       Just s  -> (\t -> ([], t)) <$> instantiate s
+                       Nothing -> throwError $ UndefinedVariable v
+        ExLam x e -> do
+            b <- freshVar
+            (s, t) <- typeExpr (deleteBy ((==) `on` fst) (x, undefined) gamma)
+                               (replVar (x, b) lambda) sEnv e
+            return (s, TyFun (substType s b) t)
+        ExApp e1 e2 -> do
+            b <- freshVar
+            (s1, t1) <- typeExpr gamma lambda sEnv e1
+            (s2, t2) <- typeExpr gamma (substEnv s1 lambda) sEnv e2
+            s3 <- mgu sEnv (substType s2 t1) (TyFun t2 b) []
+            return (compSubst s3 $ compSubst s2 s1, substType s3 b)
+        ExPair e1 e2 -> do
+            (s1, t1) <- typeExpr gamma lambda sEnv e1
+            (s2, t2) <- typeExpr gamma (substEnv s1 lambda) sEnv e2
+            return (compSubst s2 s1, TyPair (substType s2 t1) t2)
+{-
+        ExLiftApp e1 e2 -> do
+            (s1, t1) <- typeExpr gamma lambda e1
+            [c, d] <- replicateM 2 freshVar
+            s2 <- mgu (TyBehav $ TyFun c d) t1 []
+            (s3, t2) <- typeExpr gamma (substEnv (compSubst s2 s1) lambda) e2
+            s4 <- mgu (substType (compSubst s2 s1) $ TyBehav c) t2 []
+            return (compSubst s4 $ compSubst s3 $ compSubst s2 s1, substType s4 $ TyBehav d)
+-}
+        -- TODO: rewrite
+        ExLiftAppB e1 e2 -> do
+            (s2', t1) <- typeExpr gamma lambda sEnv e1
+            [a, b, c, d] <- replicateM 4 freshVar
+            s3' <- mgu sEnv (TyFun (TyBehav $ TyFun c d)
+                                   (TyFun (TyBehav c) (TyBehav d))) (TyFun t1 a) []
+            (s2, t2) <- typeExpr gamma (substEnv (compSubst s3' s2') lambda) sEnv e2
+            s3 <- mgu sEnv (substType (compSubst s2 s3') a) (TyFun t2 b) []
+            return (compSubst s3 $ compSubst s2 $ compSubst s3' s2', substType s3 b)
+        -- TODO: rewrite
+        ExLiftAppE e1 e2 -> do
+            (s2', t1) <- typeExpr gamma lambda sEnv e1
+            [a, b, c, d] <- replicateM 4 freshVar
+            s3' <- mgu sEnv (TyFun (TyBehav $ TyFun c d)
+                                   (TyFun (TyEvent c) (TyEvent d))) (TyFun t1 a) []
+            (s2, t2) <- typeExpr gamma (substEnv (compSubst s3' s2') lambda) sEnv e2
+            s3 <- mgu sEnv (substType (compSubst s2 s3') a) (TyFun t2 b) []
+            return (compSubst s3 $ compSubst s2 $ compSubst s3' s2', substType s3 b)
+        ExConst e -> do
+            (_, t) <- typeExpr gamma [] sEnv e
+            return ([], TyBehav t)
+        ExBehav f -> do
+            (_, t) <- typeExpr gamma [] sEnv f
+            a <- freshVar
+            s <- mgu sEnv (TyFun TyNat a) t []
+            return (s, substType s (TyBehav a))
+        ExEvent t e -> do
+            (s1, t1) <- typeExpr gamma lambda sEnv t
+            s2 <- mgu sEnv TyNat t1 []
+            (_, t2) <- typeExpr gamma [] sEnv e
+            return (compSubst s2 s1, TyEvent t2)
+        ExFold t f -> do
+            mu@(MuType a t1) <- either throwError return $ expandMuType sEnv t
+            (_, t2) <- typeExpr gamma [] sEnv f
+            b <- freshVar
+            s <- mgu sEnv (TyFun (substVar a b t1) b) t2 []
+            return (s, substType s $ TyFun (TyMu mu) b)
+        ExUnfold t f -> do
+            nu@(NuType a t1) <- either throwError return $ expandNuType sEnv t
+            (_, t2) <- typeExpr gamma [] sEnv f
+            b <- freshVar
+            s <- mgu sEnv (TyFun b (substVar a b t1)) t2 []
+            return (s, substType s $ TyFun b (TyNu nu))
+        -- TODO: throw returned error, not NoRecType
+        ExPack t -> case (expandMuType sEnv t, expandNuType sEnv t) of
+            (Right s@(MuType x t), Left _) -> return ([], TyFun (substVar x (TyMu s) t) (TyMu s))
+            (Left _, Right s@(NuType x t)) -> return ([], TyFun (substVar x (TyNu s) t) (TyNu s))
+            (Left _, Left _)               -> throwError $ NoRecType t
+        ExUnpack t -> case (expandMuType sEnv t, expandNuType sEnv t) of
+            (Right s@(MuType x t), Left _) -> return ([], TyFun (TyMu s) (substVar x (TyMu s) t))
+            (Left _, Right s@(NuType x t)) -> return ([], TyFun (TyNu s) (substVar x (TyNu s) t))
+            (Left _, Left _)               -> throwError $ NoRecType t
+        _ -> (\t -> ([], t)) <$> typeSimple e
+
+
+-- | Looks up a variable name in the type synonym list and applies the type synonym to the list of
+-- argument types. Either a context error or the expanded type is returned.
+expandTypeSyn :: TypeSynEnv -> Var -> [Type] -> Either ContextError Type
+expandTypeSyn env v ts = case lookup v env of
+    Nothing -> Left $ UndefinedType v
+    Just (vs, t)
+        | length vs == length ts -> Right $ foldr (uncurry substVar) t $ zip vs ts
+        | otherwise -> Left $ TypeArgsMismatch v
+
+-- | Tries to expand a type to a mu type. If the resulting type isn't a mu type, an error is
+-- returned, otherwise, the mu type is returned.
+expandMuType :: TypeSynEnv -> Type -> Either ContextError MuType
+expandMuType sEnv (TyMu mu)    = Right mu
+expandMuType sEnv (TyApp v ts) = expandTypeSyn sEnv v ts >>= expandMuType sEnv
+expandMuType sEnv t            = Left $ NoMuType t
+
+-- | Tries to expand a type to a nu type. If the resulting type isn't a nu type, an error is
+-- returned, otherwise, the nu type is returned.
+expandNuType :: TypeSynEnv -> Type -> Either ContextError NuType
+expandNuType sEnv (TyNu nu)    = Right nu
+expandNuType sEnv (TyApp v ts) = expandTypeSyn sEnv v ts >>= expandNuType sEnv
+expandNuType sEnv t            = Left $ NoNuType t
+
+-- | Instantiates a type scheme to a type.
+instantiate :: TypeScheme -> T Type
+instantiate (vs, t) = do
+    bs <- replicateM (length vs) freshVar
+    return $ substType (zip vs bs) t
+
+-- TODO: condense type vars
+-- | Generalizes a type to a type scheme.
+generalize :: Type -> TypeScheme
+generalize t = (ftv t, t)
+
+-- | Returns the free type variables of a type as a list of type variable IDs.
+ftv :: Type -> [Integer]
+ftv = nub . ftv'
+    where
+        ftv' (TyVar i) = [i]
+        ftv' t         = concatMap ftv' $ children t
+
+
+-- | Compose two substitutions to a new one.
+compSubst :: Subst -> Subst -> Subst
+compSubst sigma theta = let theta' = map (second $ substType sigma) theta
+                            sigma' = let domTheta = map fst theta
+                                     in [ (x,t) | (x,t) <- sigma, x `notElem` domTheta ]
+                            theta'' = [ (x,t) | (x,t) <- theta', t /= TyVar x ]
+                        in nub $ theta'' ++ sigma'
+
+{-
+-- defined in Baader
+compSubst :: Subst' -> Subst' -> Subst'
+compSubst sigma theta = let sigma' = map (second $ substType theta) sigma
+                            theta' = let domSigma = map fst sigma
+                                     in [ (x,t) | (x,t) <- theta, x `notElem` domSigma ]
+                            sigma'' = [ (x,t) | (x,t) <- sigma', t /= TyVar x ]
+                        in nub $ sigma'' ++ theta'
+-}
+
+-- | Apply a substitution to each type in the type environment.
+substEnv :: Subst -> TypeEnv -> TypeEnv
+substEnv s = map (second $ second $ substType s)
+
+-- | Apply a substitution to a type.
+substType :: Subst -> Type -> Type
+substType s t = transform f t
+    where
+        f (TyVar i) = fromMaybe (TyVar i) $ lookup i s
+        f t = t
+
+-- | Add, or replace if already present, a variable with a type in a list of variables with types.
+replVar :: (Var, Type) -> TypeEnv -> TypeEnv
+replVar (v,t) = ((v, ([], t)):) . filter ((/= v) . fst)
+
+
+-- version Baader, Unification Theory; see also Heeren, Top Quality Type Error Messages
+-- | Try to unify two types using a type synonym list and an initial substitution.
+mgu :: TypeSynEnv -> Type -> Type -> Subst -> T Subst
+mgu sEnv t1 t2 s =
+    case (condSubst t1, condSubst t2) of
+        (TyVar x, TyVar y)
+            | x == y -> return []
+        (TyVar x, t)
+            | x `occursIn` t -> throwError $ OccursCheck (TyVar x) t
+            | otherwise      -> return $ compSubst [(x, t)] s
+        (t1, t2@(TyVar _)) -> mgu sEnv t2 t1 s
+        (TyMu (MuType x1 t1), TyMu (MuType x2 t2)) -> do
+            c <- freshCon
+            mgu sEnv (substVar x1 c t1) (substVar x2 c t2) []
+        (TyNu (NuType x1 t1), TyNu (NuType x2 t2)) -> do
+            c <- freshCon
+            mgu sEnv (substVar x1 c t1) (substVar x2 c t2) []
+        (TyApp v ts, t) -> either throwError (\t' -> mgu sEnv t' t s) $ expandTypeSyn sEnv v ts
+        (t, TyApp v ts) -> either throwError (\t' -> mgu sEnv t t' s) $ expandTypeSyn sEnv v ts
+        (t1, t2)
+            | equalSymbols t1 t2 -> unifySubterms (children t1) (children t2) s
+            | otherwise -> throwError $ SymbolClash t1 t2
+    where
+        condSubst t@(TyVar _) = substType s t
+        condSubst t           = t
+
+        equalSymbols t1 t2 = case (t1, t2) of
+            (TyFun _ _, TyFun _ _)   -> True
+            (TyPlus _ _, TyPlus _ _) -> True
+            (TyPair _ _, TyPair _ _) -> True
+            (TyBehav _, TyBehav _)   -> True
+            (TyEvent _, TyEvent _)   -> True
+            (TyNat, TyNat)           -> True
+            (TyZero, TyZero)         -> True
+            (TyUnit, TyUnit)         -> True
+            (TyCon x, TyCon y)       -> x == y
+            _                        -> False
+
+        -- TODO: use foldM
+        unifySubterms [] [] sigma = return sigma
+        unifySubterms (s:ss) (t:ts) sigma = do
+            sigma' <- mgu sEnv s t sigma
+            unifySubterms ss ts $ compSubst sigma sigma'
+        unifySubterms _ _ _ = error "unifySubterms: same symbols with different arities"
+
+-- | Check if a type variable with the given ID occurs in the type.
+occursIn :: Integer -> Type -> Bool
+occursIn x t = x `elem` [ y | TyVar y <- universe t]
+
+-- | @substVar v s t@ replaces all occurrences of @v@ in @t@ by @s@. @v@ is not replaced if it is
+-- bound locally by a mu type.
+substVar :: Var -> Type -> Type -> Type
+substVar x s t@(TyMu (MuType y t'))
+    | x == y    = t
+    | otherwise = TyMu (MuType y $ substVar x s t')
+substVar x s t@(TyNu (NuType y t'))
+    | x == y    = t
+    | otherwise = TyNu (NuType y $ substVar x s t')
+substVar x s t@(TyApp y [])
+    | x == y    = s
+    | otherwise = t
+substVar x s t = descend (substVar x s) t
+
+-- | Returns the type of a Tempus primitive expression.
+typeSimple :: Expr -> T Type
+typeSimple e =
+    case e of
+        ExNatLit _ -> return $ TyNat
+        ExNull  -> TyFun TyZero <$> freshVar
+        ExUnit  -> return $ TyUnit
+        ExLeft  -> fresh2 $ \t1 t2 -> TyFun t1 (TyPlus t1 t2)
+        ExRight -> fresh2 $ \t1 t2 -> TyFun t2 (TyPlus t1 t2)
+        ExCase  -> fresh3 $ \t1 t2 s -> TyFun (TyFun t1 s) $
+                                            TyFun (TyFun t2 s) $ TyFun (TyPlus t1 t2) s
+        ExFst   -> fresh2 $ \t1 t2 -> TyFun (TyPair t1 t2) t1
+        ExSnd   -> fresh2 $ \t1 t2 -> TyFun (TyPair t1 t2) t2
+        ExExpand -> fresh1 $ \t -> TyFun (TyBehav t) (TyBehav $ TyPair t (TyBehav t))
+        ExNever -> return $ TyEvent TyZero
+        ExRace  -> fresh2 $ \t1 t2 -> TyFun (TyEvent t1) $
+                                          TyFun (TyEvent t2) $
+                                              TyEvent $ TyPlus (TyPair t1 t2) $
+                                                        TyPlus (TyPair t1 $ TyEvent t2)
+                                                               (TyPair t2 $ TyEvent t1)
+        -- TODO: Replace n, s by new var
+        ExReflect -> return $ TyFun TyNat $ TyMu $
+                                  MuType (Var "n") (TyPlus TyUnit (TyApp (Var "n") []))
+        ExUJump   -> fresh1 $ \t -> TyFun (TyNu $ NuType (Var "s") $ TyEvent $
+                                               TyPlus t (TyApp (Var "s") []))
+                                          (TyEvent t)
+        ExUSwitch  -> fresh1 $ \t -> TyFun (TyNu $ NuType (Var "s") $
+                                               TyPair (TyBehav t) $ TyEvent $ TyPair t $
+                                                   TyApp (Var "s") [])
+                                           (TyBehav t)
+        _ -> error "typeSimple: expression is not simple"
+
+-- | Generate a new unused type variable as a type expression.
+freshVar :: T Type
+freshVar = do
+    i <- gets varID
+    modify (\st -> st { varID = varID st + 1 })
+    return $ TyVar i
+
+-- | Generate a new unused type variable as a type expression and apply the given function to that
+-- type.
+fresh1 :: (Type -> Type) -> T Type
+fresh1 f = liftM f freshVar
+
+-- | Like 'fresh1' but for two variables.
+fresh2 :: (Type -> Type -> Type) -> T Type
+fresh2 f = liftM2 f freshVar freshVar
+
+-- | Like 'fresh1' but for three variables.
+fresh3 :: (Type -> Type -> Type -> Type) -> T Type
+fresh3 f = liftM3 f freshVar freshVar freshVar
+
+-- | Generate a new unused type constructor variable as a type expression.
+freshCon :: T Type
+freshCon = do
+    i <- gets conID
+    modify (\st -> st { conID = conID st + 1 })
+    return $ TyCon i
+
+
+-- | A variance.
+data Variance = CoVariant | ContraVariant deriving (Eq, Show)
+
+-- | Inverts a variance.
+invertVariance :: Variance -> Variance
+invertVariance CoVariant     = ContraVariant
+invertVariance ContraVariant = CoVariant
+
+-- TODO: Distinguish between bound variables with wrong variances and unbound variables
+-- | Perform a variances check for the type using a type synonym environment, and return @true@
+-- iff the test was successful.
+correctVariances :: TypeSynEnv -> Type -> T Bool
+correctVariances = var []
+    where
+        var delta sEnv (TyApp x ts)
+            | (x, CoVariant) `elem` delta     = return True
+            | (x, ContraVariant) `elem` delta = return False
+            | otherwise                       = either throwError (var delta sEnv) $
+                                                    expandTypeSyn sEnv x ts
+        var delta _    (TyVar x)           = return True
+        var _     _    TyNat               = return True
+        var _     _    TyZero              = return True
+        var _     _    TyUnit              = return True
+        var delta sEnv (TyBehav t)         = var delta sEnv t
+        var delta sEnv (TyEvent t)         = var delta sEnv t
+        var delta sEnv (TyPair t1 t2)      = liftM2 (&&) (var delta sEnv t1) (var delta sEnv t2)
+        var delta sEnv (TyPlus t1 t2)      = liftM2 (&&) (var delta sEnv t1) (var delta sEnv t2)
+        var delta sEnv (TyFun t1 t2)       = liftM2 (&&)
+                                                 (var (map (second invertVariance) delta) sEnv t1)
+                                                 (var delta sEnv t2)
+        var delta sEnv (TyMu (MuType v t)) = var (replVar (v, CoVariant) delta) sEnv t
+        var delta sEnv (TyNu (NuType v t)) = var (replVar (v, CoVariant) delta) sEnv t
+
+        replVar :: (Var, Variance) -> [(Var, Variance)] -> [(Var, Variance)]
+        replVar (v,t) = ((v, t):) . filter ((/= v) . fst)
diff --git a/tempus.cabal b/tempus.cabal
new file mode 100644
--- /dev/null
+++ b/tempus.cabal
@@ -0,0 +1,50 @@
+Name:          tempus
+Version:       0.1.0
+Cabal-Version: >= 1.6
+Build-Type:    Simple
+License:       BSD3
+License-File:  LICENSE
+Copyright:     (C) 2010, Matthias Reisner
+Author:        Matthias Reisner
+Maintainer:    Matthias Reisner <matthias.reisner@googlemail.com>
+Stability:     experimental
+Synopsis:      Interpreter for the FRP language Tempus
+Description:   This package provides an interactive console application for loading of modules,
+               definition of types and values, as well as type checking and evaluation of
+               expressions in the functional reactive language Tempus.
+Category:      FRP, Language, Compilers/Interpreters
+Tested-With:   GHC == 6.10.4, GHC == 6.12.1
+
+Data-Files:          Prelude.tp
+Extra-Source-Files:  Tempus/Examples/lightbulb.tp
+
+Flag base4
+    Description: base >= 4.0
+    Default: True
+
+Executable tempus
+    Build-Tools:        happy >= 1.18
+
+    if flag(base4)
+        Build-Depends:  base              >= 4       && < 5
+    else
+        Build-Depends:  base              >= 3.0.3   && < 4
+    Build-Depends:      mtl               >= 1.1.0.2 && < 1.2,
+                        uniplate          >= 1.5.1,
+                        array             >= 0.2     && < 3,
+                        utf8-string       >= 0.3.6,
+                        filepath          >= 1.1.0.2,
+                        directory         >= 1.0.0.3,
+                        haskeline         >= 0.6.3.2,
+                        executable-path   >= 0.0.2
+    Extensions:         DeriveDataTypeable,
+                        FlexibleInstances
+
+    Main-Is:            Tempus/Main.hs
+    Other-Modules:      Tempus.Loc,
+                        Tempus.Lexer,
+                        Tempus.Syntax,
+                        Tempus.Parser,
+                        Tempus.TypeCheck,
+                        Tempus.Evaluation,
+                        Tempus.Interpreter