diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -10,4 +10,5 @@
 and simply typed λ-calculus.
 
  * [Mikrokosmos user's guide](https://m42.github.io/mikrokosmos/).
+ * [Mikrokosmos tutorial](https://github.com/M42/mikrokosmos/blob/master/docs/tutorial.ipynb).
  * [Mikrokosmos on Hackage](https://hackage.haskell.org/package/mikrokosmos).
diff --git a/mikrokosmos.cabal b/mikrokosmos.cabal
--- a/mikrokosmos.cabal
+++ b/mikrokosmos.cabal
@@ -1,5 +1,5 @@
 name:                mikrokosmos
-version:             0.5.0
+version:             0.6.0
 synopsis:            Lambda calculus interpreter
 description:         A didactic untyped lambda calculus interpreter.
 homepage:            https://github.com/M42/mikrokosmos
@@ -35,6 +35,7 @@
                        options,
                        tasty,
                        tasty-hunit,
+                       tasty-quickcheck,
                        directory >= 1.0
                        
   other-modules:       Format
@@ -48,3 +49,35 @@
                        
   default-language:    Haskell2010
   ghc-options:         -Wall
+
+
+test-suite test
+  default-language:
+    Haskell2010
+  type:
+    exitcode-stdio-1.0
+  hs-source-dirs: tests
+                  source
+  main-is:
+    test.hs
+  build-depends: base >=4.7 && <5,
+                 mtl >=2.2,
+                 containers >= 0.5,
+                 haskeline >=0.7,
+                 parsec >=3,
+                 ansi-terminal,
+                 multimap,
+                 HUnit >=1.0,
+                 options,
+                 tasty,
+                 tasty-hunit,
+                 tasty-quickcheck,
+                 directory >= 1.0
+  other-modules: Format
+                 Lambda
+                 NamedLambda
+                 MultiBimap
+                 Interpreter
+                 Environment
+                 Ski
+                 Types
diff --git a/source/Environment.hs b/source/Environment.hs
--- a/source/Environment.hs
+++ b/source/Environment.hs
@@ -12,6 +12,7 @@
     Environment
   , context
   , defaultEnv
+  , emptyContext
 
   -- * Reading the environment
   , getVerbose
@@ -19,6 +20,7 @@
   , getSki
   , getTypes
   , getExpressionName
+  , getTopo
   
   -- * Modifying the environment
   , addBind
@@ -26,6 +28,7 @@
   , changeVerbose
   , changeSkioutput
   , changeTypes
+  , changeTopo
 
   -- * Filenames and Modulenames
   , Filename
@@ -52,6 +55,7 @@
   , color :: Bool
   , skioutput :: Bool
   , types :: Bool
+  , topo :: Bool
   }
 
 -- | Default environment for the interpreter.
@@ -63,14 +67,16 @@
   , color       = True
   , skioutput   = False
   , types       = False
+  , topo        = False
   }
 
 -- | Get current settings
-getColor, getVerbose, getSki, getTypes :: Environment -> Bool
+getColor, getVerbose, getSki, getTypes, getTopo :: Environment -> Bool
 getColor   = color
 getVerbose = verbose
 getSki     = skioutput
 getTypes   = types
+getTopo    = topo
 
 
 
@@ -78,7 +84,7 @@
 addBind :: Environment -> String -> Exp -> Environment
 addBind env s e =
   -- If the binding already exists, it changes nothing
-  if elem s (MultiBimap.lookup e $ context env)
+  if s `elem` MultiBimap.lookup e (context env)
     then env
     else env {context = MultiBimap.insert e s (context env)}
 
@@ -97,7 +103,8 @@
 -- | Sets the types output configuration on/off
 changeTypes :: Environment -> Bool -> Environment
 changeTypes options setting = options {types = setting}
-
+changeTopo :: Environment -> Bool -> Environment
+changeTopo options setting = options {topo = setting}
 
 -- | Given an expression, returns its name if it is bounded to any.
 getExpressionName :: Environment -> Exp -> Maybe String
diff --git a/source/Format.hs b/source/Format.hs
--- a/source/Format.hs
+++ b/source/Format.hs
@@ -27,6 +27,11 @@
   , helpText
   , initialText
   , versionText
+  , restartText
+  , errorNonTypeableText
+  , errorTypeConstructors
+  , errorUndefinedText
+  , errorUnknownCommand
   )
 where
 
@@ -34,61 +39,28 @@
 import Data.List
 import Data.Monoid
 
--- Colors
--- | Prompt messages color
-promptColor :: Color
+-- | Colors used on the prompt.
+promptColor, nameColor, substColor, subst2Color, typeColor, errorColor :: Color
 promptColor = Blue
-
--- | Named variables color
-nameColor :: Color
 nameColor = Green
-
--- | Substitutions are marked with this color
-substColor :: Color
 substColor = Cyan
-
--- | To-be-substituted expressions are marked with this color
-subst2Color :: Color
 subst2Color = Cyan
-
--- | Types are marked with this color
-typeColor :: Color
 typeColor = Yellow
+errorColor = Red
 
 -- Format sequences
 -- | Sequence of characters that signals the format of a formula to the terminal.
-formatFormula :: String
+formatFormula, formatIntro, formatLoading, formatPrompt, formatName  :: String
+formatSubs1, formatSubs2, formatType, formatError :: String
 formatFormula = setSGRCode [SetConsoleIntensity NormalIntensity, SetColor Foreground Dull promptColor]
-
--- | Sequence of characters that signals the format of the introduction to the terminal.
-formatIntro :: String
-formatIntro = setSGRCode [SetConsoleIntensity BoldIntensity, SetColor Foreground Dull promptColor]
-
--- | Sequence of characters that signals the format of the loading of a module to the terminal.
-formatLoading :: String
+formatIntro   = setSGRCode [SetConsoleIntensity BoldIntensity, SetColor Foreground Dull promptColor]
 formatLoading = formatIntro
