diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,7 +1,10 @@
 # mikrokosmos
 
+![Version](https://img.shields.io/badge/version-0.8.0-blue.svg)
+![Travis (.org)](https://img.shields.io/travis/mroman42/mikrokosmos.svg)
+
 <p align="center">
-  <img src ="https://raw.githubusercontent.com/M42/mikrokosmos/master/docs/icon.svg.png" />
+  <img src ="https://raw.githubusercontent.com/mroman42/mikrokosmos/master/docs/icon.svg.png" />
 </p>
 
 **Mikrokosmos** is a λ-calculus interpreter, borrowing its name from the series of
@@ -9,6 +12,7 @@
 It aims to provide students with a tool to learn and understand λ-calculus. It supports both untyped λ-calculus 
 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).
+ * [Try Mikrokosmos!](https://mroman42.github.io/mikrokosmos/)
+ * [Mikrokosmos tutorial](https://mroman42.github.io/mikrokosmos/tutorial.html).
+ * [Mikrokosmos user's guide](https://mroman42.github.io/mikrokosmos/userguide.html).
  * [Mikrokosmos on Hackage](https://hackage.haskell.org/package/mikrokosmos).
diff --git a/mikrokosmos.cabal b/mikrokosmos.cabal
--- a/mikrokosmos.cabal
+++ b/mikrokosmos.cabal
@@ -1,23 +1,22 @@
 name:                mikrokosmos
-version:             0.6.0
+version:             0.8.0
 synopsis:            Lambda calculus interpreter
 description:         A didactic untyped lambda calculus interpreter.
-homepage:            https://github.com/M42/mikrokosmos
-bug-reports:         https://github.com/M42/mikrokosmos/issues
+homepage:            https://github.com/mroman42/mikrokosmos
+bug-reports:         https://github.com/mroman42/mikrokosmos/issues
 license:             GPL-3
 license-file:        LICENSE
-author:              Mario Román (M42)
+author:              Mario Román (mroman42)
 maintainer:          mromang08+github@gmail.com
 category:            Language
 build-type:          Simple
 extra-source-files:  README.md
 cabal-version:       >=1.10
 tested-with:         GHC == 8.0.2
-extra-source-files:  std.mkr
                                           
 source-repository head
   type:           git
-  location:       git://github.com/M42/mikrokosmos.git
+  location:       git://github.com/mroman42/mikrokosmos.git
 
 
                        
@@ -36,6 +35,7 @@
                        tasty,
                        tasty-hunit,
                        tasty-quickcheck,
+                       tasty-golden,
                        directory >= 1.0
                        
   other-modules:       Format
@@ -45,7 +45,10 @@
                        Interpreter
                        Environment
                        Ski
-                       Types
+                       Libraries
+                       Stlc.Types
+                       Stlc.Gentzen
+                       Stlc.Block
                        
   default-language:    Haskell2010
   ghc-options:         -Wall
@@ -60,6 +63,7 @@
                   source
   main-is:
     test.hs
+    
   build-depends: base >=4.7 && <5,
                  mtl >=2.2,
                  containers >= 0.5,
@@ -71,8 +75,11 @@
                  options,
                  tasty,
                  tasty-hunit,
+                 tasty-golden,
                  tasty-quickcheck,
-                 directory >= 1.0
+                 directory >= 1.0,
+                 process
+                 
   other-modules: Format
                  Lambda
                  NamedLambda
@@ -80,4 +87,8 @@
                  Interpreter
                  Environment
                  Ski
-                 Types
+                 Libraries
+                 Stlc.Types
+                 Stlc.Gentzen
+                 Stlc.Block
+                 
diff --git a/source/Format.hs b/source/Format.hs
--- a/source/Format.hs
+++ b/source/Format.hs
@@ -32,6 +32,7 @@
   , errorTypeConstructors
   , errorUndefinedText
   , errorUnknownCommand
+  , errorNotFoundText
   )
 where
 
@@ -85,6 +86,7 @@
   , formatType
   , formatPrompt
   , formatLoading
+  , formatError
   , end
   ]
 
@@ -118,6 +120,12 @@
   "Error: undefined terms on the lambda expression"
   ++ end
 
+errorNotFoundText :: String
+errorNotFoundText =
+  formatError ++
+  "Error: module or dependencies cannot be found"
+  ++ end
+
 restartText :: String
 restartText = "Mikrokosmos context has been cleaned up"
 
@@ -150,10 +158,10 @@
   formatFormula ++ "Version " ++ version ++ ". GNU General Public License Version 3." ++ end
   ]
 
--- | Version complete text
+-- | Version, complete text
 versionText :: String
 versionText = "Mikrokosmos, version " ++ version
 
 -- | Version
 version :: String
-version = "0.6.0"
+version = "0.8.0"
diff --git a/source/Interpreter.hs b/source/Interpreter.hs
--- a/source/Interpreter.hs
+++ b/source/Interpreter.hs
@@ -15,6 +15,9 @@
   , multipleAct
   , Action (..)
   , actionParser
+  , executeWithEnv
+  , librariesEnv
+  , preformat
   )
 where
 
@@ -27,45 +30,115 @@
 import           Environment
 import           NamedLambda
 import           Lambda
+import           Libraries
 import           Ski
-import           Types
+import           Stlc.Types
+import           Stlc.Gentzen
 
 
+-- | Execute a block of code in a given environment
+executeWithEnv :: Environment -> String -> (String, Environment)
+executeWithEnv initEnv block = do
+  let parsing = map (parse actionParser "" . preformat) . filter (/="") . lines $ block
+  let actions = mapMaybe (\x -> case x of
+                             Left _  -> Nothing
+                             Right a -> Just a) parsing
+  case runState (multipleAct actions) initEnv of
+    (outputs, env) -> (unlines outputs, env)
+
+-- | Default environment plus standard libraries
+librariesEnv :: Environment
+librariesEnv = snd $ executeWithEnv defaultEnv stdlibraries
+
+-- | Preformats text before sending it to the interpreter
+preformat :: String -> String
+preformat = reverse . dropWhile (==' ') . reverse . dropWhile (==' ')
+
 -- | Interpreter action. It can be a language action (binding and evaluation)
 -- or an interpreter specific one, such as "quit".
 data InterpreterAction = Interpret Action -- ^ Language action
-                       | EmptyLine        -- ^ Empty line, it will be ignored
-                       | Error            -- ^ Error on the interpreter
                        | Quit             -- ^ Close the interpreter
-                       | Restart          -- ^ Restarts the environment
                        | Load String      -- ^ Load the given file
-                       | SetVerbose Bool  -- ^ Changes verbosity
-                       | 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;
 -- all on the following possible forms.
 data Action = Bind (String, NamedLambda)     -- ^ bind a name to an expression
             | EvalBind (String, NamedLambda) -- ^ bind a name to an expression and simplify it
             | Execute NamedLambda            -- ^ execute an expression
+            | Diagram NamedLambda            -- ^ show the diagram of a lambda expression
+            | SimpDiagram NamedLambda        -- ^ show the diagram of the simplified expression
             | Comment                        -- ^ comment
-
+            | EmptyLine                      -- ^ empty line, it will be ignored
+            | Error                          -- ^ error on the interpreter
+            | Restart                        -- ^ restarts the environment
+            | Help                           -- ^ shows help
+            | Ask String                     -- ^ asks for the definition of a function
+            | SetVerbose Bool                -- ^ changes verbosity
+            | SetColor Bool                  -- ^ changes colors
+            | SetSki Bool                    -- ^ changes ski output
+            | SetTypes Bool                  -- ^ changes type configuration
+            | SetTopo Bool
 
+              
 -- | Executes a language action. Given a context and an action, returns
 -- the new context after the action and a text output.
 act :: Action -> State Environment [String]
 act Comment = return [""]
-act (Bind (s,le)) =
-  do modify (\env -> addBind env s (toBruijn (context env) le))
-     return [""]
-act (EvalBind (s,le)) =
-  do modify (\env -> addBind env s (simplifyAll $ toBruijn (context env) le))
-     return [""]
+act (Bind (s,le)) = do
+  modify (\env -> addBind env s (toBruijn (context env) le))
+  return [""]
+act (EvalBind (s,le)) = do
+  modify (\env -> addBind env s (simplifyAll $ toBruijn (context env) le))
+  return [""]
 act (Execute le) = executeExpression le
+act (Diagram le) = drawDiagram False le
+act (SimpDiagram le) = drawDiagram True le
+act EmptyLine = return [""]
+act Error = return [errorUnknownCommand ++ "\n"]
+act Restart = put defaultEnv >> return [restartText ++ "\n"]
+act Help = return [helpText ++ "\n"]
+act (SetVerbose setting) = setOption setting changeVerbose "verbose: "
+act (SetColor setting) = setOption setting changeColor "color mode: "
+act (SetSki setting) = setOption setting changeSkioutput "ski mode: "
+act (SetTypes setting) = setOption setting changeTypes "types: "
+act (SetTopo setting) = setOption setting changeTopo "topology: "
+act (Ask func) = return $ askfor func
 
+
+-- | Asks for the name of a function.
+askfor :: String -> [String]
+askfor func = case stdquery func of
+  Nothing -> ["Error: the function '" ++ func ++ "' is not defined on the standard library.\n"]
+  Just f -> [description f ++ "\n", "Defined as: " ++ code f,"\n"]
+    
+
+-- | Sets the given option on/off.
+setOption :: Bool ->
+             (Environment -> Bool -> Environment) ->
+             String ->
+             State Environment [String]
+setOption setting change message = do
+  modify (`change` setting)
+  env <- get
+  return [messageenv env ++ "\n"]
+    where messageenv env =
+            (if getColor env then formatFormula else "") ++ message ++
+            (if setting then "on" else "off") ++ end
+
+drawDiagram :: Bool -> NamedLambda -> State Environment [String]
+drawDiagram wantsimplification le = do
+  env <- get
+  let bruijn = toBruijn (context env) le
+  let isopen = isOpenExp bruijn
+  let simpbruijn = simplifyAll bruijn
+  let maybediagram = gentzendiagram (if wantsimplification then simpbruijn else bruijn)
+
+  return $
+    if isopen then [errorUndefinedText ++ "\n"] else
+      case maybediagram of
+        Nothing -> [errorNonTypeableText ++ "\n"]
+        Just diagram -> map (++ "\n") . lines $ showProofTree diagram
+  
 -- | Executes a lambda expression. Given the context, returns the new
 -- context after the evaluation.
 executeExpression :: NamedLambda -> State Environment [String]
@@ -78,6 +151,8 @@
      let verbose = getVerbose env
      let completeexp = showCompleteExp env $ simplifyAll bruijn
      let isopen = isOpenExp bruijn
+     let coloring = getColor env
+     let decolorif = if coloring then id else decolor
      
      return $
        if isopen then [errorUndefinedText ++ "\n"] else
@@ -86,7 +161,7 @@
        if not verbose then [completeexp ++ "\n"] else
          [unlines $
            [show le] ++
-           [unlines $ map showReduction $ simplifySteps bruijn] ++
+           [unlines $ map (decolorif . showReduction) $ simplifySteps bruijn] ++
            [completeexp]
          ]
   
@@ -100,25 +175,22 @@
 -- | Shows an expression and the name that is bound to the expression
 -- in the current context
 showCompleteExp :: Environment -> Exp -> String
-showCompleteExp environment expr = let
-      lambdaname = show $ nameExp expr
-      skiname = if getSki environment
-                 then formatSubs2 ++ " ⇒ " ++ show (skiabs $ nameExp expr) ++ end
-                 else ""
-      inferredtype = typeinference expr
-      typename = if getTypes environment
-                  then formatType ++ " :: " ++ (case inferredtype of
-                                                   Just s -> if getTopo environment
-                                                             then show (Top s)
-                                                             else show s
-                                                   Nothing -> "Type error!") ++ end
-                  else ""
-      expName = case getExpressionName environment expr of
-                  Nothing -> ""
-                  Just exname -> formatName ++ " ⇒ " ++ exname ++ end
-  in
-      lambdaname ++ skiname ++ expName ++ typename ++ end
-    
+showCompleteExp environment expr = 
+  lambdaname ++ skiname ++ expName ++ typename ++ end
+  where
+    coloring = getColor environment
+    ifvoid b x = if b then x else ""
+    typesset = getTypes environment
+    skiset = getSki environment
+    lambdaname = show $ nameExp expr
+    skiname = ifvoid skiset $ formatSubs2 ++ " ⇒ " ++ show (skiabs $ nameExp expr) ++ end
+    inferredtype = case typeinference expr of
+                     Just s -> if getTopo environment then show (Top s) else show s
+                     Nothing -> "Type error!"
+    typename = ifvoid typesset $ ifvoid coloring formatType ++ " :: " ++ inferredtype ++ end
+    expName = case getExpressionName environment expr of
+                Just exname -> ifvoid coloring formatName ++ " ⇒ " ++ exname ++ end
+                Nothing -> ""
 
 
 -- Parsing of interpreter command line commands.
@@ -127,14 +199,7 @@
 interpreteractionParser = choice
   [ try interpretParser
   , try quitParser
-  , try restartParser
   , try loadParser
-  , try verboseParser
-  , try colorParser
-  , try skiOutputParser
-  , try typesParser
-  , try topoParser
-  , try helpParser
   ]
 
 -- | Parses a language action as an interpreter action.
@@ -143,16 +208,37 @@
 
 -- | Parses a language action.
 actionParser :: Parser Action
-actionParser = choice
-  [ try bindParser
-  , try evalbindParser
-  , try executeParser
-  , try commentParser
+actionParser = choice $ map try
+  [ simpdiagramParser
+  , diagramParser
+  , bindParser
+  , evalbindParser
+  , executeParser
+  , commentParser
+  , helpParser
+  , askParser
+  , restartParser
+  , verboseParser
+  , colorParser
+  , skiOutputParser
+  , typesParser
+  , topoParser
   ]
 
+
+-- | Parses a diagram request
+diagramParser :: Parser Action
+diagramParser = Diagram <$> (string "@ " >> lambdaexp)
+
+-- | Parses a simplfication and diagram request
+simpdiagramParser :: Parser Action
+simpdiagramParser = SimpDiagram <$> (string "@@ " >> lambdaexp)
+
 -- | Parses a binding between a variable an its representation.
 bindParser :: Parser Action
-bindParser = fmap Bind $ (,) <$> many1 alphaNum <*> (spaces >> string "!=" >> spaces >> lambdaexp)
+bindParser = fmap Bind $ (,) <$>
+  many1 alphaNum <*>
+  (spaces >> choice [try (string "!="), try (string ":=")] >> spaces >> lambdaexp)
 
 -- | Parses a binding and evaluation expression between a variable an its representation
 evalbindParser :: Parser Action
@@ -162,18 +248,22 @@
 executeParser :: Parser Action
 executeParser = Execute <$> lambdaexp
 
+-- | Parses a definition request to the interpreter.
+askParser :: Parser Action
+askParser = Ask <$> (string ":? " >> many1 alphaNum)
+
 -- | Parses comments.
 commentParser :: Parser Action
 commentParser = string "#" >> many anyChar >> return Comment
 
--- | Parses a "quit" command.
-quitParser, restartParser, helpParser :: Parser InterpreterAction
+quitParser :: Parser InterpreterAction
 quitParser    = string ":quit" >> return Quit
+restartParser, helpParser :: Parser Action
 restartParser = string ":restart" >> return Restart
 helpParser    = string ":help" >> return Help
 
 -- | Parses a change in a setting
-settingParser :: (Bool -> InterpreterAction) -> String -> Parser InterpreterAction
+settingParser :: (Bool -> Action) -> String -> Parser Action
 settingParser setSetting settingname = choice
   [ try settingonParser
   , try settingoffParser
@@ -183,7 +273,7 @@
     settingoffParser = string (settingname ++ " off") >> return (setSetting False)
 
 -- | Multiple setting parsers
-verboseParser, colorParser, skiOutputParser, typesParser, topoParser :: Parser InterpreterAction
+verboseParser, colorParser, skiOutputParser, typesParser, topoParser :: Parser Action
 verboseParser   = settingParser SetVerbose ":verbose"
 colorParser     = settingParser SetColor   ":color"
 skiOutputParser = settingParser SetSki     ":ski"
diff --git a/source/Lambda.hs b/source/Lambda.hs
--- a/source/Lambda.hs
+++ b/source/Lambda.hs
@@ -89,7 +89,7 @@
 -- Reductions of lambda expressions.
 
 -- | Applies repeated simplification to the expression until it stabilizes and
--- returns the final simplified expression.
+--   returns the final simplified expression.
 --
 -- >>> simplifyAll $ App (Lambda (Var 1)) (Lambda (Var 1))
 -- λ1
diff --git a/source/Libraries.hs b/source/Libraries.hs
new file mode 100644
--- /dev/null
+++ b/source/Libraries.hs
@@ -0,0 +1,106 @@
+module Libraries
+  ( stdlibraries
+  , stdmap
+  , stdquery
+  , code
+  , name
+  , description
+  )
+where
+
+import qualified Data.Map as M
+import Control.Arrow
+
+stdlibraries :: String
+stdlibraries = unlines $ map code stdfunctions
+
+stdquery :: String -> Maybe Function
+stdquery = flip M.lookup stdmap
+
+stdmap :: M.Map String Function
+stdmap = M.fromList $ map (name &&& id) stdfunctions
+
+data Function = Function
+  { name :: String
+  , code :: String
+  , description :: String
+  }
+  deriving (Show)
+
+stdfunctions :: [Function]
+stdfunctions = 
+  [ Function "id" "id = \\x.x" "Identity function. Returns its argument unchanged."
+  , Function "const" "const = \\x.\\y.x" "Binay function evaluating to its first argument."
+  , Function "compose" "compose = \\f.\\g.\\x.f (g x)" "Function composition."
+  , Function "true" "true = \\a.\\b.a" "Boolean 'true', using Church encoding."
+  , Function "false" "false = \\a.\\b.b" "Boolean 'false', using Church encoding."
+  , Function "and" "and = \\p.\\q.p q p" "Boolean conjunction."
+  , Function "or" "or = \\p.\\q.p p q" "Boolean disjunction."
+  , Function "not" "not = \\b.b false true" "Boolean negation."
+  , Function "implies" "implies = \\a.\\b.or (not a) b" "Boolean implication."
+  , Function "ifelse" "ifelse = (\\x.x)" "Identity function, can be used as a boolean case analysis."
+  , Function "succ" "succ = \\n.\\f.\\x.f (n f x)" "Return the successor of a natural number."
+  , Function "0" "0 = \\f.\\x.x" "The natural number 0, using Church encoding."
+  , Function "plus" "plus = \\m.\\n.\\f.\\x.m f (n f x)" "Adds two natural numbers."
+  , Function "mult" "mult = \\m.\\n.\\f.\\x.m (n f) x" "Multiplies two natural numbers."
+  , Function "pred" "pred = \\n.\\f.\\x.n (\\g.(\\h.h (g f))) (\\u.x) (\\u.u)" "Predecessor of a natural number"
+  , Function "minus" "minus = \\m.\\n.(n pred) m" "Substracts two natural numbers"
+  , Function "iszero" "iszero = \\n.(n (\\x.false) true)" "Returns true if the natural number is zero."
+  , Function "leq" "leq = \\m.\\n.(iszero (minus m n))" "Returns true if the first argument is a natural number lesser or equal than the second."
+  , Function "geq" "geq = \\m.\\n.(iszero (minus n m))" "Returns true if the first argument is a natural number greater or equal than the second."
+  , Function "lt" "lt = \\m.\\n.not (geq m n)" "Returns true if the first argument is a natural number lesser than the second."
+  , Function "gt" "gt = \\m.\\n.not (leq m n)" "Returns true if the first argument is a natural number greater than the second."
+  , Function "eq" "eq = \\m.\\n.(and (leq m n) (leq n m))" "Returns true if the two natural numbers are equal."
+  , Function "S" "S = \\x.\\y.\\z. x z (y z)" "S combinator. Substitution operator."
+  , Function "K" "K = \\x.\\y.x" "K combinator. Constant operator."
+  , Function "I" "I = S K K" "I combinator. Identity operator."
+  , Function "C" "C = \\f.\\x.\\y.f y x" "C combinator."
+  , Function "B" "B = \\f.\\g.\\x.f (g x)" "B combinator."
+  , Function "W" "W = \\x.\\y.(y y)" "W combinator."
+  , Function "Y" "Y != \\f.(\\x.f (x x))(\\x.f (x x))" "Y combinator. Fixed-point combinator."
+  , Function "tuple" "tuple = \\x.\\y.\\z.z x y" "Untyped tuple constructor. Takes a and b and returns the tuple (a,b)."
+  , Function "first" "first = \\p.p true" "Untyped tuple projection. Returns the first element of a tuple."
+  , Function "second" "second = \\p.p false" "Untyped tuple projection. Returns the second element of a tuple."
+  , Function "cons" "cons = \\h.\\t.\\c.\\n.(c h (t c n))" "List constructor. Appends an element to the head of the list."
+  , Function "nil" "nil = \\c.\\n.n" "List constructor. Creates the empty list."
+  , Function "foldr" "foldr = \\o.\\n.\\l.(l o n)" "List folding. Combines the elements of the list using a binary operation."
+  , Function "fold" "fold = \\o.\\n.\\l.(l o n)" "List folding. Combines the elements of the list using a binary operation."
+  , Function "head" "head = fold const nil" "Returns the head of a list."
+  , Function "tail" "tail = \\l.first (l (\\a.\\b.tuple (second b) (cons a (second b))) (tuple nil nil))" "Extracts the head of a list."
+  , Function "take" "take = \\n.\\l.first (n (\\t.tuple (cons (head (second t)) (first t)) (tail (second t))) (tuple nil l))" "Extracts all the elements except the head of a list"
+  , Function "sum" "sum = (foldr plus 0)" "Adds a list of natural numbers."
+  , Function "prod" "prod = (foldr mult (succ 0))" "Multiplies a list of natural numbers."
+  , Function "length" "length = (foldr (\\h.\\t.succ t) 0)" "Returns the length of a list."
+  , Function "map" "map = (\\f.(foldr (\\h.\\t.cons (f h) t) nil))" "Maps a function over a list. Returns a list obtained by applying the function to each element of the original list."
+  , Function "filter" "filter = \\p.(foldr (\\h.\\t.((p h) (cons h t) t)) nil)" "Filters a list with a predicate. Returns a list containing only the elements that satisfy the predicate."
+  , Function "node" "node = \\x.\\l.\\r.\\f.\\n.(f x (l f n) (r f n))" "Binary tree constructor. Creates a tree whose root is given by the first argument and whose left and right subtrees are given by the second and third arguments, respectively."
+  , Function "omega" "omega := (\\x.(x x))(\\x.(x x))" "Omega combinator. An example of a non-reducible lambda calculus expression."
+  , Function "fix" "fix := (\\f.(\\x.f (x x)) (\\x.f (x x)))" "Fixed-point combinator. Given f, returns an element x such that f x = x."
+  , Function "fact" "fact := fix (\\f.\\n.iszero n (succ 0) (mult n (f (pred n))))" "Factorial of a natural number."
+  , Function "fib" "fib := fix (\\f.\\n.iszero n (succ 0) (plus (f (pred n)) (f (pred (pred n)))))" "Returns the n-th Fibonacci number."
+  , Function "naturals" "naturals := fix (compose (cons 0) (map (plus 1)))" "Infinite list of the natural numbers."
+  , Function "infinity" "infinity := fix succ" "Fixed point of the successor function on the natural numbers."
+  , Function "division" "division := fix (\\d.\\q.\\a.\\b. lt a b (tuple q a) (d (succ q) (minus a b) b)) 0" "Integer division between natural numbers. Returns the quotient and the modulo."
+  , Function "mu" "mu := \\p.fix (\\f.\\n.(p n) n (f (succ n))) 0" "Göedel mu-operator. Finds the first natural number satisfying a certain predicate."
+  , Function "div" "div := \\a.\\b.first (division a b)" "Quotient of the division between two natural numbers."
+  , Function "mod" "mod := \\a.\\b.second (division a b)" "Modulo of the division between two natural numbers."
+  , Function "pair" "pair = \\x.\\y.(x,y)" "Pair constructor of the simply-typed lambda calculus."
+  , Function "fst" "fst = \\x.FST x" "First projection of a typed pair."
+  , Function "snd" "snd = \\x.SND x" "Second projection of a typed pair."
+  , Function "inl" "inl = \\x.INL x" "First injection of a typed sum."
+  , Function "inr" "inr = \\x.INR x" "Second injection of a typed sum."
+  , Function "caseof" "caseof = \\x.\\y.\\z.CASE x OF (\\a.y a);(\\a.z a)" "Case analysis of a sum type."
+  , Function "unit" "unit = UNIT" "The only element of the unit type."
+  , Function "abort" "abort = \\x.ABORT x" "Takes an element of the empty type and creates an element of any given type."
+  , Function "absurd" "absurd = \\x.ABSURD x" "Takes an element of the empty type and creates an element of any given type."
+  ] ++ natsdef
+  where
+    fnat :: Int -> Function
+    fnat n = Function
+      (show (n+1))
+      (show (n+1) ++ " = succ " ++ show n)
+      ("The natural number " ++ show (n+1) ++ ", using Church encoding.")
+    
+    natsdef :: [Function]
+    natsdef = map fnat [0..999]
+     
diff --git a/source/Main.hs b/source/Main.hs
--- a/source/Main.hs
+++ b/source/Main.hs
@@ -4,6 +4,7 @@
 import           Control.Monad.State
 import           Control.Exception
 import           Data.List
+import           Data.Foldable (forM_)
 import           System.Directory
 import           System.Console.Haskeline
 import           Text.ParserCombinators.Parsec hiding (try)
@@ -13,7 +14,7 @@
 import           Options hiding (defaultOptions)
 
 
--- Lambda interpreter
+-- Lambda interpreter.
 -- The actions of the interpreter are written here. It allows to execute normal
 -- actions (bindings and evaluation), and interpreter specific actions, as "quit"
 -- or "load".
@@ -22,19 +23,23 @@
 -- | Runs the interpreter with default settings and an empty context.
 main :: IO ()
 main =
-  -- 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
-  -- Reads the flags
-   ->
-    if flagVersion opts
-      then putStrLn versionText
-      else case args of
+  -- Uses the Options library, which requires the program to start
+  -- with runCommand. The command-line flags are stored in opts and
+  -- other command line arguments are stored in args.
+  runCommand $ \opts args -> do
+  -- Reads the libaries flag. If activated, it will not automatically
+  -- load the libraries.
+  let initialEnv = if flagLibs opts then defaultEnv else librariesEnv
+  -- Reads the rest of the flags. The --version flag shows the current
+  -- version of the interpreter. An optional argument may be used to
+  -- indicate a file to load.
+  if flagVersion opts
+  then putStrLn versionText
+  else case args of
              [] ->
                runInputT
                  defaultSettings
-                 (outputStrLn initialText >> interpreterLoop defaultEnv)
+                 (outputStrLn initialText >> interpreterLoop initialEnv)
              [filename] -> executeFile filename
              _ -> putStrLn "Wrong number of arguments"
 
@@ -47,68 +52,59 @@
   let interpreteraction =
         case minput of
           Nothing -> Quit
-          Just "" -> EmptyLine
+          Just "" -> Interpret EmptyLine
           Just input ->
-            case parse interpreteractionParser "" input of
-              Left _ -> Error
+            case parse interpreteractionParser "" (preformat input) of
+              Left  _ -> Interpret 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
+
+  newenvironment <- executeAction environment interpreteraction
+  forM_ newenvironment interpreterLoop
+              
+
+-- | Executes the parsed action, every action may affect the context
+-- in a way, and returns the control to the interpreter.
+executeAction :: Environment -> InterpreterAction -> InputT IO (Maybe Environment)
+executeAction environment interpreteraction = 
+  case interpreteraction of
     -- Interprets an action
-        of
     Interpret action ->
       case runState (act action) environment of
         (output, newenv) -> do
           outputActions newenv output
-          interpreterLoop newenv
+          return $ Just 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])
-      files <- lift $ mapM findFilename modules
-      -- Concats all the module contents
-      maybeactions <- fmap concat . sequence <$> lift (mapM loadFile files)
-      case maybeactions of
+      readallmoduledeps <- lift $ readAllModuleDepsRecursively [modulename]
+      case readallmoduledeps 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
-    -- Ignores the empty line
-    EmptyLine -> interpreterLoop environment
+          outputStrLn errorNotFoundText
+          return $ Just environment
+        Just readallmodules -> do
+          let modules = nub readallmodules
+          files <- lift $ mapM findFilename modules
+          -- Concats all the module contents
+          case sequence files of
+            Nothing -> do
+              outputStrLn errorNotFoundText
+              return $ Just environment
+            Just allfiles -> do
+              maybeactions <- fmap concat . sequence <$> lift (mapM loadFile allfiles)
+              case maybeactions of
+                Nothing -> do
+                  outputStrLn "Error loading file"
+                  return $ Just environment
+                Just actions ->
+                  case runState (multipleAct actions) environment of
+                    (output, newenv) -> do
+                      outputActions newenv output
+                      return $ Just newenv
     -- Exits the interpreter
-    Quit -> return ()
-    -- Restarts the interpreter context
-    Restart -> outputStrLn restartText >> interpreterLoop defaultEnv
-    -- Unknown command
-    Error -> outputStrLn errorUnknownCommand >> interpreterLoop environment
-    -- Sets the verbose option
-    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
+    Quit -> return Nothing
 
 
--- | 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,
 --   formats and prints them in console.
 outputActions :: Environment -> [String] -> InputT IO ()
@@ -127,14 +123,14 @@
 -- Loading and reading files
 -- | Loads the given filename and returns the complete list of actions.
 --   Returns Nothing if there is an error reading or parsing the file.
-loadFile :: String -> IO (Maybe [Action])
+loadFile :: Filename -> IO (Maybe [Action])
 loadFile filename = do
   putStrLn $ formatLoading ++ "Loading " ++ filename ++ "..." ++ end
   input <- try $ readFile filename :: IO (Either IOException String)
   case input of
     Left _ -> return Nothing
     Right inputs -> do
-      let parsing = map (parse actionParser "") $ filter (/="") $ lines inputs
+      let parsing = map (parse actionParser "" . preformat) . filter (/="") . lines $ inputs
       let actions = map (\x -> case x of
                                  Left _  -> Nothing
                                  Right a -> Just a) parsing
@@ -149,11 +145,7 @@
     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
-
+        (outputs, _) -> mapM_ putStr outputs
 
 -- | Reads module dependencies
 readFileDependencies :: Filename -> IO [Modulename]
@@ -164,43 +156,51 @@
     Right inputs -> return $
       map (drop 9) (filter (isPrefixOf "#INCLUDE ") $ filter (/="") $ lines inputs)
 
--- | Reads all the dependencies from a module list
-readAllModuleDeps :: [Modulename] -> IO [Modulename]
+-- | Reads all the dependencies from a module list.
+--   Returns an error if a dependency cannot be found
+readAllModuleDeps :: [Modulename] -> IO (Maybe [Modulename])
 readAllModuleDeps modulenames = do
   files <- mapM findFilename modulenames
-  deps <- mapM readFileDependencies files
-  return $ concat deps
+  deps <- mapM (mapM readFileDependencies) files
+  return (concat <$> sequence deps)
 
--- | Read module dependencies recursively
-readAllModuleDepsRecursively :: [Modulename] -> IO [Modulename]
+-- | Read module dependencies recursively.
+--   Returns an error if a dependency cannot be found
+readAllModuleDepsRecursively :: [Modulename] -> IO (Maybe [Modulename])
 readAllModuleDepsRecursively modulenames = do
-  newmodulenames <- readAllModuleDeps modulenames
-  let allmodulenames = nub (newmodulenames ++ modulenames)
-  if modulenames == allmodulenames
-    then return modulenames
-    else readAllModuleDepsRecursively allmodulenames
+  maybenewmodulenames <- readAllModuleDeps modulenames
+  case maybenewmodulenames of
+    Nothing -> return Nothing
+    Just newmodulenames -> do
+      let allmodulenames = nub (newmodulenames ++ modulenames)
+      if modulenames == allmodulenames
+      then return (Just modulenames)
+      else readAllModuleDepsRecursively allmodulenames
 
 -- | Given a module name, returns the filename associated with it
-findFilename :: Modulename -> IO Filename
+findFilename :: Modulename -> IO (Maybe Filename)
 findFilename s = do
   appdir <- getAppUserDataDirectory "mikrokosmos"
   homedir <- getHomeDirectory
 
   -- Looks for the module in the common locations
-  head <$> filterM doesFileExist
+  headMaybe <$> filterM doesFileExist
     [ "lib/" ++ s ++ ".mkr"
     , "./" ++ s ++ ".mkr"
     , appdir ++ "/" ++ s ++ ".mkr"
     , homedir ++ "/" ++ s ++ ".mkr"
     , "/usr/lib/mikrokosmos/" ++ s ++ ".mkr"
     ]
+  where
+    headMaybe [] = Nothing
+    headMaybe (x:_) = Just x
 
 
--- Flags
 -- | Flags datatype
 data MainFlags = MainFlags
   { flagExec :: String
   , flagVersion :: Bool
+  , flagLibs :: Bool
   }
 
 instance Options MainFlags where
@@ -208,3 +208,4 @@
   defineOptions = pure MainFlags
     <*> simpleOption "exec"    ""    "A file to execute and show its results"
     <*> simpleOption "version" False "Show program version"
+    <*> simpleOption "no-libs" False "Runs mikrokosmos without standard libraries"
diff --git a/source/NamedLambda.hs b/source/NamedLambda.hs
--- a/source/NamedLambda.hs
+++ b/source/NamedLambda.hs
@@ -15,6 +15,8 @@
   , lambdaexp
   , toBruijn
   , nameExp
+  , quicknameIndexes
+  , variableNames
   )
 where
 
