diff --git a/src/Bergamot/Latex.elm b/src/Bergamot/Latex.elm
new file mode 100644
index 0000000..404ade4
--- /dev/null
+++ b/src/Bergamot/Latex.elm
@@ -0,0 +1,34 @@
+module Bergamot.Latex exposing (..)
+
+import Bergamot.Syntax exposing (..)
+import Bergamot.Rules exposing (..)
+
+termToLatex : (a -> String) -> Term a -> String
+termToLatex f t =
+    case t of
+        Call "type" [t1, t2] -> termToLatex f t1 ++ " : " ++ termToLatex f t2
+        Call "intlit" [t1]   -> termToLatex f t1
+        Call "tpair" [t1, t2] -> termToLatex f t1 ++ "\\times" ++ termToLatex f t2
+        Call "plus" [t1, t2] -> termToLatex f t1 ++ " + " ++ termToLatex f t2
+        Call "pair" [t1, t2] -> "(" ++ termToLatex f t1 ++ ", " ++ termToLatex f t2 ++ ")"
+        Call s [] -> "\\text{" ++ s ++ "}"
+        Call s ts -> "\\text{" ++ s ++ "}(" ++ String.join "," (List.map (termToLatex f) ts) ++ ")"
+        Var x -> f x
+        IntLit i -> String.fromInt i
+        StringLit s -> "\"" ++ s ++ "\""
+
+metavariableToLatex : Metavariable -> String
+metavariableToLatex (MkMetavariable s) =
+    let
+        noQuestion = String.dropLeft 1 s
+    in
+        if String.startsWith "tau" noQuestion then "\\" ++ noQuestion else noQuestion
+
+ruleToLatex : Rule -> String
+ruleToLatex r = "\\cfrac{" ++ String.join "\\quad " (List.map (termToLatex metavariableToLatex) r.premises) ++ "}{" ++ termToLatex metavariableToLatex r.conclusion ++ "}\\ \\texttt{" ++ r.name ++ "}"
+
+unificationVarToLatex : UnificationVar -> String
+unificationVarToLatex (MkUnificationVar s) = s
+
+proofTreeToLatex : ProofTree -> String
+proofTreeToLatex (MkProofTree node) = "\\cfrac{" ++ String.join "\\quad " (List.map proofTreeToLatex node.premises) ++ "}{" ++ termToLatex unificationVarToLatex node.conclusion ++ "}\\ \\texttt{" ++ node.name ++ "}"
diff --git a/src/Main.elm b/src/Main.elm
index 54c603e..84a1fb6 100644
--- a/src/Main.elm
+++ b/src/Main.elm
@@ -8,6 +8,7 @@ import Bergamot.Syntax exposing (..)
 import Bergamot.Search exposing (..)
 import Bergamot.Rules exposing (..)
 import Bergamot.Parser exposing (..)
+import Bergamot.Latex exposing (..)
 import Maybe
 import Tuple
 import Debug
@@ -24,6 +25,12 @@ type Msg
 init : Flags -> (Model, Cmd Msg)
 init () = ({ program = "", query = "" }, Cmd.none)
 
+printRules : String -> Maybe String
+printRules progs =
+    case run program progs of
+        Just prog -> Just (String.join "\n\\quad" (List.map ruleToLatex prog.rules))
+        Nothing -> Nothing
+
 proveQuery : String -> String -> Maybe ProofTree
 proveQuery progs querys =
     case (run program progs, run term querys) of
@@ -35,7 +42,11 @@ view m = Html.div []
     [ Html.textarea [ onInput SetProgram ] []
     , Html.br [] []
     , Html.input [ type_ "text", onInput SetQuery ] []
-    , Html.p [] [ Html.text (Debug.toString (proveQuery m.program m.query)) ]
+    , Html.pre [] [ Html.code [] [ Html.text (Maybe.withDefault "" (printRules m.program)) ] ]
+    , Html.pre [] [ Html.code [] [ Html.text (
+        proveQuery m.program m.query
+        |> Maybe.map proofTreeToLatex
+        |> Maybe.withDefault "") ] ]
     ]
 
 update : Msg -> Model -> (Model, Cmd Msg)