-
--- | Sequence of characters that signals the format of the prompt to the terminal.
-formatPrompt :: String
-formatPrompt = setSGRCode [SetConsoleIntensity BoldIntensity, SetColor Foreground Vivid promptColor]
-
--- | Sequence of characters that signals the format of a name to the terminal.
-formatName :: String
-formatName = setSGRCode [SetColor Foreground Dull nameColor]
-
--- | Sequence of characters that signals the format of a substitution to the terminal.
-formatSubs1 :: String
-formatSubs1 = setSGRCode [SetConsoleIntensity BoldIntensity, SetColor Foreground Dull substColor]
-
--- | Sequence of characters that signals the format of a expression which will
---   be substituted in the next reduction step to the terminal.
-formatSubs2 :: String
-formatSubs2 = setSGRCode [SetConsoleIntensity FaintIntensity, SetColor Foreground Dull subst2Color]
-
--- | Sequence of characters that signals the format of a type to the terminal.
-formatType :: String
-formatType = setSGRCode [SetConsoleIntensity NormalIntensity, SetColor Foreground Dull typeColor]
-
+formatPrompt  = setSGRCode [SetConsoleIntensity BoldIntensity, SetColor Foreground Vivid promptColor]
+formatName    = setSGRCode [SetColor Foreground Dull nameColor]
+formatSubs1   = setSGRCode [SetConsoleIntensity BoldIntensity, SetColor Foreground Dull substColor]
+formatSubs2   = setSGRCode [SetConsoleIntensity FaintIntensity, SetColor Foreground Dull subst2Color]
+formatType    = setSGRCode [SetConsoleIntensity NormalIntensity, SetColor Foreground Dull typeColor]
+formatError   = setSGRCode [SetConsoleIntensity NormalIntensity, SetColor Foreground Dull errorColor]
 
 -- | Sequence of characters that cleans all the format.
 end :: String
@@ -117,7 +89,38 @@
   ]
 
 
+-- | Unknown command error message
+errorUnknownCommand :: String
+errorUnknownCommand =
+  formatError ++
+  "Error: parse error, unknown command"
+  ++ end
 
+
+-- | Non typeable expression error message.
+errorNonTypeableText :: String
+errorNonTypeableText =
+  formatError ++
+  "Error: non typeable expression"
+  ++ end
+
+-- | Type constructors on untyped lambda calculus error message.
+errorTypeConstructors :: String
+errorTypeConstructors =
+  formatError ++
+  "Error: this expression uses type constructors. You may want to activate ':types on'."
+  ++ end
+
+-- | Undefined expression error message.
+errorUndefinedText :: String
+errorUndefinedText =
+  formatError ++
+  "Error: undefined terms on the lambda expression"
+  ++ end
+
+restartText :: String
+restartText = "Mikrokosmos context has been cleaned up"
+
 -- | Prompt line. It is shown when the interpreter asks the user
 --   to introduce a new command.
 promptText :: String
@@ -130,6 +133,7 @@
   "Commands available from the prompt:",
   "\t<expression>\t\t evaluates the expression",
   "\t:quit       \t\t quits the interpreter",
+  "\t:restart    \t\t restarts the interpreter",
   "\t:load <file>\t\t loads the given .mkr library or script",
   "\t:verbose <on/off> \t sets verbose mode on/off",
   "\t:color <on/off> \t sets color mode on/off",
@@ -152,4 +156,4 @@
 
 -- | Version
 version :: String
-version = "0.5.0"
+version = "0.6.0"
diff --git a/source/Interpreter.hs b/source/Interpreter.hs
--- a/source/Interpreter.hs
+++ b/source/Interpreter.hs
@@ -22,6 +22,7 @@
 import           Control.Monad.State.Lazy      
 import           Text.ParserCombinators.Parsec hiding (State)
 import           Data.Char
+import           Data.Maybe
 import           Format
 import           Environment
 import           NamedLambda
@@ -42,6 +43,7 @@
                        | SetColor Bool    -- ^ Changes colors
                        | SetSki Bool      -- ^ Changes ski output
                        | SetTypes Bool    -- ^ Changes type configuration
+                       | SetTopo Bool
                        | Help             -- ^ Shows help
 
 -- | Language action. The language has a number of possible valid statements;
@@ -62,22 +64,32 @@
 act (EvalBind (s,le)) =
   do modify (\env -> addBind env s (simplifyAll $ toBruijn (context env) le))
      return [""]
-act (Execute le) = do
+act (Execute le) = executeExpression le
+
+-- | Executes a lambda expression. Given the context, returns the new
+-- context after the evaluation.
+executeExpression :: NamedLambda -> State Environment [String]
+executeExpression le = do
      env <- get
      let typed = getTypes env
-     let illtyped = typed && typeinference (toBruijn (context env) le) == Nothing
-     let notypes = not typed && usestypecons (toBruijn (context env) le)
+     let bruijn = toBruijn (context env) le
+     let illtyped = typed && isNothing (typeinference bruijn)
+     let notypes = not typed && usestypecons bruijn
+     let verbose = getVerbose env
+     let completeexp = showCompleteExp env $ simplifyAll bruijn
+     let isopen = isOpenExp bruijn
      
-     return $ if illtyped then [formatType ++ "Error: non typeable expression" ++ end ++ "\n"] else
-              if notypes then [formatType ++
-                  "Error: this expression uses type constructors. You may want to activate ':types on'."
-                  ++ end ++ "\n"] else
-            [ unlines $
-              [ show le ] ++
-              [ unlines $ map showReduction $ simplifySteps $ toBruijn (context env) le ] ++
-              [ showCompleteExp env $ simplifyAll $ toBruijn (context env) le ] 
-            ]
-
+     return $
+       if isopen then [errorUndefinedText ++ "\n"] else
+       if illtyped then [errorNonTypeableText ++ "\n"] else
+       if notypes then [errorTypeConstructors ++ "\n"] else
+       if not verbose then [completeexp ++ "\n"] else
+         [unlines $
+           [show le] ++
+           [unlines $ map showReduction $ simplifySteps bruijn] ++
+           [completeexp]
+         ]
+  
 
 -- | Executes multiple actions. Given a context and a set of actions, returns
 -- the new context after the sequence of actions and a text output.