@@ -91,6 +93,9 @@
 nameParser :: Parser String
 nameParser = many1 alphaNum
 
+choicest :: [String] -> Parser String
+choicest sl = choice (try . string <$> sl)
+
 -- | Parses a lambda abstraction. The '\' is used as lambda. 
 lambdaAbstractionParser :: Parser NamedLambda
 lambdaAbstractionParser = LambdaAbstraction <$>
@@ -104,47 +109,92 @@
 pairParser = parens (TypedPair <$> lambdaexp <*> (char ',' >> lambdaexp))
 
 pi1Parser, pi2Parser :: Parser NamedLambda
-pi1Parser = TypedPi1 <$> (string "FST " >> lambdaexp)
-pi2Parser = TypedPi2 <$> (string "SND " >> lambdaexp)
+pi1Parser = TypedPi1 <$> (choicest namesPi1 >> lambdaexp)
+pi2Parser = TypedPi2 <$> (choicest namesPi2 >> lambdaexp)
 
 inlParser, inrParser :: Parser NamedLambda
-inlParser = TypedInl <$> (string "INL " >> lambdaexp)
-inrParser = TypedInr <$> (string "INR " >> lambdaexp)
+inlParser = TypedInl <$> (choicest namesInl >> lambdaexp)
+inrParser = TypedInr <$> (choicest namesInr >> lambdaexp)
 
 caseParser :: Parser NamedLambda