@@ -91,12 +103,14 @@
 showCompleteExp environment expr = let
       lambdaname = show $ nameExp expr
       skiname = if getSki environment
-                 then formatSubs2 ++ " ⇒ " ++ (show $ skiabs $ nameExp expr) ++ end
+                 then formatSubs2 ++ " ⇒ " ++ show (skiabs $ nameExp expr) ++ end
                  else ""
       inferredtype = typeinference expr
       typename = if getTypes environment
                   then formatType ++ " :: " ++ (case inferredtype of
-                                                   Just s -> show s
+                                                   Just s -> if getTopo environment
+                                                             then show (Top s)
+                                                             else show s
                                                    Nothing -> "Type error!") ++ end
                   else ""
       expName = case getExpressionName environment expr of
@@ -107,9 +121,6 @@
     
 
 
-
-
-
 -- Parsing of interpreter command line commands.
 -- | Parses an interpreter action.
 interpreteractionParser :: Parser InterpreterAction
@@ -122,6 +133,7 @@
   , try colorParser
   , try skiOutputParser
   , try typesParser
+  , try topoParser
   , try helpParser
   ]
 
@@ -155,16 +167,10 @@
 commentParser = string "#" >> many anyChar >> return Comment
 
 -- | Parses a "quit" command.
-quitParser :: Parser InterpreterAction
-quitParser = string ":quit" >> return Quit
-
--- | Parses a "restart" command.
-restartParser :: Parser InterpreterAction
+quitParser, restartParser, helpParser :: Parser InterpreterAction
+quitParser    = string ":quit" >> return Quit
 restartParser = string ":restart" >> return Restart
-
--- | Parses a "help" command.
-helpParser :: Parser InterpreterAction
-helpParser = string ":help" >> return Help
+helpParser    = string ":help" >> return Help
 
 -- | Parses a change in a setting
 settingParser :: (Bool -> InterpreterAction) -> String -> Parser InterpreterAction
@@ -177,11 +183,12 @@
     settingoffParser = string (settingname ++ " off") >> return (setSetting False)
 
 -- | Multiple setting parsers
-verboseParser, colorParser, skiOutputParser, typesParser :: Parser InterpreterAction
+verboseParser, colorParser, skiOutputParser, typesParser, topoParser :: Parser InterpreterAction
 verboseParser   = settingParser SetVerbose ":verbose"
 colorParser     = settingParser SetColor   ":color"
 skiOutputParser = settingParser SetSki     ":ski"
 typesParser     = settingParser SetTypes   ":types"
+topoParser      = settingParser SetTopo    ":topology"
 
 
 -- | Parses a "load-file" command.
diff --git a/source/Lambda.hs b/source/Lambda.hs
--- a/source/Lambda.hs
+++ b/source/Lambda.hs
@@ -15,7 +15,7 @@
   , simplifySteps
   , showReduction
   , usestypecons
---  , freein
+  , isOpenExp
   )
 where
 
@@ -40,21 +40,20 @@
 instance Show Exp where
   show = showexp
 
-
 -- | Shows an expression with DeBruijn indexes.
 showexp :: Exp -> String
 showexp (Var n)        = show n
 showexp (Lambda e)     = "λ" ++ showexp e ++ ""
 showexp (App f g)      = "(" ++ showexp f ++ " " ++ showexp g ++ ")"
 showexp (Pair a b)     = "(" ++ showexp a ++ "," ++ showexp b ++ ")"
-showexp (Pi1 m)        = "(" ++ "fst " ++ showexp m ++ ")"
-showexp (Pi2 m)        = "(" ++ "snd " ++ showexp m ++ ")"
-showexp (Inl m)        = "(" ++ "inl " ++ showexp m ++ ")"
-showexp (Inr m)        = "(" ++ "inr " ++ showexp m ++ ")"
-showexp (Caseof m n p) = "(" ++ "case " ++ showexp m ++ " of " ++ showexp n ++ "; " ++ showexp p ++ ")"
-showexp (Unit)         = "*"
-showexp (Abort a)      = "(abort " ++ showexp a ++ ")"
-showexp (Absurd a)     = "(absurd " ++ showexp a ++ ")"
+showexp (Pi1 m)        = "(" ++ "FST " ++ showexp m ++ ")"
+showexp (Pi2 m)        = "(" ++ "SND " ++ showexp m ++ ")"
+showexp (Inl m)        = "(" ++ "INL " ++ showexp m ++ ")"
+showexp (Inr m)        = "(" ++ "INR " ++ showexp m ++ ")"
+showexp (Caseof m n p) = "(" ++ "CASE " ++ showexp m ++ " OF " ++ showexp n ++ "; " ++ showexp p ++ ")"
+showexp Unit         = "*"
+showexp (Abort a)      = "(ABORT " ++ showexp a ++ ")"
+showexp (Absurd a)     = "(ABSURD " ++ showexp a ++ ")"
 
 -- | Shows an expression coloring the next reduction.
 showReduction :: Exp -> String
@@ -64,6 +63,7 @@
 showReduction (App rs x)         = "(" ++ showReduction rs ++ " " ++ showReduction x ++ ")"
 showReduction e                  = show e
 
+
 -- | Colors a beta reduction
 betaColor :: Exp -> String
 betaColor (App (Lambda e) x) =