-caseParser = TypedCase <$> (string "CASE " >> simpleexp) <*> (string " OF " >> simpleexp) <*> (string ";" >> simpleexp)
+caseParser =
+  TypedCase <$>
+  (choicest namesCase >> simpleexp) <*>
+  (choicest namesOf >> simpleexp) <*>
+  (choicest namesCaseSep >> simpleexp)
 
 unitParser :: Parser NamedLambda
-unitParser = string "UNIT" >> return TypedUnit
+unitParser = choicest namesUnit >> return TypedUnit
 
 abortParser :: Parser NamedLambda
-abortParser = TypedAbort <$> (string "ABORT " >> lambdaexp)
+abortParser = TypedAbort <$> (choicest namesAbort >> lambdaexp)
 
 absurdParser :: Parser NamedLambda
-absurdParser = TypedAbsurd <$> (string "ABSURD " >> lambdaexp)
+absurdParser = TypedAbsurd <$> (choicest namesAbsurd >> lambdaexp)
 
 -- | Shows a lambda expression with named variables.
 -- Parentheses are ignored; they are written only around applications.
 showNamedLambda :: NamedLambda -> String
-showNamedLambda (LambdaVariable c)      = c
-showNamedLambda (LambdaAbstraction c e) = "λ" ++ c ++ "." ++ showNamedLambda e ++ ""
-showNamedLambda (LambdaApplication f g) = "(" ++ showNamedLambda f ++ " " ++ showNamedLambda g ++ ")"
-showNamedLambda (TypedPair a b)         = "(" ++ showNamedLambda a ++ "," ++ showNamedLambda b ++ ")"
-showNamedLambda (TypedPi1 a)            = "(" ++ "FST " ++ showNamedLambda a ++ ")"
-showNamedLambda (TypedPi2 a)            = "(" ++ "SND " ++ showNamedLambda a ++ ")"
-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 (TypedAbort a)          = "(" ++ "ABORT " ++ showNamedLambda a ++ ")"
-showNamedLambda (TypedAbsurd a)          = "(" ++ "ABSURD " ++ showNamedLambda a ++ ")"
+showNamedLambda (LambdaVariable c) = c
+showNamedLambda (LambdaAbstraction c e) = "λ" ++ c ++ "." ++ showNamedLambda e
+showNamedLambda (LambdaApplication f g) =
+  showNamedLambdaPar f ++ " " ++ showNamedLambdaPar g
+showNamedLambda (TypedPair a b) =
+  "(" ++ showNamedLambda a ++ "," ++ showNamedLambda b ++ ")"
+showNamedLambda (TypedPi1 a) = head namesPi1 ++ showNamedLambdaPar a
+showNamedLambda (TypedPi2 a) = head namesPi2 ++ showNamedLambdaPar a
+showNamedLambda (TypedInl a) = head namesInl ++ showNamedLambdaPar a
+showNamedLambda (TypedInr a) = head namesInr ++ showNamedLambdaPar a
+showNamedLambda (TypedCase a b c) =
+  last namesCase ++
+  showNamedLambda a ++
+  last namesOf ++ showNamedLambda b ++ head namesCaseSep ++ showNamedLambda c
+showNamedLambda TypedUnit = head namesUnit
+showNamedLambda (TypedAbort a) = head namesAbort ++ showNamedLambdaPar a
+showNamedLambda (TypedAbsurd a) = head namesAbsurd ++ showNamedLambdaPar a
 