@@ -115,7 +115,7 @@
 simplify (Lambda e)           = Lambda (simplify e)
 simplify (App (Lambda f) x)   = betared (App (Lambda f) x)
 simplify (App (Var e) x)      = App (Var e) (simplify x)
-simplify (App (App f g) x)    = App (simplify (App f g)) x
+simplify (App (App f g) x)    = App (simplify (App f g)) (simplify x)
 simplify (App a b)            = App (simplify a) (simplify b)
 simplify (Var e)              = Var e
 simplify (Pair a b)           = Pair (simplify a) (simplify b)
@@ -128,7 +128,7 @@
 simplify (Caseof (Inl m) a _) = App a m
 simplify (Caseof (Inr m) _ b) = App b m
 simplify (Caseof a b c)       = Caseof (simplify a) (simplify b) (simplify c)
-simplify (Unit)               = Unit
+simplify Unit               = Unit
 simplify (Abort a)            = Abort (simplify a)
 simplify (Absurd a)           = Absurd (simplify a)
 
@@ -151,7 +151,7 @@
 substitute n x (Inl a) = Inl (substitute n x a)
 substitute n x (Inr a) = Inr (substitute n x a)
 substitute n x (Caseof a b c) = Caseof (substitute n x a) (substitute n x b) (substitute n x c)
-substitute _ _ (Unit) = Unit
+substitute _ _ Unit = Unit
 substitute n x (Abort a) = Abort (substitute n x a)
 substitute n x (Absurd a) = Absurd (substitute n x a)
 substitute n x (Var m)
@@ -177,7 +177,7 @@
 incrementFreeVars n (Inl a)    = Inl (incrementFreeVars n a)
 incrementFreeVars n (Inr a)    = Inr (incrementFreeVars n a)
 incrementFreeVars n (Caseof a b c) = Caseof (incrementFreeVars n a) (incrementFreeVars n b) (incrementFreeVars n c)
-incrementFreeVars _ (Unit)    = Unit
+incrementFreeVars _ Unit    = Unit
 incrementFreeVars n (Abort a) = Abort (incrementFreeVars n a)
 incrementFreeVars n (Absurd a) = Absurd (incrementFreeVars n a)
 
@@ -188,8 +188,25 @@
 -- freein n (Lambda e) = freein (succ n) e
 -- freein n (App u v)  = (freein n u) && (freein n v)
 
+-- | Returns true if the expression has at least one type constructor.
 usestypecons :: Exp -> Bool
 usestypecons (Var _) = False
 usestypecons (App a b) = usestypecons a || usestypecons b
 usestypecons (Lambda b) = usestypecons b
 usestypecons _ = True
+
+
+-- | Returns true if the expression contains open undefined variables.
+isOpenExp :: Exp -> Bool
+isOpenExp (Var n) = n == 0
+isOpenExp (App a b) = isOpenExp a || isOpenExp b
+isOpenExp (Lambda a) = isOpenExp a
+isOpenExp (Pair a b) = isOpenExp a || isOpenExp b
+isOpenExp (Pi1 a) = isOpenExp a
+isOpenExp (Pi2 a) = isOpenExp a
+isOpenExp (Inl a) = isOpenExp a
+isOpenExp (Inr a) = isOpenExp a
+isOpenExp (Caseof a b c) = isOpenExp a || isOpenExp b || isOpenExp c
+isOpenExp Unit = False
+isOpenExp (Abort a) = isOpenExp a
+isOpenExp (Absurd a) = isOpenExp a
diff --git a/source/Main.hs b/source/Main.hs
--- a/source/Main.hs
+++ b/source/Main.hs
@@ -25,19 +25,18 @@
   -- Uses the Options library, which requires the program to start with
   -- runCommand. The flags are stored in opts and other command line arguments
   -- are stored in args.
-  runCommand $ \opts args -> do
-  
+  runCommand $ \opts args
   -- Reads the flags
-  case flagVersion opts of
-    True -> putStrLn versionText
-    False ->
-      case args of
-        [] -> runInputT defaultSettings ( outputStrLn initialText
-                                          >> interpreterLoop defaultEnv
-                                        )
-        [filename] -> executeFile filename
-        _ -> putStrLn "Wrong number of arguments"
-
+   ->
+    if flagVersion opts
+      then putStrLn versionText
+      else case args of
+             [] ->
+               runInputT
+                 defaultSettings
+                 (outputStrLn initialText >> interpreterLoop defaultEnv)
+             [filename] -> executeFile filename
+             _ -> putStrLn "Wrong number of arguments"
 
 -- | Interpreter awaiting for an instruction.
 interpreterLoop :: Environment -> InputT IO ()
@@ -49,88 +48,65 @@
         case minput of
           Nothing -> Quit
           Just "" -> EmptyLine
-          Just input -> case parse interpreteractionParser "" input of
-            Left _  -> Error
-            Right a -> a
-
+          Just input ->
+            case parse interpreteractionParser "" input of
+              Left _ -> Error
+              Right a -> a
   -- Executes the parsed action, every action may affect the
-  -- context in a way, and returns the control to the interpreter. 
-  case interpreteraction of
+  -- context in a way, and returns the control to the interpreter.
+  case interpreteraction
     -- Interprets an action
-    Interpret action -> case runState (act action) environment of
-                          (output, newenv) -> do
-                            outputActions newenv output
-                            interpreterLoop newenv
-
+        of
+    Interpret action ->
+      case runState (act action) environment of
+        (output, newenv) -> do
+          outputActions newenv output
+          interpreterLoop newenv
     -- Loads a module and its dependencies given its name.
     -- Avoids repeated modules keeping only their first ocurrence.
     Load modulename -> do
-      modules <- lift $ (nub <$> readAllModuleDepsRecursively [modulename])
+      modules <- lift (nub <$> readAllModuleDepsRecursively [modulename])
       files <- lift $ mapM findFilename modules