+showNamedLambdaPar :: NamedLambda -> String
+showNamedLambdaPar l@(LambdaVariable _) = showNamedLambda l
+showNamedLambdaPar l@TypedUnit = showNamedLambda l
+showNamedLambdaPar l@(TypedPair _ _) = showNamedLambda l
+showNamedLambdaPar l = "(" ++ showNamedLambda l ++ ")"
+
 instance Show NamedLambda where
   show = showNamedLambda
 
 
+-- Name type constructors
+namesPi1 :: [String]
+namesPi1 = ["π₁ ", "FST "]
 
+namesPi2 :: [String]
+namesPi2 = ["π₂ ", "SND "]
 
+namesInl :: [String]
+namesInl = ["ιnl ", "INL "]
+
+namesInr :: [String]
+namesInr = ["ιnr ", "INR "]
+
+namesCase :: [String]
+namesCase = ["CASE ", "Case ", "ᴄᴀꜱᴇ "]
+
+namesOf :: [String]
+namesOf = [" OF ", " Of ", " ᴏꜰ "]
+
+namesCaseSep :: [String]
+namesCaseSep = ["; ", ";"]
+
+namesUnit :: [String]
+namesUnit = ["★", "UNIT"]
+
+namesAbort :: [String]
+namesAbort = ["□ ", "ABORT "]
+
+namesAbsurd :: [String]
+namesAbsurd = ["■ ", "ABSURD "]
+
+
 -- | Translates a named variable expression into a DeBruijn one.
 -- Uses a dictionary of already binded numbers and variables.
 tobruijn :: Map.Map String Integer -- ^ dictionary of the names of the variables used
@@ -195,9 +245,25 @@
 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)
+
+
+quicknameIndexes :: Int -> [String] -> Exp -> NamedLambda
+quicknameIndexes _ _  (Var 0)          = LambdaVariable "undefined"
+quicknameIndexes n vars   (Var m)      = LambdaVariable (vars !! (n - fromInteger m))
+quicknameIndexes n vars (Lambda e)     = LambdaAbstraction (vars !! n) (quicknameIndexes (succ n) vars e)
+quicknameIndexes n vars (App f g)      = LambdaApplication (quicknameIndexes n vars f) (quicknameIndexes n vars g)
+quicknameIndexes n vars (Pair a b)     = TypedPair (quicknameIndexes n vars a) (quicknameIndexes n vars b)
+quicknameIndexes n vars (Pi1 a)        = TypedPi1 (quicknameIndexes n vars a)
+quicknameIndexes n vars (Pi2 a)        = TypedPi2 (quicknameIndexes n vars a)
+quicknameIndexes n vars (Inl a)        = TypedInl (quicknameIndexes n vars a)
+quicknameIndexes n vars (Inr a)        = TypedInr (quicknameIndexes n vars a)
+quicknameIndexes n vars (Caseof a b c) = TypedCase (quicknameIndexes n vars a) (quicknameIndexes n vars b) (quicknameIndexes n vars c)
+quicknameIndexes _ _   Unit            = TypedUnit
+quicknameIndexes n vars (Abort a)      = TypedAbort (quicknameIndexes n vars a)
+quicknameIndexes n vars (Absurd a)     = TypedAbsurd (quicknameIndexes n vars 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
@@ -45,21 +45,21 @@
 showski (Comb x (Cte c)) = showski x ++ showski (Cte c)
 showski (Comb x (Comb u v)) = showski x ++ "(" ++ showski (Comb u v) ++ ")"
 showski (Comb x a) = showski x ++ showski a
-showski (Spair) = "[PAIR]"
-showski (Spi1) = "[FST]"
-showski (Spi2) = "[SND]"
-showski (Sinl) = "[INL]"
-showski (Sinr) = "[INR]"
-showski (Scase) = "[CASEOF]"
-showski (Sunit) = "[UNIT]"
-showski (Sabort) = "[ABORT]"
-showski (Sabsurd) = "[ABSURD]"
+showski Spair = "[PAIR]"
+showski Spi1 = "[FST]"
+showski Spi2 = "[SND]"
+showski Sinl = "[INL]"
+showski Sinr = "[INR]"
+showski Scase = "[CASEOF]"
+showski Sunit = "[UNIT]"
+showski Sabort = "[ABORT]"
+showski Sabsurd = "[ABSURD]"
 
 -- | SKI abstraction of a named lambda term. From a lambda expression
 -- creates a SKI equivalent expression. The following algorithm is a
 -- version of the algorithm 9.10 on the Hindley-Seldin book.
 skiabs :: NamedLambda -> Ski
-skiabs (LambdaVariable x) = Cte x
+skiabs (LambdaVariable x)      = Cte x
 skiabs (LambdaApplication m n) = Comb (skiabs m) (skiabs n)
 skiabs (LambdaAbstraction x m) = bracketabs x (skiabs m)
 skiabs (TypedPair a b) = Comb (Comb Spair (skiabs a)) (skiabs b)
@@ -68,7 +68,7 @@
 skiabs (TypedInl a) = Comb Sinl (skiabs a)
 skiabs (TypedInr a) = Comb Sinr (skiabs a)
 skiabs (TypedCase a b c) = Comb (Comb (Comb Scase (skiabs a)) (skiabs b)) (skiabs c)
-skiabs (TypedUnit) = Sunit
+skiabs TypedUnit = Sunit
 skiabs (TypedAbort a) = Comb Sabort (skiabs a)
 skiabs (TypedAbsurd a) = Comb Sabsurd (skiabs a)
 
@@ -82,9 +82,9 @@
   | freein x u           = Comb K (Comb u (Cte y))
   | otherwise            = Comb (Comb S (bracketabs x u)) (bracketabs x (Cte y))
 bracketabs x (Comb u v)
-  | freein x (Comb u v) = Comb K (Comb u v)
-  | otherwise           = Comb (Comb S (bracketabs x u)) (bracketabs x v)
-bracketabs _ a = Comb K a
+  | freein x (Comb u v)  = Comb K (Comb u v)
+  | otherwise            = Comb (Comb S (bracketabs x u)) (bracketabs x v)
+bracketabs _ a           = Comb K a
 
 -- | Checks if a given variable is used on a SKI expression.
 freein :: String -> Ski -> Bool
diff --git a/source/Stlc/Block.hs b/source/Stlc/Block.hs
new file mode 100644
--- /dev/null
+++ b/source/Stlc/Block.hs
@@ -0,0 +1,87 @@
+module Stlc.Block
+  ( Block
+  , textBlock
+  , deductionBlock
+  , box
+  )
+where 
+
+import Data.Monoid
+
+newtype Block = Block { getBlock :: [String] }
+  deriving (Eq, Ord)
+
+instance Monoid Block where
+  mappend = joinBlocks
+  mempty  = Block [[]]
+
+instance Show Block where
+  show = unlines . getBlock
+
+
+hsepChar :: Char
+hsepChar = '─'
+
+spaceChar :: Char
+spaceChar = ' '
+
+height :: Block -> Int
+height = length . getBlock
+
+width :: Block -> Int
+width (Block [])    = 0
+width (Block (x:_)) = length x
+
+-- | Horizontal join
+joinBlocks :: Block -> Block -> Block
+joinBlocks u@(Block a) v@(Block b) = Block $ zipWith (++) us vs
+  where
+    us = replicate (mh - uh) (replicate uw spaceChar) ++ a
+    vs = replicate (mh - vh) (replicate vw spaceChar) ++ b
+    uh = height u
+    vh = height v
+    mh = max uh vh
+    uw = width u
+    vw = width v
+
+-- | Vertical join
+stackBlocks :: String -> Block -> Block -> Block
+stackBlocks label u v = Block $ getBlock ut ++ [hline] ++ getBlock vt
+  where
+    mw = max (width u) (width v)
+    us = centerBlock mw u
+    vs = centerBlock mw v
+    hline = replicate mw hsepChar ++ label
+    ut = us <> Block [replicate (length label) ' ']
+    vt = vs <> Block [replicate (length label) ' ']
+
+
+centerBlock :: Int -> Block -> Block
+centerBlock n = Block . map (centerString n) . getBlock
+
+centerString :: Int -> String -> String
+centerString n s = centered
+  where
+    w = length s
+    diff = n - w
+    semicentered = replicate (diff `div` 2 + diff `mod` 2) ' ' ++ s
+    centered = take n (semicentered ++ repeat ' ')
+
+-- | Inserts a text into a text block
+textBlock :: String -> Block
+textBlock s = Block [centerString (length s) s]
+
+-- | Draws a logical inference in a text block
+deductionBlock :: Block -> String -> [Block] -> Block
+deductionBlock inference label blocks = stackBlocks label top inference
+  where
+    top = if not (null blocks)
+          then foldr1 (\x y -> x <> Block ["   "] <> y) blocks
+          else Block [""]
+
+-- | Draws a box around a text block
+box :: Block -> Block
+box c@(Block cm) = Block $
+  ["╭" ++ replicate (width c) '─' ++ "╮"] ++
+  map (" " ++) cm                  ++
+  ["╰" ++ replicate (width c) '─' ++ "╯"]
diff --git a/source/Stlc/Gentzen.hs b/source/Stlc/Gentzen.hs
new file mode 100644
--- /dev/null
+++ b/source/Stlc/Gentzen.hs
@@ -0,0 +1,188 @@
+module Stlc.Gentzen
+  ( gentzendiagram
+  , showProofTree
+  )
+where
+
+import Stlc.Types
+import Stlc.Block
+import Lambda
+import NamedLambda
+import Data.Bifunctor
+import qualified Data.Map as Map
+
+
+data ProofTree a l = Inference a | Deduction a l [ProofTree a l]
+
+instance Bifunctor ProofTree where
+  bimap f _ (Inference a)      = Inference (f a)
+  bimap f g (Deduction a l ps) = Deduction (f a) (g l) (map (bimap f g) ps)
+
+proofBlock :: ProofTree String String -> Block
+proofBlock (Inference x)      = textBlock x
+proofBlock (Deduction x l xs) = deductionBlock (textBlock x) l (map proofBlock xs)
+
+-- | Draws a complete derivation tree
+showProofTree :: ProofTree String String -> String
+showProofTree = show . box . proofBlock
+
+
+data Label = Lponens | Labs | Lpair | Lpi1 | Lpi2
+           | Linr | Linl | Lcase | Lunit | Labort | Labsurd
+           
+instance Show Label where
+  show Lponens = "(→)"
+  show Labs = "(λ)"
+  show Lpair = "(,)"
+  show Lpi1 = "(π₁)"
+  show Lpi2 = "(π₂)"
+  show Linl = "(ιnl)"
+  show Linr = "(ιnr)"
+  show Lcase = "(Case)"
+  show Lunit = "(★)"
+  show Labort = "(□)"
+  show Labsurd = "(■)"
+
+type Depth = Int
+type TermDiagram = (Exp,Depth,Type)
+
+
+-- | Gets a type derivation diagram of the term.
+-- It fails if the term is non-typeable.
+gentzendiagram :: Exp -> Maybe (ProofTree String String)
+gentzendiagram l = do
+  (_, d)   <- typeinfer' variables 0 emptyctx l (Tvar 0)
+  maintype <- typeinfer variables emptyctx l (Tvar 0) <*> pure (Tvar 0)
+  let (normtemplate, _) = normalizeTemplate Map.empty 0 maintype
+  return (bimap (showTermDiagram normtemplate) show d)
+  where
+    showTermDiagram normtemplate (expl, depth, t) =
+      show (quicknameIndexes depth variableNames expl) ++
+      " ∷ " ++
+      show (applynormalization normtemplate t)
+
+-- | Type inference algorithm. Infers a type from a given context and expression
+-- with a set of constraints represented by a unifier type. The result type must
+-- be unifiable with this given type.
+-- Generalized version.
+typeinfer' :: [Variable] -- ^ List of fresh variables
+          -> Depth       -- ^ Lambda abstraction depth
+          -> Context     -- ^ Type context
+          -> Exp         -- ^ Lambda expression whose type has to be inferred
+          -> Type        -- ^ Constraint
+          -> Maybe (Substitution, ProofTree TermDiagram Label)
+          
+typeinfer' []  _ _ _ _ = Nothing
+typeinfer' [_] _ _ _ _ = Nothing
+
+typeinfer' _ depth ctx l@(Var n) b
+   | Map.member n ctx = do
+       var <- Map.lookup n ctx
+       ss <- unify var b
+       return (ss, Inference (l, depth, ss b))
+   | otherwise  = Nothing
+
+typeinfer' (x:vars) depth ctx l@(App p q) b = do
+  (sigma, d1) <- typeinfer' (evens vars) depth ctx                  p (Arrow (Tvar x) b)
+  (tau,   d2) <- typeinfer' (odds  vars) depth (applyctx sigma ctx) q (sigma (Tvar x))
+  let ss = tau . sigma
+  let fulld1 = bimap (\(d1e,d1d,d1t) -> (d1e,d1d,tau d1t)) id d1
+  return (ss, Deduction (l, depth, ss b) Lponens [fulld1,d2])
+  where
+    odds [] = []
+    odds [_] = []
+    odds (_:e:xs) = e : odds xs
+    evens [] = []
+    evens [e] = [e]
+    evens (e:_:xs) = e : evens xs
+
+
+typeinfer' (a:x:vars) depth ctx l@(Lambda p) b = do
+  sigma <- unify b (Arrow (Tvar a) (Tvar x))
+  let nctx = applyctx sigma (Map.insert 1 (sigma $ Tvar a) (incrementindices ctx))
+  (tau, d2) <- typeinfer' vars (succ depth) nctx p (sigma $ Tvar x)
+  let ss = tau . sigma
+  return (ss, Deduction (l, depth, ss b) Labs [d2])
+
+typeinfer' (x:y:vars) depth ctx l@(Pair m n) a = do
+  sigma <- unify a (Times (Tvar x) (Tvar y))
+  (tau, d1) <- typeinfer' (evens vars) depth (applyctx sigma         ctx) m (sigma (Tvar x))
+  (rho, d2) <- typeinfer' (odds  vars) depth (applyctx (tau . sigma) ctx) n (tau (sigma (Tvar y)))
+  let ss = rho . tau . sigma
+  let fulld1 = bimap (\(d1e,d1d,d1t) -> (d1e,d1d,rho d1t)) id d1
+  return (ss, Deduction (l, depth, ss a) Lpair [fulld1,d2])
+  where
+    odds [] = []
+    odds [_] = []
+    odds (_:e:xs) = e : odds xs
+    evens [] = []
+    evens [e] = [e]
+    evens (e:_:xs) = e : evens xs
+
+
+typeinfer' (y:vars) depth ctx l@(Pi1 m) a = do
+  (sigma, d1) <- typeinfer' vars depth ctx m (Times a (Tvar y))
+  let ss = sigma
+  return (ss, Deduction (l, depth, ss a) Lpi1 [d1])
+  
+typeinfer' (x:vars) depth ctx l@(Pi2 m) b = do
+  (sigma, d1) <- typeinfer' vars depth ctx m (Times (Tvar x) b)
+  let ss = sigma
+  return (ss, Deduction (l, depth, ss b) Lpi2 [d1])
+
+typeinfer' (x:y:vars) depth ctx l@(Inl m) a = do
+  sigma <- unify a (Union (Tvar x) (Tvar y))
+  (tau, d1) <- typeinfer' vars depth (applyctx sigma ctx) m (sigma (Tvar x))
+  let ss = tau . sigma
+  return (ss, Deduction (l, depth, ss a) Linl [d1])
+
+typeinfer' (x:y:vars) depth ctx l@(Inr m) a = do
+  sigma <- unify a (Union (Tvar x) (Tvar y))
+  (tau, d1) <- typeinfer' vars depth (applyctx sigma ctx) m (sigma (Tvar y))
+  let ss = tau . sigma
+  return (ss, Deduction (l, depth, ss a) Linr [d1])
+
+typeinfer' (x:y:vars) depth ctx l@(Caseof m f g) a = do
+  (sigma, d1) <- typeinfer' (third1 vars) depth ctx                          f (Arrow (Tvar x) a)
+  (tau,   d2) <- typeinfer' (third2 vars) depth (applyctx sigma ctx)         g (Arrow (sigma $ Tvar y) (sigma a))
+  (rho,   d3) <- typeinfer' (third3 vars) depth (applyctx (tau . sigma) ctx) m (Union (tau . sigma $ Tvar x) (tau . sigma $ Tvar y))
+  let ss = rho . tau . sigma
+  let fulld1 = bimap (\(d1e,d1d,d1t) -> (d1e,d1d,(rho . tau) d1t)) id d1
+  let fulld2 = bimap (\(d2e,d2d,d2t) -> (d2e,d2d,rho d2t)) id d2
+  -- Pruning the tree to make it match the natural deduction case rule
+  case fulld1 of
+    Deduction _ Labs [reald1] ->
+      case fulld2 of
+        Deduction _ Labs [reald2] -> return (ss, Deduction (l, depth, ss a) Lcase [reald1,reald2,d3])
+        _ -> Nothing
+    _ -> Nothing
+    
+  where
+    third1 [] = []
+    third1 [_] = []
+    third1 [_,_] = []
+    third1 (_:_:e:xs) = e : third1 xs
+    third2 [] = []
+    third2 [_] = []
+    third2 [_,e] = [e]
+    third2 (_:e:_:xs) = e : third2 xs
+    third3 [] = []
+    third3 [e] = [e]
+    third3 [e,_] = [e]
+    third3 (e:_:_:xs) = e : third3 xs
+
+typeinfer' _ depth _ l@Unit a = do
+  ss <- unify Unitty a
+  return (ss, Deduction (l, depth, ss a) Lunit [])
+
+typeinfer' vars depth ctx l@(Abort m) a = do
+  (ss, d1) <- typeinfer' vars depth ctx m Bottom
+  return (ss, Deduction (l, depth, ss a) Labort [d1])
+
+typeinfer' vars depth ctx l@(Absurd m) a = do
+  sigma     <- unify Bottom a
+  (tau, d1) <- typeinfer' vars depth (applyctx sigma ctx) m Bottom
+  let ss = tau . sigma
+  return (ss, Deduction (l, depth, ss a) Labsurd [d1])
+
+                     
diff --git a/source/Stlc/Types.hs b/source/Stlc/Types.hs
new file mode 100644
--- /dev/null
+++ b/source/Stlc/Types.hs
@@ -0,0 +1,275 @@
+module Stlc.Types
+  ( Type (Tvar, Arrow, Times, Union, Unitty, Bottom)
+  , typeinference
+  , typeinfer
+  , unify
+  , applyctx
+  , emptyctx
+  , incrementindices
+  , variables
+  , normalizeTemplate
+  , applynormalization
+  , Top (Top)
+  , Context
+  , Variable
+  , Substitution
+  )
+where
+
+import Control.Monad
+import Lambda
+
+import qualified Data.Map as Map
+
+-- | 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
+
+-- | A type variable is an integer.
+type Variable = Integer
+
+-- | A type substitution is a function that can be applied to any type
+-- to get a new one.
+type Substitution = Type -> Type
+
+-- | 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
+          deriving (Eq)
+
+instance Show Type where
+  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 = "⊥"
+
+showparens :: Type -> String
+showparens (Tvar t) = show (Tvar t)
+showparens Unitty = show Unitty
+showparens Bottom = show Bottom
+showparens m = "(" ++ show m ++ ")"
+  
+-- | Creates the substitution given by the change of a variable for
+-- the given type.
+subs :: Variable -> Type -> Substitution
+subs x typ (Tvar y)
+  | x == y    = typ
+  | otherwise = Tvar y
+subs x typ (Arrow a b) = Arrow (subs x typ a) (subs x typ b)
+subs x typ (Times a b) = Times (subs x typ a) (subs x typ b)
+subs x typ (Union a b) = Union (subs x typ a) (subs x typ b)
+subs _ _ Unitty = Unitty
+subs _ _ Bottom = Bottom
+
+-- | Returns true if the given variable appears on the type.
+occurs :: Variable -> Type -> Bool
+occurs x (Tvar y)    = x == y
+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 _ Bottom = False
+
+-- | Unifies two types with their most general unifier. Returns the substitution
+-- that transforms any of the types into the unifier.
+unify :: Type -> Type -> Maybe Substitution
+unify (Tvar x) (Tvar y)
+  | x == y = Just id
+  | otherwise = Just (subs x (Tvar y))
+unify (Tvar x) b
+  | occurs x b = Nothing
+  | otherwise = Just (subs x b)
+unify a (Tvar y)
+  | occurs y a = Nothing
+  | otherwise = Just (subs y a)
+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
+
+-- | The empty context.
+emptyctx :: Context
+emptyctx = Map.empty
+
+-- | Increments all the indices of a given context. It is useful for
+-- adapting the context to a new scope.
+incrementindices :: Context -> Context
+incrementindices = Map.mapKeys succ
+
+-- | Type inference algorithm. Infers a type from a given context and expression
+-- with a set of constraints represented by a unifier type. The result type must
+-- be unifiable with this given type.
+typeinfer :: [Variable] -- ^ List of fresh variables
+          -> Context    -- ^ Type context
+          -> Exp        -- ^ Lambda expression whose type has to be inferred
+          -> Type       -- ^ Constraint
+          -> Maybe Substitution
+          
+typeinfer []  _ _ _ = Nothing
+typeinfer [_] _ _ _ = Nothing
+
+typeinfer _ ctx (Var n) b
+   | Map.member n ctx = do
+       var <- Map.lookup n ctx
+       unify var b
+   | otherwise  = Nothing
+
+typeinfer (x:vars) ctx (App p q) b = do
+  sigma <- typeinfer (evens vars) ctx                  p (Arrow (Tvar x) b)
+  tau   <- typeinfer (odds  vars) (applyctx sigma ctx) q (sigma (Tvar x))
+  return (tau . sigma)
+  where
+    odds [] = []
+    odds [_] = []
+    odds (_:e:xs) = e : odds xs
+    evens [] = []
+    evens [e] = [e]
+    evens (e:_:xs) = e : evens xs
+
+
+typeinfer (a:x:vars) ctx (Lambda p) b = do
+  sigma <- unify b (Arrow (Tvar a) (Tvar x))
+  let nctx = applyctx sigma (Map.insert 1 (sigma $ Tvar a) (incrementindices ctx))
+  tau   <- typeinfer vars nctx p (sigma $ Tvar x)
+  return (tau . sigma)
+
+typeinfer (x:y:vars) ctx (Pair m n) a = do
+  sigma <- unify a (Times (Tvar x) (Tvar y))
+  tau   <- typeinfer (evens vars) (applyctx sigma         ctx) m (sigma (Tvar x))
+  rho   <- typeinfer (odds  vars) (applyctx (tau . sigma) ctx) n (tau (sigma (Tvar y)))
+  return (rho . tau . sigma)
+  where
+    odds [] = []
+    odds [_] = []
+    odds (_:e:xs) = e : odds xs
+    evens [] = []
+    evens [e] = [e]
+    evens (e:_:xs) = e : evens xs
+
+
+typeinfer (y:vars) ctx (Pi1 m) a = typeinfer vars ctx m (Times a (Tvar y))
+typeinfer (x:vars) ctx (Pi2 m) b = typeinfer vars ctx m (Times (Tvar x) b)
+
+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))
+  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))
+  return (tau . sigma)
+
+typeinfer (x:y:vars) ctx (Caseof m f g) a = do
+  sigma <- typeinfer (third1 vars) ctx                          f (Arrow (Tvar x) a)
+  tau   <- typeinfer (third2 vars) (applyctx sigma ctx)         g (Arrow (sigma $ Tvar y) (sigma a))
+  rho   <- typeinfer (third3 vars) (applyctx (tau . sigma) ctx) m (Union (tau . sigma $ Tvar x) (tau . sigma $ Tvar y))
+  return (rho . tau . sigma)
+  where
+    third1 [] = []
+    third1 [_] = []
+    third1 [_,_] = []
+    third1 (_:_:e:xs) = e : third1 xs
+    third2 [] = []
+    third2 [_] = []
+    third2 [_,e] = [e]
+    third2 (_:e:_:xs) = e : third2 xs
+    third3 [] = []
+    third3 [e] = [e]
+    third3 [e,_] = [e]
+    third3 (e:_:_:xs) = e : third3 xs
+
+typeinfer _ _ Unit a = unify Unitty a
+
+typeinfer vars ctx (Abort m) _ = typeinfer vars ctx m Bottom
+
+typeinfer vars ctx (Absurd m) a = do
+  sigma <- unify Bottom a
+  tau   <- typeinfer vars (applyctx sigma ctx) m Bottom
+  return (tau . sigma)
+  
+
+-- | Type inference of a lambda expression.
+typeinference :: Exp -> Maybe Type
+typeinference e = normalize <$> (typeinfer variables emptyctx e (Tvar 0) <*> pure (Tvar 0))
+
+-- | List of possible variable names.
+typevariableNames :: [String]
+typevariableNames = concatMap (`replicateM` ['A'..'Z']) [1..]
+
+-- | Infinite list of variables.
+variables :: [Variable]
+variables = [1..]
+
+
+-- | Substitutes a set of type variables on a type template for the smaller
+-- possible ones.
+normalizeTemplate :: Map.Map Integer Integer -> Integer -> Type -> (Map.Map Integer Integer, Integer)
+normalizeTemplate sub n (Tvar m) = case Map.lookup m sub of
+                                    Just _  -> (sub, n)
+                                    Nothing -> (Map.insert m n sub, succ n)
+normalizeTemplate sub n (Arrow a b) =
+  let (nsub, nn) = normalizeTemplate sub n a in normalizeTemplate nsub nn b
+normalizeTemplate sub n (Times a b) =
+  let (nsub, nn) = normalizeTemplate sub n a in normalizeTemplate nsub nn b
+normalizeTemplate sub n (Union a b) =
+  let (nsub, nn) = normalizeTemplate sub n a in normalizeTemplate nsub nn b
+normalizeTemplate sub n Unitty = (sub, n)
+normalizeTemplate sub n Bottom = (sub, n)
+
+-- | 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
+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)
+applynormalization _ Unitty = Unitty
+applynormalization _ Bottom = Bottom
+
+
+
+-- | Normalizes a type, that is, substitutes the set of type variables for
+-- 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/source/Types.hs b/source/Types.hs
deleted file mode 100644
--- a/source/Types.hs
+++ /dev/null
@@ -1,268 +0,0 @@
-module Types
-  ( Type (Tvar, Arrow, Times, Union, Unitty, Bottom)
-  , typeinference
-  , Top (Top)
-  )
-where
-
-import Control.Monad
-import Lambda
-
-import qualified Data.Map as Map
-
--- | 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
-
--- | A type variable is an integer.
-type Variable = Integer
-
--- | A type substitution is a function that can be applied to any type
--- to get a new one.
-type Substitution = Type -> Type
-
--- | 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
-  deriving (Eq)
-
-instance Show Type where
-  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) = "⊥"
-
-showparens :: Type -> String
-showparens (Tvar t) = show (Tvar t)
-showparens Unitty = show Unitty
-showparens Bottom = show Bottom
-showparens m = "(" ++ show m ++ ")"
-  
--- | Creates the substitution given by the change of a variable for
--- the given type.
-subs :: Variable -> Type -> Substitution
-subs x typ (Tvar y)
-  | x == y    = typ
-  | otherwise = Tvar y
-subs x typ (Arrow a b) = Arrow (subs x typ a) (subs x typ b)
-subs x typ (Times a b) = Times (subs x typ a) (subs x typ b)
-subs x typ (Union a b) = Union (subs x typ a) (subs x typ b)
-subs _ _ Unitty = Unitty
-subs _ _ Bottom = Bottom
-
--- | Returns true if the given variable appears on the type.
-occurs :: Variable -> Type -> Bool
-occurs x (Tvar y)    = x == y
-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 _ (Bottom)    = False
-
--- | Unifies two types with their most general unifier. Returns the substitution
--- that transforms any of the types into the unifier.
-unify :: Type -> Type -> Maybe Substitution
-unify (Tvar x) (Tvar y)
-  | x == y    = Just id
-  | otherwise = Just (subs x (Tvar y))
-unify (Tvar x) b
-  | occurs x b = Nothing
-  | otherwise  = Just (subs x b)
-unify a (Tvar y)
-  | occurs y a = Nothing
-  | otherwise  = Just (subs y a)
-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
-
--- | The empty context.
-emptyctx :: Context
-emptyctx = Map.empty
-
--- | Increments all the indices of a given context. It is useful for
--- adapting the context to a new scope.
-incrementindices :: Context -> Context
-incrementindices = Map.mapKeys succ
-
--- | Type inference algorithm. Infers a type from a given context and expression
--- with a set of constraints represented by a unifier type. The result type must
--- be unifiable with this given type.
-typeinfer :: [Variable] -- ^ List of fresh variables
-          -> Context    -- ^ Type context
-          -> Exp        -- ^ Lambda expression whose type has to be inferred
-          -> Type       -- ^ Constraint
-          -> Maybe Substitution
-          
-typeinfer []  _ _ _ = Nothing
-typeinfer [_] _ _ _ = Nothing
-
-typeinfer _ ctx (Var n) b
-   | Map.member n ctx = do
-       var <- Map.lookup n ctx
-       unify var b
-   | otherwise  = Nothing
-
-typeinfer (x:vars) ctx (App p q) b = do
-  sigma <- typeinfer (evens vars) ctx                  p (Arrow (Tvar x) b)
-  tau   <- typeinfer (odds  vars) (applyctx sigma ctx) q (sigma (Tvar x))
-  return (tau . sigma)
-  where
-    odds [] = []
-    odds [_] = []
-    odds (_:e:xs) = e : odds xs
-    evens [] = []
-    evens [e] = [e]
-    evens (e:_:xs) = e : evens xs
-
-
-typeinfer (a:x:vars) ctx (Lambda p) b = do
-  sigma <- unify b (Arrow (Tvar a) (Tvar x))
-  let nctx = applyctx sigma (Map.insert 1 (sigma $ Tvar a) (incrementindices ctx))
-  tau   <- typeinfer vars nctx p (sigma $ Tvar x)
-  return (tau . sigma)
-
-typeinfer (x:y:vars) ctx (Pair m n) a = do
-  sigma <- unify a (Times (Tvar x) (Tvar y))
-  tau   <- typeinfer (evens vars) (applyctx sigma         ctx) m (sigma (Tvar x))
-  rho   <- typeinfer (odds  vars) (applyctx (tau . sigma) ctx) n (tau (sigma (Tvar y)))
-  return (rho . tau . sigma)
-  where
-    odds [] = []
-    odds [_] = []
-    odds (_:e:xs) = e : odds xs
-    evens [] = []
-    evens [e] = [e]
-    evens (e:_:xs) = e : evens xs
-
-
-typeinfer (y:vars) ctx (Pi1 m) a = typeinfer vars ctx m (Times a (Tvar y))
-typeinfer (x:vars) ctx (Pi2 m) b = typeinfer vars ctx m (Times (Tvar x) b)
-
-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))
-  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))
-  return (tau . sigma)
-
-typeinfer (x:y:vars) ctx (Caseof m f g) a = do
-  sigma <- typeinfer (third1 vars) ctx                          f (Arrow (Tvar x) a)
-  tau   <- typeinfer (third2 vars) (applyctx sigma ctx)         g (Arrow (sigma $ Tvar y) (sigma a))
-  rho   <- typeinfer (third3 vars) (applyctx (tau . sigma) ctx) m (Union (tau . sigma $ Tvar x) (tau . sigma $ Tvar y))
-  return (rho . tau . sigma)
-  where
-    third1 [] = []
-    third1 [_] = []
-    third1 [_,_] = []
-    third1 (_:_:e:xs) = e : third1 xs
-    third2 [] = []
-    third2 [_] = []
-    third2 [_,e] = [e]
-    third2 (_:e:_:xs) = e : third2 xs
-    third3 [] = []
-    third3 [e] = [e]
-    third3 [e,_] = [e]
-    third3 (e:_:_:xs) = e : third3 xs
-
-typeinfer _ _ Unit a = unify Unitty a
-
-typeinfer vars ctx (Abort m) _ = typeinfer vars ctx m Bottom
-
-typeinfer vars ctx (Absurd m) a = do
-  sigma <- unify Bottom a
-  tau   <- typeinfer vars (applyctx sigma ctx) m Bottom
-  return (tau . sigma)
-  
-
--- | Type inference of a lambda expression.
-typeinference :: Exp -> Maybe Type
-typeinference e = normalize <$> (typeinfer variables emptyctx e (Tvar 0) <*> pure (Tvar 0))
-
--- | List of possible variable names.
-typevariableNames :: [String]
-typevariableNames = concatMap (`replicateM` ['A'..'Z']) [1..]
-
--- | Infinite list of variables.
-variables :: [Variable]
-variables = [1..]
-
-
--- | Substitutes a set of type variables on a type template for the smaller
--- possible ones.
-normalizeTemplate :: Map.Map Integer Integer -> Integer -> Type -> (Map.Map Integer Integer, Integer)
-normalizeTemplate sub n (Tvar m) = case Map.lookup m sub of
-                                    Just _  -> (sub, n)
-                                    Nothing -> (Map.insert m n sub, succ n)
-normalizeTemplate sub n (Arrow a b) =
-  let (nsub, nn) = normalizeTemplate sub n a in normalizeTemplate nsub nn b
-normalizeTemplate sub n (Times a b) =
-  let (nsub, nn) = normalizeTemplate sub n a in normalizeTemplate nsub nn b
-normalizeTemplate sub n (Union a b) =
-  let (nsub, nn) = normalizeTemplate sub n a in normalizeTemplate nsub nn b
-normalizeTemplate sub n Unitty = (sub, n)
-normalizeTemplate sub n Bottom = (sub, n)
-
--- | 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
-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)
-applynormalization _ Unitty = Unitty
-applynormalization _ Bottom = Bottom
-
-
-
--- | Normalizes a type, that is, substitutes the set of type variables for
--- 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/std.mkr b/std.mkr
deleted file mode 100644
--- a/std.mkr
+++ /dev/null
@@ -1,192 +0,0 @@
-## Standard library ##
-
-# This is the standard library for the Mikrokosmos untyped lambda calculus
-# interpreter. It contains basic logic and arithmetic operations.
-# You can read more about Church encoding in its wikipedia page:
-#   https://en.wikipedia.org/wiki/Church_encoding
-#
-# This library is licensed under CC0.
-
-
-
-
-## Logic
-# Uses Church Booleans
-true  = \a.\b.a
-false = \a.\b.b
-
-# Basic logic gates
-and = \p.\q.p q p
-or  = \p.\q.p p q
-not = \b.b false true
-
-# Conditional
-ifelse = (\x.x)
-
-
-
-
-## Arithmethic
-# This library uses Church numerals to represent natural numbers
-# Succesor of a natural number is defined with 0
-succ = \n.\f.\x.f (n f x)
-0 = \f.\x.x
-
-# Basic operations on natural numbers
-plus = \m.\n.\f.\x.m f (n f x)
-mult = \m.\n.\f.\x.m (n f) x
-
-# Substraction
-pred  = \n.\f.\x.n (\g.(\h.h (g f))) (\u.x) (\u.u)
-minus = \m.\n.(n pred) m
-
-# Predicates on natural numbers
-iszero = \n.(n (\x.false) true)
-leq    = \m.\n.(iszero (minus m n))
-eq     = \m.\n.(and (leq m n) (leq n m))
-
-
-
-
-## Data structures
-# Pairs
-pair   = \x.\y.\z.z x y
-first  = \p.p true
-second = \p.p false
-
-# Lists
-# Uses the right-fold representation of lists.
-# The representation of a list is its foldr function.
-cons = \h.\t.\c.\n.(c h (t c n))
-nil = \c.\n.n
-
-# Folds
-foldr  = \o.\n.\l.(l o n)
-sum    = (foldr plus 0)
-prod   = (foldr mult (succ 0))
-length = (foldr (\h.\t.succ t) 0)
-
-# Map
-# Writes map as a foldr.
-map    = (\f.(foldr (\h.\t.cons (f h) t) nil))
-filter = \p.(foldr (\h.\t.((p h) (cons h t) t)) nil)
-
-# Trees
-# Uses the fold representation of a binary tree
-# Its nil is the same one as the list representation
-node = \x.\l.\r.\f.\n.(f x (l f n) (r f n))
-
-
-
-
-## Fixpoint operator and recursion
-fix != (\f.(\x.f (x x)) (\x.f (x x)))
-fact != fix (\f.\n.iszero n (succ 0) (mult n (f (pred n))))
-fib != fix (\f.\n.iszero n (succ 0) (plus (f (pred n)) (f (pred (pred n)))))
-
-
-
-
-## APPENDIX
-## Natural numbers
-# List of 100 first natural numbers
-1 = succ 0
-2 = succ 1
-3 = succ 2
-4 = succ 3
-5 = succ 4
-6 = succ 5
-7 = succ 6
-8 = succ 7
-9 = succ 8
-10 = succ 9
-11 = succ 10
-12 = succ 11
-13 = succ 12
-14 = succ 13
-15 = succ 14
-16 = succ 15
-17 = succ 16
-18 = succ 17
-19 = succ 18
-20 = succ 19
-21 = succ 20
-22 = succ 21
-23 = succ 22
-24 = succ 23
-25 = succ 24
-26 = succ 25
-27 = succ 26
-28 = succ 27
-29 = succ 28
-30 = succ 29
-31 = succ 30
-32 = succ 31
-33 = succ 32
-34 = succ 33
-35 = succ 34
-36 = succ 35
-37 = succ 36
-38 = succ 37
-39 = succ 38
-40 = succ 39
-41 = succ 40
-42 = succ 41
-43 = succ 42
-44 = succ 43
-45 = succ 44
-46 = succ 45
-47 = succ 46
-48 = succ 47
-49 = succ 48
-50 = succ 49
-51 = succ 50
-52 = succ 51
-53 = succ 52
-54 = succ 53
-55 = succ 54
-56 = succ 55
-57 = succ 56
-58 = succ 57
-59 = succ 58
-60 = succ 59
-61 = succ 60
-62 = succ 61
-63 = succ 62
-64 = succ 63
-65 = succ 64
-66 = succ 65
-67 = succ 66
-68 = succ 67
-69 = succ 68
-70 = succ 69
-71 = succ 70
-72 = succ 71
-73 = succ 72
-74 = succ 73
-75 = succ 74
-76 = succ 75
-77 = succ 76
-78 = succ 77
-79 = succ 78
-80 = succ 79
-81 = succ 80
-82 = succ 81
-83 = succ 82
-84 = succ 83
-85 = succ 84
-86 = succ 85
-87 = succ 86
-88 = succ 87
-89 = succ 88
-90 = succ 89
-91 = succ 90
-92 = succ 91
-93 = succ 92
-94 = succ 93
-95 = succ 94
-96 = succ 95
-97 = succ 96
-98 = succ 97
-99 = succ 98
-100 = succ 99
diff --git a/tests/test.hs b/tests/test.hs
--- a/tests/test.hs
+++ b/tests/test.hs
@@ -1,13 +1,16 @@
 import Test.Tasty
 import Test.Tasty.HUnit
 import Test.Tasty.QuickCheck as QC