-
       -- Concats all the module contents
-      maybeactions <- (fmap concat) . sequence <$> (lift $ mapM loadFile files)
+      maybeactions <- fmap concat . sequence <$> lift (mapM loadFile files)
       case maybeactions of
         Nothing -> do
           outputStrLn "Error loading file"
           interpreterLoop environment
-        Just actions -> case runState (multipleAct actions) environment of
-                          (output, newenv) -> do
-                            outputActions newenv output
-                            interpreterLoop newenv
-    
+        Just actions ->
+          case runState (multipleAct actions) environment of
+            (output, newenv) -> do
+              outputActions newenv output
+              interpreterLoop newenv
     -- Ignores the empty line
     EmptyLine -> interpreterLoop environment
-    
-    -- Exists the interpreter
+    -- Exits the interpreter
     Quit -> return ()
-
     -- Restarts the interpreter context
-    Restart -> interpreterLoop defaultEnv
-
+    Restart -> outputStrLn restartText >> interpreterLoop defaultEnv
     -- Unknown command
-    Error -> do
-      outputStr (if getColor environment then formatFormula else "")
-      outputStrLn "Unknown command"
-      outputStr end
-      interpreterLoop environment
-
+    Error -> outputStrLn errorUnknownCommand >> interpreterLoop environment
     -- Sets the verbose option
-    SetVerbose setting -> do
-      outputStrLn $
-        (if getColor environment then formatFormula else "") ++
-        "verbose mode: " ++ if setting then "on" else "off" ++
-        end
-      interpreterLoop (changeVerbose environment setting)
-      
-    -- Sets the color option
-    SetColor setting -> do
-      outputStrLn $
-        (if getColor environment then formatFormula else "") ++
-        "color mode: " ++ if setting then "on" else "off" ++
-        end
-      interpreterLoop (changeColor environment setting)
-
-    -- Sets the ski option
-    SetSki setting -> do
-      outputStrLn $
-        (if getColor environment then formatFormula else "") ++
-        "ski mode: " ++ if setting then "on" else "off" ++
-        end
-      interpreterLoop (changeSkioutput environment setting)
-
-    -- Sets the types option
-    SetTypes setting -> do
-      outputStrLn $
-        (if getColor environment then formatFormula else "") ++
-        "types: " ++ if setting then "on" else "off" ++
-        end
-      interpreterLoop (changeTypes environment setting)
-
+    SetVerbose setting ->
+      setOption environment setting changeVerbose "verbose: "
+    SetColor setting -> setOption environment setting changeColor "color mode: "
+    SetSki setting -> setOption environment setting changeSkioutput "ski mode: "
+    SetTypes setting -> setOption environment setting changeTypes "types: "
+    SetTopo setting -> setOption environment setting changeTopo "topo mode: "
     -- Prints the help
     Help -> outputStr helpText >> interpreterLoop environment
 
 
+-- | Sets the given option on/off.
+setOption :: Environment -> Bool ->
+             (Environment -> Bool -> Environment) ->
+             String ->
+             InputT IO ()
+setOption environment setting change message = do
+  outputStrLn $
+    (if getColor environment then formatFormula else "") ++
+    message ++ if setting then "on" else "off" ++ end  
+  interpreterLoop (change environment setting)
 
 
 -- | Outputs results from actions. Given a list of options and outputs,
@@ -141,16 +117,10 @@
     mapM_ (outputStr . format) output
     outputStr end
   where
-    format = formatColor . formatVerbose
-
+    format = formatColor
     formatColor s
       | getColor environment = s
       | otherwise            = unlines $ map decolor $ lines s
-    
-    formatVerbose "" = ""
-    formatVerbose s
-      | not (getVerbose environment) = (++"\n") . last . lines $ s
-      | otherwise                    = s
 
 
 
@@ -160,7 +130,7 @@
 loadFile :: String -> IO (Maybe [Action])
 loadFile filename = do
   putStrLn $ formatLoading ++ "Loading " ++ filename ++ "..." ++ end
-  input <- try $ (readFile filename) :: IO (Either IOException String)
+  input <- try $ readFile filename :: IO (Either IOException String)
   case input of
     Left _ -> return Nothing
     Right inputs -> do
@@ -176,19 +146,19 @@
 executeFile filename = do
   maybeloadfile <- loadFile filename
   case maybeloadfile of
-    Nothing    -> putStrLn "Error loading file"
-    Just actions -> case runState (multipleAct actions) defaultEnv of
-                      (outputs, _) -> mapM_ (putStr . format) outputs
-                      where
-                        format :: String -> String
-                        format "" = ""
-                        format s = (++"\n") . last . lines $ s
+    Nothing -> putStrLn "Error loading file"
+    Just actions ->
+      case runState (multipleAct actions) defaultEnv of
+        (outputs, _) -> mapM_ (putStr . format) outputs
+      where format :: String -> String
+            format "" = ""
+            format s = (++ "\n") . last . lines $ s
 
 
 -- | Reads module dependencies
 readFileDependencies :: Filename -> IO [Modulename]
 readFileDependencies filename = do
-  input <- try $ (readFile filename) :: IO (Either IOException String)
+  input <- try $ readFile filename :: IO (Either IOException String)
   case input of
     Left _ -> return []
     Right inputs -> return $
@@ -222,6 +192,7 @@
     , "./" ++ s ++ ".mkr"
     , appdir ++ "/" ++ s ++ ".mkr"
     , homedir ++ "/" ++ s ++ ".mkr"
+    , "/usr/lib/mikrokosmos/" ++ s ++ ".mkr"
     ]
 
 
@@ -235,7 +206,5 @@
 instance Options MainFlags where
   -- | Flags definition
   defineOptions = pure MainFlags