+import Test.Tasty.Golden as TG
+import System.Process
 
 import Text.ParserCombinators.Parsec
 import NamedLambda
 import Lambda
-import Types
+import Stlc.Types
 import Ski
 import Environment
+import Interpreter
 
 
 main :: IO ()
@@ -19,6 +22,8 @@
   , typeinferTests
   , skiabsTests
   , lambdaProps
+  , parserProps
+  , goldenTests
   ]
 
 -- Unit tests
@@ -53,7 +58,7 @@
     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)))))))))
+    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)
   ]
@@ -75,31 +80,23 @@
   ]
 
 
--- Lambda properties
+
+-- Quickcheck
 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
+  [ QC.testProperty "Expression -> named -> expression" $
+      \expr -> toBruijn emptyContext (nameExp expr) == expr
+  , QC.testProperty "Open expressions are not allowed" $
+      \expr -> not (isOpenExp expr)
   ]
-  
 
--- 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)
---   ]
+parserProps :: TestTree
+parserProps = testGroup "Parser properties (quickcheck)"
+  [ QC.testProperty "Comments are ignored" $
+      \str -> case parse interpreteractionParser "" ("#" ++ str) of
+                Right (Interpret Comment) -> True
+                _ -> False
+  ]
 
 
 -- Arbitrary typed lambda expressions
@@ -109,7 +106,7 @@
 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 0    = Var <$> (toInteger <$> choose (1, lim))
 lambda lim size = oneof
   [ Var <$> (toInteger <$> choose (1, lim))
   , Lambda <$> lambda (succ lim) (size-1)
@@ -129,3 +126,14 @@
   , Abort <$> lambda lim (size-1)
   , Absurd <$> lambda lim (size-1)
   ]
+
+
+-- Golden test
+goldenTests :: TestTree
+goldenTests = testGroup "Golden tests (tasty-golden)"
+  [ goldenVsFile "Main golden test"
+      "tests/goldenfile.golden"
+      "tests/testingfile"
+      (callCommand "mikrokosmos tests/testing.mkr > tests/testingfile")
+  ]
+