-    <*> simpleOption "exec" ""
-    "A file to execute and show its results"
-    <*> simpleOption "version" False
-    "Show program version"
+    <*> simpleOption "exec"    ""    "A file to execute and show its results"
+    <*> simpleOption "version" False "Show program version"
diff --git a/source/NamedLambda.hs b/source/NamedLambda.hs
--- a/source/NamedLambda.hs
+++ b/source/NamedLambda.hs
@@ -46,6 +46,7 @@
                  | TypedUnit                                     -- ^ unit
                  | TypedAbort NamedLambda                        -- ^ abort
                  | TypedAbsurd NamedLambda                       -- ^ absurd
+                 deriving (Eq)
 
 -- | Parses a lambda expression with named variables.
 -- A lambda expression is a sequence of one or more autonomous
@@ -93,25 +94,21 @@
 -- | Parses a lambda abstraction. The '\' is used as lambda. 
 lambdaAbstractionParser :: Parser NamedLambda
 lambdaAbstractionParser = LambdaAbstraction <$>
-  (char lambdaChar >> nameParser) <*> (char '.' >> lambdaexp)
+  (lambdaChar >> nameParser) <*> (char '.' >> lambdaexp)
 
 -- | Char used to represent lambda in user's input.
-lambdaChar :: Char
-lambdaChar = '\\'
+lambdaChar :: Parser Char
+lambdaChar = choice [try $ char '\\', try $ char 'λ']
 
 pairParser :: Parser NamedLambda
 pairParser = parens (TypedPair <$> lambdaexp <*> (char ',' >> lambdaexp))
 
-pi1Parser :: Parser NamedLambda
+pi1Parser, pi2Parser :: Parser NamedLambda
 pi1Parser = TypedPi1 <$> (string "FST " >> lambdaexp)
-
-pi2Parser :: Parser NamedLambda
 pi2Parser = TypedPi2 <$> (string "SND " >> lambdaexp)
 
-inlParser :: Parser NamedLambda
+inlParser, inrParser :: Parser NamedLambda
 inlParser = TypedInl <$> (string "INL " >> lambdaexp)
-
-inrParser :: Parser NamedLambda
 inrParser = TypedInr <$> (string "INR " >> lambdaexp)
 
 caseParser :: Parser NamedLambda
@@ -138,7 +135,7 @@
 showNamedLambda (TypedInl a)            = "(" ++ "INL " ++ showNamedLambda a ++ ")"
 showNamedLambda (TypedInr a)            = "(" ++ "INR " ++ showNamedLambda a ++ ")"
 showNamedLambda (TypedCase a b c)       = "(" ++ "CASE " ++ showNamedLambda a ++ " of " ++ showNamedLambda b ++ "; " ++ showNamedLambda c ++ ")"
-showNamedLambda (TypedUnit)             = "UNIT"
+showNamedLambda TypedUnit             = "UNIT"
 showNamedLambda (TypedAbort a)          = "(" ++ "ABORT " ++ showNamedLambda a ++ ")"
 showNamedLambda (TypedAbsurd a)          = "(" ++ "ABSURD " ++ showNamedLambda a ++ ")"
 
@@ -172,7 +169,7 @@
 tobruijn d context (TypedInl a) = Inl (tobruijn d context a)
 tobruijn d context (TypedInr a) = Inr (tobruijn d context a)
 tobruijn d context (TypedCase a b c) = Caseof (tobruijn d context a) (tobruijn d context b) (tobruijn d context c)
-tobruijn _ _       (TypedUnit) = Unit
+tobruijn _ _       TypedUnit = Unit
 tobruijn d context (TypedAbort a) = Abort (tobruijn d context a)
 tobruijn d context (TypedAbsurd a) = Absurd (tobruijn d context a)
 
@@ -198,9 +195,9 @@
 nameIndexes used new (Inl a)        = TypedInl (nameIndexes used new a)
 nameIndexes used new (Inr a)        = TypedInr (nameIndexes used new a)
 nameIndexes used new (Caseof a b c) = TypedCase (nameIndexes used new a) (nameIndexes used new b) (nameIndexes used new c)
-nameIndexes _    _   (Unit)         = TypedUnit
+nameIndexes _    _   Unit         = TypedUnit
 nameIndexes used new (Abort a)      = TypedAbort (nameIndexes used new a)
-nameIndexes used new (Absurd a)      = TypedAbsurd (nameIndexes used new a)
+nameIndexes used new (Absurd a)     = TypedAbsurd (nameIndexes used new a)
 
 
 -- | Gives names to every variable in a deBruijn expression using
diff --git a/source/Ski.hs b/source/Ski.hs
--- a/source/Ski.hs
+++ b/source/Ski.hs
@@ -9,7 +9,8 @@
 -}
 
 module Ski
-  ( Ski (S, K, I, Comb)
+  ( Ski (S, K, I, Comb, Cte,
+         Spair, Spi1, Spi2, Sinl, Sinr, Scase, Sunit, Sabort, Sabsurd)
   , skiabs
   )
 where
@@ -87,6 +88,6 @@
 
 -- | Checks if a given variable is used on a SKI expression.
 freein :: String -> Ski -> Bool
-freein x (Cte y)    = not (x == y)
+freein x (Cte y)    = x /= y
 freein x (Comb u v) = freein x u && freein x v
 freein _ _ = True
diff --git a/source/Types.hs b/source/Types.hs
--- a/source/Types.hs
+++ b/source/Types.hs
@@ -1,8 +1,7 @@
 module Types
-  ( Type (Tvar, Arrow)
-  , typeinfer
+  ( Type (Tvar, Arrow, Times, Union, Unitty, Bottom)
   , typeinference
-  , normalize
+  , Top (Top)
   )
 where
 
@@ -13,10 +12,10 @@
 
 -- | A type context is a map from deBruijn indices to types. Given
 -- any lambda variable as a deBruijn index, it returns its type.
-type Context      = Map.Map Integer Type
+type Context = Map.Map Integer Type
 
 -- | A type variable is an integer.
-type Variable     = Integer
+type Variable = Integer
 
 -- | A type substitution is a function that can be applied to any type
 -- to get a new one.
@@ -24,21 +23,25 @@
 
 -- | A type template is a free type variable or an arrow between two
 -- types; that is, the function type.
-data Type         = Tvar Variable
-                  | Arrow Type Type
-                  | Times Type Type
-                  | Union Type Type
-                  | Unitty
-                  | Bottom
+data Type
+  = Tvar Variable
+  | Arrow Type
+          Type
+  | Times Type
+          Type
+  | Union Type
+          Type
+  | Unitty
+  | Bottom
   deriving (Eq)
 
 instance Show Type where
-  show (Tvar t)    = typevariableNames !! (fromInteger t)
+  show (Tvar t) = typevariableNames !! fromInteger t
   show (Arrow a b) = showparens a ++ " → " ++ show b
   show (Times a b) = showparens a ++ " × " ++ showparens b
   show (Union a b) = showparens a ++ " + " ++ showparens b
-  show (Unitty)    = "⊤"
-  show (Bottom)    = "⊥"
+  show Unitty = "⊤"
+  show (Bottom) = "⊥"
 
 showparens :: Type -> String
 showparens (Tvar t) = show (Tvar t)
@@ -64,7 +67,7 @@
 occurs x (Arrow a b) = occurs x a || occurs x b
 occurs x (Times a b) = occurs x a || occurs x b
 occurs x (Union a b) = occurs x a || occurs x b
-occurs _ (Unitty)    = False
+occurs _ Unitty    = False
 occurs _ (Bottom)    = False
 
 -- | Unifies two types with their most general unifier. Returns the substitution
@@ -79,22 +82,20 @@
 unify a (Tvar y)
   | occurs y a = Nothing
   | otherwise  = Just (subs y a)
-unify (Arrow a b) (Arrow c d) = do
-  p <- unify b d
-  q <- unify (p a) (p c)
-  return (q . p)
-unify (Times a b) (Times c d) = do
-  p <- unify b d
-  q <- unify (p a) (p c)
-  return (q . p)
-unify (Union a b) (Union c d) = do
-  p <- unify b d
-  q <- unify (p a) (p c)
-  return (q . p)
+unify (Arrow a b) (Arrow c d) = unifypair (a,b) (c,d)
+unify (Times a b) (Times c d) = unifypair (a,b) (c,d)
+unify (Union a b) (Union c d) = unifypair (a, b) (c, d)
 unify Unitty Unitty = Just id
 unify Bottom Bottom = Just id
 unify _ _ = Nothing
 
+-- | Unifies a pair of types
+unifypair :: (Type,Type) -> (Type,Type) -> Maybe Substitution
+unifypair (a,b) (c,d) = do
+  p <- unify b d
+  q <- unify (p a) (p c)
+  return (q . p)
+
 -- | Apply a substitution to all the types on a type context.
 applyctx :: Substitution -> Context -> Context
 applyctx = Map.map
@@ -164,12 +165,12 @@
 
 typeinfer (x:y:vars) ctx (Inl m) a = do
   sigma <- unify a (Union (Tvar x) (Tvar y))
-  tau   <- typeinfer vars (applyctx sigma ctx) m (sigma (Tvar x))
+  tau <- typeinfer vars (applyctx sigma ctx) m (sigma (Tvar x))
   return (tau . sigma)
 
 typeinfer (x:y:vars) ctx (Inr m) a = do
   sigma <- unify a (Union (Tvar x) (Tvar y))
-  tau   <- typeinfer vars (applyctx sigma ctx) m (sigma (Tvar y))
+  tau <- typeinfer vars (applyctx sigma ctx) m (sigma (Tvar y))
   return (tau . sigma)
 
 typeinfer (x:y:vars) ctx (Caseof m f g) a = do
@@ -232,8 +233,8 @@
 -- | Applies a set of variable substitutions to a type to normalize it.
 applynormalization :: Map.Map Integer Integer -> Type -> Type
 applynormalization sub (Tvar m) = case Map.lookup m sub of
-                                    Just n -> (Tvar n)
-                                    Nothing -> (Tvar m)
+                                    Just n -> Tvar n
+                                    Nothing -> Tvar m
 applynormalization sub (Arrow a b) = Arrow (applynormalization sub a) (applynormalization sub b)
 applynormalization sub (Times a b) = Times (applynormalization sub a) (applynormalization sub b)
 applynormalization sub (Union a b) = Union (applynormalization sub a) (applynormalization sub b)
@@ -246,3 +247,22 @@
 -- the smaller possible ones.
 normalize :: Type -> Type
 normalize t = applynormalization (fst $ normalizeTemplate Map.empty 0 t) t
+
+
+
+
+-- This is definitely not an easter egg
+newtype Top = Top Type
+instance Show Top where
+  show (Top (Tvar t))         = typevariableNames !! fromInteger t
+  show (Top (Arrow a Bottom)) = "(Ω∖" ++ showparensT (Top a)  ++ ")ᴼ"
+  show (Top (Arrow a b))      = "((Ω∖" ++ showparensT (Top a) ++ ") ∪ " ++ showparensT (Top b) ++ ")ᴼ"
+  show (Top (Times a b))      = showparensT (Top a) ++ " ∩ " ++ showparensT (Top b)
+  show (Top (Union a b))      = showparensT (Top a) ++ " ∪ " ++ showparensT (Top b)
+  show (Top Unitty)           = "Ω"
+  show (Top (Bottom))         = "Ø"
+showparensT :: Top -> String
+showparensT (Top (Tvar t)) = show (Top (Tvar t))
+showparensT (Top Unitty) = show (Top Unitty)
+showparensT (Top Bottom) = show (Top Bottom)
+showparensT (Top m) = "(" ++ show (Top m) ++ ")"
diff --git a/tests/test.hs b/tests/test.hs
new file mode 100644
--- /dev/null
+++ b/tests/test.hs
@@ -0,0 +1,131 @@
+import Test.Tasty
+import Test.Tasty.HUnit
+import Test.Tasty.QuickCheck as QC
+
+import Text.ParserCombinators.Parsec
+import NamedLambda
+import Lambda
+import Types
+import Ski
+import Environment
+
+
+main :: IO ()
+main = defaultMain tests
+
+tests :: TestTree
+tests = testGroup "Tests"
+  [ parserTests
+  , typeinferTests
+  , skiabsTests
+  , lambdaProps
+  ]
+
+-- Unit tests
+parserTests :: TestTree
+parserTests = testGroup "Parser tests"
+  [ testCase "INR parser test" $
+    parse lambdaexp "" "INR (\\x.y)"
+    @?=
+    Right (TypedInr (LambdaAbstraction "x" (LambdaVariable "y")))
+
+  , testCase "INL parser test" $
+    parse lambdaexp "" "INL (\\ab.cd)"
+    @?=
+    Right (TypedInl (LambdaAbstraction "ab" (LambdaVariable "cd")))
+
+  , testCase "Spaces between lambdas test" $
+    parse lambdaexp "" "(\\x.      x)"
+    @?=
+    Right (LambdaAbstraction "x" (LambdaVariable "x"))
+
+  , testCase "Multiple-character variable name test" $
+    parse lambdaexp "" "(\\asdf. asdf)"
+    @?=
+    Right (LambdaAbstraction "asdf" (LambdaVariable "asdf"))
+  ]
+
+typeinferTests :: TestTree
+typeinferTests = testGroup "Type inference tests"
+  [ testCase "Identity type inference" $
+    typeinference (Lambda (Var 1))
+    @?=
+    Just (Arrow (Tvar 0) (Tvar 0))
+
+  , testCase "Double negation of LEM" $
+    typeinference (Lambda (Absurd ((App (Var 1) (Inr (Lambda (App (Var 2) (Inl (Var 1)))))))))
+    @?=
+    Just (Arrow (Arrow (Union (Tvar 0) (Arrow (Tvar 0) Bottom)) Bottom) Bottom)
+  ]
+
+skiabsTests :: TestTree
+skiabsTests = testGroup "SKI abstraction tests"
+  [ testCase "Identity SKI abstraction" $
+    skiabs (LambdaAbstraction "x" (LambdaVariable "x"))
+    @?=
+    I
+
+  , testCase "Numeral 2 SKI abstraction" $
+    skiabs (LambdaAbstraction "a"
+            (LambdaAbstraction "b"
+              (LambdaApplication (LambdaVariable "a")
+                (LambdaApplication (LambdaVariable "a") (LambdaVariable "b")))))
+    @?=
+    Comb (Comb S (Comb (Comb S (Comb K S)) K)) I
+  ]
+
+
+-- Lambda properties
+lambdaProps :: TestTree
+lambdaProps = testGroup "Lambda expression properties (quickcheck)"
+  [ QC.testProperty "expression -> named -> expression" $
+      \exp -> toBruijn emptyContext (nameExp exp) == exp
+  , QC.testProperty "open expressions not allowed" $
+      \exp -> isOpenExp exp == False
+  ]
+  
+
+-- Arbitrary untyped lambda expressions
+-- {-# LANGUAGE TypeSynonymInstances #-}
+-- type UntypedExp = Exp
+-- instance Arbitrary UntypedExp where
+--   arbitrary = sized (untlambda 0)
+
+-- untlambda :: Int -> Int -> Gen UntypedExp
+-- untlambda 0   0    = return $ Lambda (Var 1)
+-- untlambda 0   size = Lambda <$> untlambda 1 (size-1)
+-- untlambda lim 0    = Var <$> (toInteger <$> (choose (1, lim)))
+-- untlambda lim size = oneof
+--   [ Var <$> (toInteger <$> choose (1, lim))
+--   , Lambda <$> untlambda (succ lim) (size-1)
+--   , App <$> untlambda lim (div size 2) <*> untlambda lim (div size 2)
+--   ]
+
+
+-- Arbitrary typed lambda expressions
+instance Arbitrary Exp where
+  arbitrary = sized (lambda 0)
+
+lambda :: Int -> Int -> Gen Exp
+lambda 0   0    = return $ Lambda (Var 1)
+lambda 0   size = Lambda <$> lambda 1 (size-1)
+lambda lim 0    = Var <$> (toInteger <$> (choose (1, lim)))
+lambda lim size = oneof
+  [ Var <$> (toInteger <$> choose (1, lim))
+  , Lambda <$> lambda (succ lim) (size-1)
+  , App <$> lambda lim (div size 2) <*> lambda lim (div size 2)
+  , Pair <$> lambda lim (div size 2) <*> lambda lim (div size 2)
+  , Pi1 <$> (Pair <$> lambda lim (div size 2) <*> lambda lim (div size 2))
+  , Pi2 <$> (Pair <$> lambda lim (div size 2) <*> lambda lim (div size 2))
+  , Inl <$> lambda lim (size-1)
+  , Inr <$> lambda lim (size-1)
+  , Caseof <$> (Inl <$> lambda lim (div size 3))
+           <*> (Lambda <$> lambda (succ lim) (div size 3))
+           <*> (Lambda <$> lambda (succ lim) (div size 3))
+  , Caseof <$> (Inr <$> lambda lim (div size 3))
+           <*> (Lambda <$> lambda (succ lim) (div size 3))
+           <*> (Lambda <$> lambda (succ lim) (div size 3))
+  , return Unit
+  , Abort <$> lambda lim (size-1)
+  , Absurd <$> lambda lim (size-1)
+  ]