diff --git a/cooltt.opam b/cooltt.opam
index 124a27199..9676279ba 100644
--- a/cooltt.opam
+++ b/cooltt.opam
@@ -18,6 +18,7 @@ depends: [
   "menhir" {>= "20180703"}
   "uuseg" {>= "12.0.0"}
   "uutf" {>= "1.0.2"}
+  "lsp" {>= "1.8.3"}
   "odoc" {with-doc}
   "bantorra"
   "yuujinchou"
diff --git a/emacs/cooltt-lsp.el b/emacs/cooltt-lsp.el
new file mode 100644
index 000000000..04f771d2e
--- /dev/null
+++ b/emacs/cooltt-lsp.el
@@ -0,0 +1,19 @@
+;;; cooltt-lsp ---  -*- lexical-binding: t; -*-
+
+;;; Commentary:
+(require 'cooltt)
+(require 'lsp-mode)
+
+(lsp-register-client
+ (make-lsp-client
+  :new-connection (lsp-stdio-connection (list cooltt-command "--mode" "server"))
+  :major-modes '(cooltt-mode)
+  :server-id 'cooltt))
+
+(lsp-consistency-check cooltt-lsp)
+(add-to-list 'lsp-language-id-configuration '(cooltt-mode . "cooltt"))
+
+;;; Code:
+
+(provide 'cooltt-lsp)
+;;; cooltt-lsp.el ends here
diff --git a/emacs/cooltt.el b/emacs/cooltt.el
index cc647d2bf..4c2d36ce0 100644
--- a/emacs/cooltt.el
+++ b/emacs/cooltt.el
@@ -120,7 +120,7 @@
   "Declaration keywords.")
 
 (defconst cooltt-command-keywords
-  '("#fail" "#normalize" "#print" "#quit")
+  '("#fail" "#normalize" "#print" "#quit" "#viz")
   "Command keywords.")
 
 (defconst cooltt-expression-keywords
@@ -186,7 +186,7 @@ See `compilation-error-regexp-alist' for semantics.")
 
 (defun cooltt-compile-options ()
   "Compute the options to provide to cooltt."
-  (let (opts cooltt-options)
+  (let ((opts cooltt-options))
     (when cooltt-debug
       (push "--debug" opts))
     opts))
diff --git a/src/basis/SegmentTree.ml b/src/basis/SegmentTree.ml
new file mode 100644
index 000000000..9c1aab754
--- /dev/null
+++ b/src/basis/SegmentTree.ml
@@ -0,0 +1,73 @@
+module type POSITION =
+sig
+  include Map.OrderedType
+  type range = { start : t; stop: t }
+  val cut_range_after : t -> range -> range
+  val cut_range_before : t -> range -> range
+end
+
+module type S = functor (Pos: POSITION) ->
+sig
+  type !+'a t
+  val lookup : Pos.t -> 'a t -> 'a option
+  val containing : Pos.t -> 'a t -> 'a list
+  val of_list : (Pos.range * 'a) list -> 'a t
+  val empty : 'a t
+
+  val pp : (Format.formatter -> Pos.range -> unit) -> (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit
+end
+
+module Make : S = functor (Pos : POSITION) ->
+struct
+
+  module Range = struct
+    type t = Pos.range
+    let compare (x : t) (y : t) =
+      CCOrd.(Pos.compare x.start y.start <?> (opp Pos.compare, x.stop, y.stop))
+  end
+
+  module SegTree = CCMap.Make(Range)
+
+  type !+'a t = 'a SegTree.t
+
+  let lookup pos t =
+    match SegTree.find_last_opt (fun k -> Range.compare k {start = pos; stop = pos} <= 0) t with
+    | None -> None
+    | Some (r, v) ->
+      if Pos.compare r.stop pos >= 0 then Some v else None
+
+  let containing pos t =
+    (* FIXME: This is suboptimal *)
+    CCList.of_iter @@ SegTree.values @@ SegTree.filter (fun range _ -> range.start <= pos && pos <= range.stop) t
+
+  let of_sorted_list l =
+    let rec loop tree stack l =
+      match stack, l with
+      | _, [] -> SegTree.add_list tree stack
+      | [], x :: l -> loop tree [x] l
+      | ((xk, xv) as x) :: stack, ((yk, _) as y :: l) ->
+        if Pos.compare yk.stop xk.start < 0 then
+          loop tree (y :: x :: stack) l
+        else if Pos.compare xk.stop yk.start < 0 then
+          loop (SegTree.add xk xv tree) stack (y :: l)
+        else
+          let tree =
+            if Pos.compare xk.start yk.start < 0 then
+              SegTree.add (Pos.cut_range_after yk.start xk) xv tree
+            else
+              tree
+          in
+          if Pos.compare xk.stop yk.stop > 0 then
+            loop tree (y :: (Pos.cut_range_before yk.stop xk, xv) :: stack) l
+          else
+            loop tree stack (y :: l)
+    in
+    loop SegTree.empty [] l
+
+  let of_list l =
+    of_sorted_list (CCList.sort (CCOrd.(>|=) Range.compare fst) l)
+
+  let empty = SegTree.empty
+
+  let pp pp_range pp_elem : Format.formatter -> 'a t -> unit = SegTree.pp pp_range pp_elem
+end
diff --git a/src/basis/SegmentTree.mli b/src/basis/SegmentTree.mli
new file mode 100644
index 000000000..46b4a19cd
--- /dev/null
+++ b/src/basis/SegmentTree.mli
@@ -0,0 +1,20 @@
+module type POSITION =
+sig
+  include Map.OrderedType
+  type range = { start : t; stop: t }
+  val cut_range_after : t -> range -> range
+  val cut_range_before : t -> range -> range
+end
+
+module type S = functor (Pos: POSITION) ->
+sig
+  type !+'a t
+  val lookup : Pos.t -> 'a t -> 'a option
+  val containing : Pos.t -> 'a t -> 'a list
+  val of_list : (Pos.range * 'a) list -> 'a t
+  val empty : 'a t
+
+  val pp : (Format.formatter -> Pos.range -> unit) -> (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit
+end
+
+module Make : S
diff --git a/src/bin/dune b/src/bin/dune
index 5d3b6ddfa..cb6dc5573 100644
--- a/src/bin/dune
+++ b/src/bin/dune
@@ -2,7 +2,7 @@
 
 (executables
  (names main)
- (libraries cooltt.frontend cmdliner))
+ (libraries cooltt.frontend cooltt.server cmdliner))
 
 (install
  (section bin)
diff --git a/src/bin/main.ml b/src/bin/main.ml
index 1a3d429ef..eb50e45c4 100644
--- a/src/bin/main.ml
+++ b/src/bin/main.ml
@@ -1,3 +1,4 @@
+open Server
 open Frontend
 open Cmdliner
 
@@ -5,18 +6,29 @@ let _ =
   Printexc.record_backtrace false;
   ()
 
+type mode =
+  [ `Interactive
+  | `Scripting of [`Stdin | `File of string]
+  | `Server
+  ]
+
 type options =
-  { mode : [`Interactive | `Scripting of [`Stdin | `File of string]];
+  { mode : mode;
     as_file : string option;
     width : int;
-    debug_mode : bool }
+    debug_mode : bool;
+  }
+
+let options mode as_file width debug_mode =
+  { mode; as_file; width; debug_mode }
 
-let main {mode; as_file; width; debug_mode} =
+let main {mode; as_file; width; debug_mode; _} =
   Format.set_margin width;
   match
     match mode with
-    | `Interactive -> Driver.do_repl ~as_file ~debug_mode
-    | `Scripting input -> Driver.load_file ~as_file ~debug_mode input
+    | `Interactive -> Driver.do_repl {as_file; debug_mode}
+    | `Scripting input -> Driver.load_file {as_file; debug_mode;} input
+    | `Server -> LanguageServer.run ()
   with
   | Ok () -> `Ok ()
   | Error () -> `Error (false, "encountered one or more errors")
@@ -25,7 +37,7 @@ let opt_mode =
   let doc =
     "Set the interaction mode. "^
     "The value $(docv) must be one of "^
-    "$(b,scripting) (default) or $(b,interactive)." in
+    "$(b,scripting) (default), $(b,interactive), or $(b,server)." in
   Arg.(value & opt (some string) None & info ["m"; "mode"] ~doc ~docv:"MODE")
 
 let opt_interactive =
@@ -63,28 +75,34 @@ let parse_mode =
   function
   | "interactive" -> `Interactive
   | "scripting" -> `Scripting
+  | "server" -> `Server
   | s -> `Nonexistent s
 
 let quote s = "`" ^ s ^ "'"
 
-let consolidate_options mode interactive width input_file as_file debug_mode : options Term.ret =
-  match Option.map parse_mode mode, interactive, width, input_file with
-  | (Some `Scripting | None), false, width, Some input_file ->
-    `Ok {mode = `Scripting input_file; as_file; width; debug_mode}
-  | (Some `Scripting | None), false, _, None ->
-    `Error (true, "scripting mode expects an input file")
-  | Some `Interactive, _, width, None | None, true, width, None ->
-    `Ok {mode = `Interactive; as_file; width; debug_mode}
-  | Some `Interactive, _, _, Some _ | None, true, _, _ ->
-    `Error (true, "interactive mode expects no input files")
-  | Some `Scripting, true, _, _ ->
-    `Error (true, "inconsistent mode assignment")
-  | Some (`Nonexistent s), _, _, _ ->
-    `Error (true, "no mode named " ^ quote s)
+let consolidate_input_options mode interactive input_file : (mode, [`Msg of string]) result  =
+  match Option.map parse_mode mode, interactive, input_file with
+  | (Some `Scripting | None), false, Some input_file ->
+    Ok (`Scripting input_file)
+  | (Some `Scripting | None), false, None ->
+    Error (`Msg "scripting mode expects an input file")
+  | Some `Interactive, _, None | None, true, None ->
+    Ok `Interactive
+  | Some `Server, false, None ->
+    Ok `Server
+  | Some `Interactive, _, Some _ | None, true, _ ->
+    Error (`Msg "interactive mode expects no input files")
+  | Some `Server, _, Some _ ->
+    Error (`Msg "server mode expects no input files")
+  | Some `Scripting, true, _ ->
+    Error (`Msg "inconsistent mode assignment")
+  | Some `Server, true, _ ->
+    Error (`Msg "inconsistent mode assignment")
+  | Some (`Nonexistent s), _, _ ->
+    Error (`Msg ("no mode named " ^ quote s))
 
 let () =
-  let options : options Term.t =
-    Term.(ret (const consolidate_options $ opt_mode $ opt_interactive $ opt_width $ opt_input_file $ opt_as_file $ opt_debug))
-  in
+  let opts_input = Term.(term_result ~usage:true (const consolidate_input_options $ opt_mode $ opt_interactive $ opt_input_file))  in
+  let options : options Term.t = Term.(const options $ opts_input $ opt_as_file $ opt_width $ opt_debug) in
   let t = Term.ret @@ Term.(const main $ options) in
   Term.exit @@ Term.eval ~catch:true ~err:Format.std_formatter (t, myinfo)
diff --git a/src/core/RefineMonad.ml b/src/core/RefineMonad.ml
index 345bd7d38..7de26444f 100644
--- a/src/core/RefineMonad.ml
+++ b/src/core/RefineMonad.ml
@@ -5,6 +5,7 @@ module S = Syntax
 module St = RefineState
 module Env = RefineEnv
 module Err = RefineError
+module Metadata = RefineMetadata
 module Qu = Quote
 module Conv = Conversion
 
@@ -167,3 +168,20 @@ let push_problem lbl =
 
 let update_span loc =
   scope @@ Env.set_location loc
+
+let emit_tp loc tp =
+  match loc with
+  | Some loc ->
+    let* env = read in
+    let* qtp = quote_tp tp in
+    modify (St.add_type_at loc (Env.pp_env env) qtp)
+  | None ->
+    ret ()
+
+let emit_hole ctx tp =
+  let* env = read in
+  match Env.location env with
+  | Some loc -> 
+    let hole = St.Metadata.Hole { ctx; tp } in
+    modify (St.add_hole loc hole)
+  | None -> ret ()
diff --git a/src/core/RefineMonad.mli b/src/core/RefineMonad.mli
index e533d3481..5fd17535d 100644
--- a/src/core/RefineMonad.mli
+++ b/src/core/RefineMonad.mli
@@ -44,3 +44,6 @@ val with_pp : (Pp.env -> 'a m) -> 'a m
 val expected_connective : RefineError.connective -> D.tp -> 'a m
 val expected_field : D.sign -> S.t -> string list -> 'a m
 val field_names_mismatch : expected:string list list -> actual:string list list -> 'a m
+
+val emit_tp : LexingUtil.span option -> D.tp -> unit m
+val emit_hole : (Ident.t * S.tp) list -> S.tp -> unit m
diff --git a/src/core/RefineState.ml b/src/core/RefineState.ml
index 511ac1c6f..5ef3ff440 100644
--- a/src/core/RefineState.ml
+++ b/src/core/RefineState.ml
@@ -1,18 +1,43 @@
+open Basis
 open CodeUnit
 
 module IDMap = Map.Make (CodeUnitID)
 module D = Domain
+module S = Syntax
+
+module Metadata = struct
+  type hole = Hole of { ctx : (Ident.t * S.tp) list; tp : S.tp }
+
+  type t = { holes : (LexingUtil.span * hole) list;
+             type_spans : (LexingUtil.span * Pp.env * S.tp) list
+           }
+
+  let init : t = { holes = []; type_spans = [] }
+
+  let holes metadata = metadata.holes
+
+  let type_spans metadata = metadata.type_spans
+
+  let add_hole span hole t = { t with holes = (span, hole) :: t.holes }
+
+  let add_type_at span env tp t = { t with type_spans = (span, env, tp) :: t.type_spans }
+end
+
 
 type t = { code_units : CodeUnit.t IDMap.t;
            (** The binding namespace for each code unit. *)
            namespaces : (Global.t Namespace.t) IDMap.t;
            (** The import namespace for each code unit. *)
-           import_namespaces : (Global.t Namespace.t) IDMap.t }
+           import_namespaces : (Global.t Namespace.t) IDMap.t;
+           metadata : Metadata.t
+         }
 
 let init =
   { code_units = IDMap.empty;
     namespaces = IDMap.empty;
-    import_namespaces = IDMap.empty }
+    import_namespaces = IDMap.empty;
+    metadata = Metadata.init
+  }
 
 let get_unit id st =
   IDMap.find id st.code_units
@@ -57,10 +82,21 @@ let add_import id modifier import_id st =
 let init_unit id st =
   { code_units = IDMap.add id (CodeUnit.create id) st.code_units;
     namespaces = IDMap.add id Namespace.empty st.namespaces;
-    import_namespaces = IDMap.add id Namespace.empty st.import_namespaces }
+    import_namespaces = IDMap.add id Namespace.empty st.import_namespaces;
+    metadata = st.metadata
+  }
 
 let get_import path st =
   IDMap.find_opt path st.code_units
 
 let is_imported path st =
   IDMap.mem path st.code_units
+
+let add_hole span hole st =
+  { st with metadata = Metadata.add_hole span hole st.metadata }
+
+let add_type_at span env tp st =
+  { st with metadata = Metadata.add_type_at span env tp st.metadata }
+
+let get_metadata st =
+  st.metadata
diff --git a/src/core/RefineState.mli b/src/core/RefineState.mli
index 9f58e5d35..54aaba0e0 100644
--- a/src/core/RefineState.mli
+++ b/src/core/RefineState.mli
@@ -1,5 +1,7 @@
+open Basis
 open CodeUnit
 module D = Domain
+module S = Syntax
 
 type t
 
@@ -23,3 +25,17 @@ val is_imported : id -> t -> bool
 
 (** Create and add a new code unit. *)
 val init_unit : id -> t -> t
+
+
+module Metadata : sig
+  type hole = Hole of { ctx : (Ident.t * S.tp) list; tp : S.tp }
+
+  type t
+
+  val holes : t -> (LexingUtil.span * hole) list
+  val type_spans : t -> (LexingUtil.span * Pp.env * S.tp) list
+end
+
+val add_hole : LexingUtil.span -> Metadata.hole -> t -> t
+val add_type_at : LexingUtil.span -> Pp.env -> S.tp -> t -> t
+val get_metadata  : t -> Metadata.t
diff --git a/src/core/Refiner.ml b/src/core/Refiner.ml
index 49761fddd..5d967824b 100644
--- a/src/core/Refiner.ml
+++ b/src/core/Refiner.ml
@@ -68,14 +68,13 @@ module Probe : sig
   val probe_chk : string option -> T.Chk.tac -> T.Chk.tac
   val probe_boundary : T.Chk.tac -> T.Chk.tac -> T.Chk.tac
   val probe_syn : string option -> T.Syn.tac -> T.Syn.tac
+
+  val probe_goal_chk : ((Ident.t * S.tp) list -> S.tp -> unit RM.m) -> T.Chk.tac -> T.Chk.tac
+  val probe_goal_syn : ((Ident.t * S.tp) list -> S.tp -> unit RM.m) -> T.Syn.tac -> T.Syn.tac
 end =
 struct
-  let print_state lbl tp : unit m =
+  let print_state lbl ctx tp : unit m =
     let* env = RM.read in
-    let cells = Env.locals env in
-
-    RM.globally @@
-    let* ctx = GlobalUtil.destruct_cells @@ Bwd.to_list cells in
     () |> RM.emit (RefineEnv.location env) @@ fun fmt () ->
     Format.fprintf fmt "Emitted hole:@,  @[<v>%a@]@." (S.pp_sequent ~lbl ctx) tp
 
@@ -98,15 +97,38 @@ struct
     () |> RM.emit (RefineEnv.location env) @@ fun fmt () ->
     Format.fprintf fmt "Emitted hole:@,  @[<v>%a@]@." (S.pp_partial_sequent bdry_sat ctx) (tm, stp)
 
-  let probe_chk name tac =
-    T.Chk.brule ~name:"probe_chk" @@ fun (tp, phi, clo) ->
+  let probe_goal_chk k tac =
+    T.Chk.brule ~name:"probe_goal_chk" @@ fun (tp, phi, clo) ->
     let* s = T.Chk.brun tac (tp, phi, clo) in
     let+ () =
       let* stp = RM.quote_tp @@ D.Sub (tp, phi, clo) in
-      print_state name stp
+
+      let* env = RM.read in
+      let cells = Env.locals env in
+      RM.globally @@
+      let* ctx = GlobalUtil.destruct_cells @@ Bwd.to_list cells in
+      k ctx stp
     in
     s
 
+  let probe_goal_syn k tac =
+    T.Syn.rule ~name:"probe_goal_syn" @@
+    let* s, tp = T.Syn.run tac in
+    let+ () =
+      let* stp = RM.quote_tp tp in
+      let* env = RM.read in
+      let cells = Env.locals env in
+      RM.globally @@
+      let* ctx = GlobalUtil.destruct_cells @@ Bwd.to_list cells in
+      k ctx stp
+    in
+    s, tp
+
+  let probe_chk name tac =
+    (* FIXME: We shouldn't print here, as that would muck up stdout for the Language Server *)
+    (* probe_goal_chk (print_state name) tac *)
+    probe_goal_chk RM.emit_hole tac
+
   let probe_boundary probe tac =
     T.Chk.brule ~name:"probe_boundary" @@ fun (tp, phi, clo) ->
     let* probe_tm = T.Chk.run probe tp in
@@ -114,13 +136,7 @@ struct
     T.Chk.brun tac (tp, phi, clo)
 
   let probe_syn name tac =
-    T.Syn.rule ~name:"probe_syn" @@
-    let* s, tp = T.Syn.run tac in
-    let+ () =
-      let* stp = RM.quote_tp tp in
-      print_state name stp
-    in
-    s, tp
+    probe_goal_syn (print_state name) tac
 end
 
 
diff --git a/src/core/Refiner.mli b/src/core/Refiner.mli
index 30d0f64b9..5478f7bce 100644
--- a/src/core/Refiner.mli
+++ b/src/core/Refiner.mli
@@ -1,6 +1,8 @@
 (** This is the basis of trusted inference rules for cooltt. This module also contains
     some auxiliary tactics, but these don't need to be trusted so they should be moved elsewhere. *)
 
+open CodeUnit
+
 module D := Domain
 module S := Syntax
 module RM := Monads.RefineM
@@ -23,6 +25,9 @@ module Probe : sig
   val probe_chk : string option -> Chk.tac -> Chk.tac
   val probe_boundary : Chk.tac -> Chk.tac -> Chk.tac
   val probe_syn : string option -> Syn.tac -> Syn.tac
+
+  val probe_goal_chk : ((Ident.t * S.tp) list -> S.tp -> unit RM.m) -> Chk.tac -> Chk.tac
+  val probe_goal_syn : ((Ident.t * S.tp) list -> S.tp -> unit RM.m) -> Syn.tac -> Syn.tac
 end
 
 module Dim : sig
diff --git a/src/core/Syntax.ml b/src/core/Syntax.ml
index 803ff1c10..518a726d6 100644
--- a/src/core/Syntax.ml
+++ b/src/core/Syntax.ml
@@ -521,6 +521,9 @@ struct
         (pp_tp envx P.(right_of times)) fam
     | Signature fields ->
       Format.fprintf fmt "sig %a" (pp_sign env) fields
+    | Sub (tp, Cof (Cof.Join []), _) ->
+      Format.fprintf fmt "%a"
+        (pp_tp env penv) tp
     | Sub (tp, phi, tm) ->
       let _x, envx = ppenv_bind env `Anon in
       Format.fprintf fmt "@[sub %a %a@ %a@]"
diff --git a/src/core/Tactic.ml b/src/core/Tactic.ml
index 0f291b01c..b4bbc459a 100644
--- a/src/core/Tactic.ml
+++ b/src/core/Tactic.ml
@@ -142,9 +142,11 @@ struct
     function
     | Chk (name, tac) ->
       rule ~name @@ fun tp ->
+      let* _ = RM.emit_tp loc tp in
       RM.update_span loc @@ tac tp
     | BChk (name, tac) ->
-      brule ~name @@ fun goal ->
+      brule ~name @@ fun ((tp, cof, bdry) as goal) ->
+      let* _ = RM.emit_tp loc (D.Sub (tp, cof, bdry)) in
       RM.update_span loc @@ tac goal
 
   let syn (tac : Syn.tac) : tac =
@@ -176,7 +178,12 @@ struct
     tac
 
   let update_span loc (name, tac) =
-    (name, RM.update_span loc tac)
+    let tac' =
+      let* (tm, tp) = RM.update_span loc tac in
+      let+ _ = RM.emit_tp loc tp in
+      (tm, tp)
+    in
+    (name, tac')
 
   let ann (tac_tm : Chk.tac) (tac_tp : Tp.tac) : tac =
     rule @@
diff --git a/src/frontend/ConcreteSyntaxData.ml b/src/frontend/ConcreteSyntaxData.ml
index e51de7194..5b2275c5b 100644
--- a/src/frontend/ConcreteSyntaxData.ml
+++ b/src/frontend/ConcreteSyntaxData.ml
@@ -45,6 +45,7 @@ and con_ =
   | Type
   | Hole of string option * con option
   | BoundaryHole of con option
+  | Visualize
   | Underscore
   | Unfold of Ident.t list * con
   | Generalize of Ident.t * con
diff --git a/src/frontend/Driver.ml b/src/frontend/Driver.ml
index 8f8f0b7d6..b0b6f5a5a 100644
--- a/src/frontend/Driver.ml
+++ b/src/frontend/Driver.ml
@@ -16,6 +16,11 @@ module ST = RefineState
 module RMU = Monad.Util (RM)
 open Monad.Notation (RM)
 
+type options =
+  { as_file : string option;
+    debug_mode : bool;
+  }
+
 type status = (unit, unit) Result.t
 type continuation = Continue of (status RM.m -> status RM.m) | Quit
 type command = continuation RM.m
@@ -209,7 +214,7 @@ and process_file input =
     Log.pp_error_message ~loc:(Some err.span) ~lvl:`Error pp_message @@ ErrorMessage {error = LexingError; last_token = err.last_token};
     RM.ret @@ Error ()
 
-let load_file ~as_file ~debug_mode input =
+let load_file {as_file; debug_mode} input =
   match load_current_library ~as_file input with
   | Error () -> Error ()
   | Ok lib ->
@@ -244,7 +249,7 @@ let rec repl lib (ch : in_channel) lexbuf =
       close_in ch;
       RM.ret @@ Ok ()
 
-let do_repl ~as_file ~debug_mode =
+let do_repl {as_file; debug_mode; _} =
   match load_current_library ~as_file `Stdin with
   | Error () -> Error ()
   | Ok lib ->
diff --git a/src/frontend/Driver.mli b/src/frontend/Driver.mli
index 64506c06c..121818c27 100644
--- a/src/frontend/Driver.mli
+++ b/src/frontend/Driver.mli
@@ -1,4 +1,11 @@
 (* This is the top-level driver for the proof assistant. *)
+open Basis
+open Core
 
-val load_file : as_file:string option -> debug_mode:bool -> [`Stdin | `File of string] -> (unit, unit) result
-val do_repl : as_file:string option -> debug_mode:bool -> (unit, unit) result
+type options =
+  { as_file : string option;
+    debug_mode : bool;
+  }
+
+val load_file : options -> [`Stdin | `File of string] -> (unit, unit) result
+val do_repl : options -> (unit, unit) result
diff --git a/src/frontend/Elaborator.ml b/src/frontend/Elaborator.ml
index 1df594007..aaf92fc3a 100644
--- a/src/frontend/Elaborator.ml
+++ b/src/frontend/Elaborator.ml
@@ -212,6 +212,7 @@ and chk_tm : CS.con -> T.Chk.tac =
   | CS.Hole (name, Some con) -> Refiner.Probe.probe_chk name @@ chk_tm con
   | CS.BoundaryHole None -> Refiner.Hole.unleash_hole None
   | CS.BoundaryHole (Some con) -> Refiner.Probe.probe_boundary (chk_tm con) (Refiner.Hole.silent_hole None)
+  | CS.Visualize -> Refiner.Probe.probe_goal_chk (fun ctx goal -> RM.ret ()) @@ Refiner.Hole.unleash_hole None
   | CS.Unfold (idents, c) ->
     (* TODO: move to a trusted rule *)
     T.Chk.brule @@
@@ -449,3 +450,12 @@ let rec modifier_ (con : CS.con) =
 
 let modifier con =
   Option.fold ~none:(RM.ret Yuujinchou.Pattern.any) ~some:modifier_ con
+
+(* Helpers *)
+let elaborate_typed_term name (args : CS.cell list) tp tm =
+  RM.push_problem name @@
+  let* tp = RM.push_problem "tp" @@ T.Tp.run @@ chk_tp_in_tele args tp in
+  let* vtp = RM.lift_ev @@ Sem.eval_tp tp in
+  let* tm = RM.push_problem "tm" @@ T.Chk.run (chk_tm_in_tele args tm) vtp in
+  let+ vtm = RM.lift_ev @@ Sem.eval tm in
+  vtp, vtm
diff --git a/src/frontend/Elaborator.mli b/src/frontend/Elaborator.mli
index 6a8296144..c12abaf25 100644
--- a/src/frontend/Elaborator.mli
+++ b/src/frontend/Elaborator.mli
@@ -1,4 +1,5 @@
 open Core
+open CodeUnit
 module CS := ConcreteSyntax
 module S := Syntax
 module RM := Monads.RefineM
@@ -12,3 +13,5 @@ val chk_tm : CS.con -> Chk.tac
 val chk_tm_in_tele : CS.cell list -> CS.con -> Chk.tac
 val syn_tm : CS.con -> Syn.tac
 val modifier : CS.con option -> [> `Print of string option] Yuujinchou.Pattern.t RM.m
+
+val elaborate_typed_term : string -> CS.cell list -> CS.con -> CS.con -> (D.tp * D.con) RM.m
diff --git a/src/frontend/Grammar.mly b/src/frontend/Grammar.mly
index 4a7f023ba..d8b3ac09d 100644
--- a/src/frontend/Grammar.mly
+++ b/src/frontend/Grammar.mly
@@ -46,6 +46,7 @@
 %token EXT
 %token COE COM HCOM HFILL
 %token QUIT NORMALIZE PRINT DEF AXIOM FAIL
+%token VISUALIZE
 %token <string list> IMPORT
 %token ELIM
 %token SEMISEMI EOF
@@ -236,6 +237,8 @@ plain_atomic_term_except_name:
     { Type }
   | name = HOLE_NAME
     { Hole (name, None) }
+  | VISUALIZE
+    { Visualize }
   | DIM
     { Dim }
   | COF
diff --git a/src/frontend/Lex.mll b/src/frontend/Lex.mll
index 0ae79f40d..c4f688165 100644
--- a/src/frontend/Lex.mll
+++ b/src/frontend/Lex.mll
@@ -22,6 +22,7 @@ let commands =
       ("#fail", FAIL);
       ("#normalize", NORMALIZE);
       ("#print", PRINT);
+      ("#viz", VISUALIZE);
       ("#quit", QUIT);
     ]
 
diff --git a/src/frontend/dune b/src/frontend/dune
index a13d5edc8..8d5b22b9f 100644
--- a/src/frontend/dune
+++ b/src/frontend/dune
@@ -6,7 +6,7 @@
 
 (library
  (name Frontend)
- (libraries bantorra cooltt.basis cooltt.cubical cooltt.core menhirLib)
+ (libraries bantorra cooltt.basis cooltt.cubical cooltt.core ezjsonm menhirLib)
  (preprocess
   (pps ppx_deriving.std))
  (flags
diff --git a/src/server/Actions.ml b/src/server/Actions.ml
new file mode 100644
index 000000000..782a9c383
--- /dev/null
+++ b/src/server/Actions.ml
@@ -0,0 +1,118 @@
+open Basis
+open Bwd
+open Frontend
+open Core
+open CodeUnit
+open Cubical
+
+module S = Syntax
+module D = Domain
+
+open Lsp.Types
+module Json = Lsp.Import.Json
+
+module LwtIO = Lwt_io
+
+open LspLwt.Notation
+
+(* FIXME: This should live elsewhere, we use this a lot. *)
+let ppenv_bind env ident =
+  Pp.Env.bind env @@ Ident.to_string_opt ident
+
+module Visualize = struct
+  let command_name = "cooltt.visualize"
+  let action_kind = CodeActionKind.Other "cooltt.visualize.hole"
+
+  let serialize_label (str : string) (pos : (string * float) list) : Json.t =
+    `Assoc [
+      "position", `Assoc (List.map (fun (nm, d) -> (nm, `Float d)) pos);
+      "txt", `String str
+    ]
+
+  let dim_tm : S.t -> float =
+    function
+    | S.Dim0 -> -. 1.0
+    | S.Dim1 -> 1.0
+    | _ -> failwith "dim_tm: bad dim"
+
+  let rec dim_from_cof (dims : (string option) bwd) (cof : S.t) : (string * float) list list =
+    match cof with
+    | S.Cof (Cof.Eq (S.Var v, r)) ->
+      let axis = Option.get @@ Bwd.nth dims v in
+      let d = dim_tm r in
+      [[(axis, d)]]
+    | S.Cof (Cof.Join cofs) -> List.concat_map (dim_from_cof dims) cofs
+    | S.Cof (Cof.Meet cofs) -> [List.concat @@ List.concat_map (dim_from_cof dims) cofs]
+    | _ -> failwith "dim_from_cof: bad cof"
+
+  let boundary_labels dims env bdry =
+    let rec go env dims (bdry, cons) =
+      match cons with
+      | S.CofSplit branches ->
+        let (_x, envx) = ppenv_bind env `Anon in
+        List.concat_map (go envx (Snoc (dims, None))) branches
+      | _ ->
+        let (_x, envx) = ppenv_bind env `Anon in
+        let lbl = Format.asprintf "%a" (S.pp envx) cons in
+        List.map (serialize_label lbl) @@ dim_from_cof (Snoc (dims, None)) bdry
+    in
+    match bdry with
+    | S.CofSplit branches ->
+      let (_x, envx) = ppenv_bind env `Anon in
+      List.concat_map (go envx dims) branches
+    | _ -> []
+
+  let serialize_boundary ctx goal : Json.t option =
+    let rec go dims env =
+      function
+      | [] ->
+        begin
+          match goal with
+          | S.Sub (_, _, bdry) ->
+            let dim_names = Bwd.to_list @@ Bwd.filter_map (Option.map (fun name -> `String name)) dims in
+            let labels = boundary_labels dims env bdry in
+            let context = Format.asprintf "%a" (S.pp_sequent ~lbl:None ctx) goal in
+            let msg = `Assoc [
+                ("dims", `List dim_names);
+                ("labels", `List labels);
+                ("context", `String context)
+              ]
+            in Some (`Assoc ["DisplayGoal", msg])
+          | _ -> None
+        end
+      | (var, var_tp) :: ctx ->
+        let (dim_name, envx) = ppenv_bind env var in
+        match var_tp with
+        | S.TpDim -> go (Snoc (dims, Some dim_name)) envx ctx
+        | _ -> go (Snoc (dims, None)) envx ctx
+    in go Emp Pp.Env.emp ctx
+
+  let create ctx goal =
+    serialize_boundary ctx goal |> Option.map @@ fun json ->
+    let command = Command.create
+        ~title:"visualize"
+        ~command:command_name
+        ~arguments:[json]
+        ()
+    in CodeAction.create
+      ~title:"visualize hole"
+      ~kind:action_kind
+      ~command
+      ()
+
+  let execute arguments =
+    match arguments with
+    | Some [arg] ->
+      (* FIXME: Handle the visualizer socket better *)
+      let host = Unix.gethostbyname "localhost" in
+      let host_entry = Array.get host.h_addr_list 0 in
+      let addr = Unix.ADDR_INET (host_entry, 3001) in
+      let* (ic, oc) = LwtIO.open_connection addr in
+      let* _ = LwtIO.write oc (Json.to_string arg) in
+      let* _ = LwtIO.flush oc in
+      let* _ = LwtIO.close ic in
+      LwtIO.close oc
+    | _ ->
+      (* FIXME: Handle this better *)
+      Lwt.return ()
+end
diff --git a/src/server/Actions.mli b/src/server/Actions.mli
new file mode 100644
index 000000000..2a694bd28
--- /dev/null
+++ b/src/server/Actions.mli
@@ -0,0 +1,11 @@
+open Basis
+open Core
+open CodeUnit
+
+module Json = Lsp.Import.Json
+
+module Visualize : sig
+  val command_name : string
+  val create : (Ident.t * Syntax.tp) list -> Syntax.tp -> Lsp.Types.CodeAction.t option
+  val execute : Json.t list option -> unit Lwt.t
+end
diff --git a/src/server/Executor.ml b/src/server/Executor.ml
new file mode 100644
index 000000000..181ea216f
--- /dev/null
+++ b/src/server/Executor.ml
@@ -0,0 +1,108 @@
+open Basis
+open Core
+open Frontend
+
+open CodeUnit
+open DriverMessage
+
+module CS = ConcreteSyntax
+module ST = RefineState
+module Err = RefineError
+module Env = RefineEnv
+module Metadata = RefineMetadata
+module RM = RefineMonad
+open Monad.Notation (RM)
+
+open Lsp.Types
+
+(* State *)
+
+type state = { refiner_state : RefineState.t;
+               refiner_env : RefineEnv.t;
+               diagnostics : Diagnostic.t list
+             }
+
+let diagnostic severity info message =
+  match Option.map Pos.located info with
+  | Some range -> Diagnostic.create ~range ~severity ~message ()
+  | None -> failwith "[FIXME] Basis.Basis.diagnostic: Handle missing locations"
+
+(* Effects *)
+
+(** Lift a refiner computation into an LWT promise. *)
+let lift_rm (st : state) (m : 'a RM.m) : ('a * state) Lwt.t =
+  st |> Lwt.wrap1 @@ fun st ->
+  RM.run_exn st.refiner_state st.refiner_env @@
+  let* r = m in
+  let+ refiner_state = RM.get in
+  r, { st with refiner_state }
+
+let lift_rm_ st m =
+  Lwt.map snd (lift_rm st m)
+
+(* Actions *)
+
+(** Parse a file. *)
+let parse_file (path : string) =
+  path |> Lwt.wrap1 @@ fun path ->
+  (* FIXME: proper error handling here *)
+  Result.get_ok @@ Load.load_file (`File path)
+
+(** Elaborate a single definition. *)
+let elab_definition (st : state) (name : Ident.t) (args : CS.cell list) (tp : CS.con) (def : CS.con) =
+  lift_rm_ st @@
+  let* (tp, tm) = Elaborator.elaborate_typed_term (Ident.to_string name) args tp def in
+  let+ _ = RM.add_global name tp (Some tm) in
+  ()
+
+(* NOTE: Maybe it makes sense to rethink how messaging works *)
+let print_ident (st : state) (ident : Ident.t CS.node) =
+  let action =
+    let* x = RM.resolve ident.node in
+    match x with
+    | `Global sym ->
+      let* vtp, con = RM.get_global sym in
+      let* tp = RM.quote_tp vtp in
+      let* tm =
+        match con with
+        | None -> RM.ret None
+        | Some con ->
+          let* tm = RM.quote_con vtp con in
+          RM.ret @@ Some tm
+      in
+      (* [TODO: Reed M, 24/11/2021] Rethink messaging? *)
+      let msg = Format.asprintf "%a"
+          pp_message @@ OutputMessage (Definition { ident = ident.node; tp; tm })
+      in
+      RM.ret @@ diagnostic DiagnosticSeverity.Information ident.info msg
+    | _ ->  RM.ret @@ diagnostic DiagnosticSeverity.Error ident.info "Unbound identifier"
+  in
+  lift_rm st action |> Lwt.map @@ fun (d, st) -> { st with diagnostics = d::st.diagnostics }
+
+(* FIXME: Handle the rest of the commands *)
+let elab_decl (st : state) (decl : CS.decl) =
+  match decl with
+  | CS.Def { name; args; def = Some def; tp } ->
+    begin
+      Lwt.catch (fun () -> elab_definition st name args tp def) @@
+      function
+      | Err.RefineError (e, span) ->
+        let msg = Format.asprintf "%a" Err.pp e in
+        let d = diagnostic DiagnosticSeverity.Error span msg in
+        Lwt.return { st with diagnostics = d :: st.diagnostics }
+      | err -> raise err
+    end
+  | CS.Print ident ->
+    print_ident st ident
+  | _ -> Lwt.return st
+
+let elaborate_file (lib : Bantorra.Manager.library) (path : string) : (Diagnostic.t list * ST.Metadata.t) Lwt.t =
+  let open LspLwt.Notation in
+  let* sign = parse_file path in
+  let unit_id = CodeUnitID.file path in
+  (* [TODO: Reed M, 24/11/2021] I don't love how the code unit stuff works here, perhaps it's time to rethink? *)
+  let refiner_state = ST.init_unit unit_id @@ ST.init in
+  let refiner_env = Env.set_current_unit_id unit_id (Env.init lib) in
+  let diagnostics = [] in
+  let+ st = Lwt_list.fold_left_s elab_decl { refiner_state; refiner_env; diagnostics } sign in
+  (st.diagnostics, ST.get_metadata st.refiner_state)
diff --git a/src/server/Executor.mli b/src/server/Executor.mli
new file mode 100644
index 000000000..0b21b2ab1
--- /dev/null
+++ b/src/server/Executor.mli
@@ -0,0 +1,4 @@
+open Basis
+open Core
+
+val elaborate_file : Bantorra.Manager.library -> string -> (Lsp.Types.Diagnostic.t list * RefineState.Metadata.t) Lwt.t
diff --git a/src/server/LanguageServer.ml b/src/server/LanguageServer.ml
new file mode 100644
index 000000000..301933f0d
--- /dev/null
+++ b/src/server/LanguageServer.ml
@@ -0,0 +1,321 @@
+open Basis
+open Bwd
+open Frontend
+open Core
+open CodeUnit
+open Cubical
+
+module S = Syntax
+module D = Domain
+module Metadata = RefineState.Metadata
+module RangeTree = SegmentTree.Make(Pos)
+
+open Lsp.Types
+
+module RPC = Jsonrpc
+module Request = Lsp.Client_request
+module Notification = Lsp.Client_notification
+module Broadcast = Lsp.Server_notification
+module Json = Lsp.Import.Json
+
+type rpc_message = RPC.Id.t option RPC.Message.t
+type rpc_request = RPC.Message.request
+type rpc_notification = RPC.Message.notification
+
+type 'resp request = 'resp Lsp.Client_request.t
+type notification = Lsp.Client_notification.t
+
+type server =
+  { lsp_io : LspLwt.io;
+    library : Bantorra.Manager.library;
+    (* FIXME: We should probably thread this through. *)
+    should_shutdown : bool;
+    hover_info : string RangeTree.t;
+    holes : RefineState.Metadata.hole RangeTree.t
+  }
+
+type lsp_error =
+  | DecodeError of string
+  | HandshakeError of string
+  | ShutdownError of string
+  | UnknownRequest of string
+  | UnknownNotification of string
+
+exception LspError of lsp_error
+
+let () = Printexc.register_printer @@
+  function
+  | LspError (DecodeError err) -> Some (Format.asprintf "Lsp Error: Couldn't decode %s" err)
+  | LspError (HandshakeError err) -> Some (Format.asprintf "Lsp Error: Invalid initialization handshake %s" err)
+  | LspError (ShutdownError err) -> Some (Format.asprintf "Lsp Error: Invalid shutdown sequence %s" err)
+  | LspError (UnknownRequest err) -> Some (Format.asprintf "Lsp Error: Unknown request %s" err)
+  | LspError (UnknownNotification err) -> Some (Format.asprintf "Lsp Error: Unknown notification %s" err)
+  | _ -> None
+
+open LspLwt.Notation
+
+(* Server Notifications *)
+let broadcast server notif =
+  let msg = Broadcast.to_jsonrpc notif in
+  LspLwt.send server.lsp_io (RPC.Message { msg with id = None })
+
+let publish_diagnostics server path (diagnostics : Diagnostic.t list) =
+  let uri = DocumentUri.of_path path in
+  let params = PublishDiagnosticsParams.create ~uri ~diagnostics () in
+  broadcast server (PublishDiagnostics params)
+
+
+(* Notifications *)
+
+let update_metadata server metadata =
+  let hover_info : string RangeTree.t =
+    Metadata.type_spans metadata
+    |> List.map (fun (span, ppenv, tp) -> (Pos.of_lex_span span, Format.asprintf "%a" (Syntax.pp_tp ppenv) tp))
+    |> RangeTree.of_list
+  in
+  let holes =
+    Metadata.holes metadata
+    |> List.map (fun (span, hole) -> (Pos.of_lex_span span, hole))
+    |> RangeTree.of_list
+  in
+  { server with hover_info; holes }
+
+let load_file server (uri : DocumentUri.t) : server Lwt.t =
+  let path = DocumentUri.to_path uri in
+  let* _ = LspLwt.log server.lsp_io "Loading File: %s" path in
+  let* (diagnostics, metadata) = Executor.elaborate_file server.library path in
+  let+ _ = publish_diagnostics server path diagnostics in
+  update_metadata server metadata
+
+let handle_notification : server -> string -> notification -> server Lwt.t =
+  fun server mthd ->
+  function
+  | TextDocumentDidOpen doc ->
+    load_file server doc.textDocument.uri
+  | DidSaveTextDocument doc ->
+    load_file server doc.textDocument.uri
+  | _ ->
+    raise (LspError (UnknownNotification mthd))
+
+(* Code Actions/Commands *)
+let supported_commands = ["cooltt.visualize"]
+
+(* Requests *)
+
+let hover server (opts : HoverParams.t) =
+  RangeTree.lookup (Pos.of_lsp_pos opts.position) server.hover_info |> Option.map @@ fun info ->
+  Hover.create ~contents:(`MarkedString { value = info; language = None }) ()
+
+let codeAction server (opts : CodeActionParams.t) =
+  let holes = RangeTree.containing (Pos.of_lsp_pos opts.range.start) server.holes in
+  let actions =
+    holes |> List.filter_map @@ fun (Metadata.Hole {ctx; tp}) ->
+    Actions.Visualize.create ctx tp
+    |> Option.map @@ fun action -> `CodeAction action
+
+  in
+  Lwt.return @@ (Some actions, server)
+
+let executeCommand server (opts : ExecuteCommandParams.t) =
+  let* _ = Actions.Visualize.execute opts.arguments in
+  let ppargs = Format.asprintf "%a" (Format.pp_print_option (Format.pp_print_list Json.pp)) opts.arguments in
+  let+ _ = LspLwt.log server.lsp_io "Execute Command: %s %s" opts.command ppargs in
+  (`Null, server)
+
+let handle_request : type resp. server -> string -> resp request -> (resp * server) Lwt.t =
+  fun server mthd ->
+  function
+  | Initialize _ ->
+    raise (LspError (HandshakeError "Server can only recieve a single initialization request."))
+  | Shutdown ->
+    Lwt.return ((), { server with should_shutdown = true })
+  | TextDocumentHover opts ->
+    Lwt.return @@ (hover server opts, server)
+  | CodeAction opts -> codeAction server opts
+  | ExecuteCommand opts -> executeCommand server opts
+  | _ -> raise (LspError (UnknownRequest mthd))
+
+(* Main Event Loop *)
+let on_notification server (notif : rpc_notification) =
+  let* _ = LspLwt.log server.lsp_io "Notification: %s" notif.method_ in
+  match Notification.of_jsonrpc notif with
+  | Ok n -> handle_notification server notif.method_ n
+  | Error err ->
+    raise (LspError (DecodeError err))
+
+let on_request server (req : rpc_request) : (RPC.Response.t * server) Lwt.t =
+  let* _ = LspLwt.log server.lsp_io "Request: %s" req.method_ in
+  match Request.of_jsonrpc req with
+  | Ok (E r) ->
+    let+ (resp, server) = handle_request server req.method_ r in
+    let json = Request.yojson_of_result r resp in
+    (RPC.Response.ok req.id json, server)
+  | Error err ->
+    raise (LspError (DecodeError err))
+
+let on_message server (msg : rpc_message) : server Lwt.t =
+  match msg.id with
+  | None -> on_notification server { msg with id = () }
+  | Some id ->
+    let* (resp, server) = on_request server { msg with id } in
+    let+ _ = LspLwt.send server.lsp_io (RPC.Response resp) in
+    server
+
+(** Attempt to recieve a request from the client. *)
+let recv_request lsp_io =
+  let+ msg = LspLwt.recv lsp_io in
+  Option.bind msg @@
+  function
+  | (Jsonrpc.Message ({ id = Some id; _ } as msg)) -> Some { msg with id }
+  | _ -> None
+
+(** Attempt to recieve a notification from the client. *)
+let recv_notification lsp_io =
+  let+ msg = LspLwt.recv lsp_io in
+  Option.bind msg @@
+  function
+  | (Jsonrpc.Message ({ id = None; _ } as msg)) -> Some { msg with id = () }
+  | _ -> None
+
+(* Initialization *)
+
+let server_capabilities =
+  let textDocumentSync =
+    let opts = TextDocumentSyncOptions.create
+        ~change:(TextDocumentSyncKind.None)
+        ~save:(`SaveOptions (SaveOptions.create ~includeText:false ()))
+        ()
+    in
+    `TextDocumentSyncOptions opts
+  in
+  let hoverProvider =
+    let opts = HoverOptions.create ()
+    in `HoverOptions opts
+  in
+  let codeActionProvider =
+    let opts = CodeActionOptions.create ~codeActionKinds:[CodeActionKind.Other "cooltt.hole.visualize"] () in
+    `CodeActionOptions opts
+  in
+  let executeCommandProvider =
+    ExecuteCommandOptions.create ~commands:supported_commands ()
+  in
+  ServerCapabilities.create
+    ~textDocumentSync
+    ~hoverProvider
+    ~codeActionProvider
+    ~executeCommandProvider
+    ()
+
+let library_manager =
+  match Bantorra.Manager.init ~anchor:"cooltt-lib" ~routers:[] with
+  | Ok ans -> ans
+  | Error (`InvalidRouter err) -> raise (LspError (HandshakeError err)) (* this should not happen! *)
+
+let initialize_library root =
+  match
+    match root with
+    | Some path -> Bantorra.Manager.load_library_from_dir library_manager path
+    | None -> Bantorra.Manager.load_library_from_cwd library_manager
+  with
+  | Ok (lib, _) -> lib
+  | Error (`InvalidLibrary err) -> raise (LspError (HandshakeError err))
+
+let get_root (init_params : InitializeParams.t) : string option =
+  match init_params.rootUri with
+  | Some uri -> Some (DocumentUri.to_path uri)
+  | None -> Option.join init_params.rootPath
+
+(** Perform the LSP initialization handshake.
+    https://microsoft.github.io/language-server-protocol/specifications/specification-current/#initialize *)
+let initialize lsp_io =
+  let* req = recv_request lsp_io in
+  match req with
+  | Some req ->
+    begin
+      match Request.of_jsonrpc req with
+      | Ok (E (Initialize init_params as init_req)) ->
+        let* _ = LspLwt.log lsp_io "Initializing..." in
+        let resp = InitializeResult.create ~capabilities:server_capabilities () in
+        let json = Request.yojson_of_result init_req resp in
+        let* _ = LspLwt.send lsp_io (RPC.Response (RPC.Response.ok req.id json)) in
+        let* notif = recv_notification lsp_io in
+        begin
+          match notif with
+          | Some notif ->
+            begin
+              match Notification.of_jsonrpc notif with
+              | Ok Initialized ->
+                let root = get_root init_params in
+                let+ _ = LspLwt.log lsp_io "Root: %s" (Option.value root ~default:"<no-root>") in
+                { lsp_io;
+                  should_shutdown = false;
+                  library = initialize_library root;
+                  hover_info = RangeTree.empty;
+                  holes = RangeTree.empty
+                }
+              | _ ->
+                raise (LspError (HandshakeError "Initialization must complete with an initialized notification."))
+            end
+          | None ->
+            raise (LspError (HandshakeError "Initialization must complete with an initialized notification."))
+        end
+      | Ok (E _) ->
+        raise (LspError (HandshakeError "Initialization must begin with an initialize request."))
+      | Error err ->
+        raise (LspError (HandshakeError err))
+    end
+  | None ->
+    raise (LspError (HandshakeError "Initialization must begin with a request."))
+
+(* Shutdown *)
+
+(** Perform the LSP shutdown sequence.
+    See https://microsoft.github.io/language-server-protocol/specifications/specification-current/#exit *)
+let shutdown server =
+  let* notif = recv_notification server.lsp_io in
+  match notif with
+  | Some notif ->
+    begin
+      match Notification.of_jsonrpc notif with
+      | Ok Exit ->
+        Lwt.return ()
+      | Ok _ ->
+        raise (LspError (ShutdownError "The only notification that can be recieved after a shutdown request is exit."))
+      | Error err -> 
+        raise (LspError (ShutdownError err))
+    end
+  | None ->
+    raise (LspError (ShutdownError "No requests can be recieved after a shutdown request."))
+
+let print_exn lsp_io exn =
+  let msg = Printexc.to_string exn
+  and stack = Printexc.get_backtrace () in
+  LspLwt.log lsp_io "%s\n%s" msg stack
+
+let rec event_loop server =
+  let* msg = LspLwt.recv server.lsp_io in
+  match msg with
+  | Some (Jsonrpc.Message msg) ->
+    let* server = Lwt.catch
+        (fun () -> on_message server msg)
+        (fun exn -> Lwt.map (fun _ -> server) (print_exn server.lsp_io exn))
+    in
+    if server.should_shutdown
+    then
+      shutdown server
+    else 
+      event_loop server
+  | _ ->
+    let+ _ = LspLwt.log server.lsp_io "Recieved an invalid message. Shutting down..." in
+    ()
+
+
+let run () =
+  let () = Printexc.record_backtrace true in
+  let lsp_io = LspLwt.init () in
+  let action =
+    let* server = initialize lsp_io in
+    event_loop server
+  in
+  let _ = Lwt_main.run @@ Lwt.catch (fun () -> action) (print_exn lsp_io) in
+  Ok ()
diff --git a/src/server/LanguageServer.mli b/src/server/LanguageServer.mli
new file mode 100644
index 000000000..a67608424
--- /dev/null
+++ b/src/server/LanguageServer.mli
@@ -0,0 +1 @@
+val run : unit -> (unit, unit) result
diff --git a/src/server/LspLwt.ml b/src/server/LspLwt.ml
new file mode 100644
index 000000000..3b7774da6
--- /dev/null
+++ b/src/server/LspLwt.ml
@@ -0,0 +1,132 @@
+(** LSP Server IO, implemented using LWT. *)
+module LwtIO = Lwt_io
+open Lsp.Import
+
+type io = { ic : LwtIO.input_channel;
+            oc : LwtIO.output_channel;
+            logc : LwtIO.output_channel
+          }
+
+let init () =
+  { ic = LwtIO.stdin; oc = LwtIO.stdout; logc = LwtIO.stderr }
+
+module Notation = struct
+  let (let*) = Lwt.bind
+  let (let+) m f = Lwt.map f m 
+  let (and*) = Lwt.both
+end
+
+open Notation
+
+(* Logging *)
+
+(** Log out a message to stderr. *)
+let log (io : io) (msg : ('a, unit, string, unit Lwt.t) format4) : 'a =
+  LwtIO.fprintlf io.logc msg
+
+(** See https://microsoft.github.io/language-server-protocol/specifications/specification-current/#headerPart *)
+module Header = struct
+  type t = { content_length : int;
+             content_type : string
+           }
+
+  let empty = { content_length = -1;
+                content_type = "application/vscode-jsonrpc; charset=utf-8"
+              }
+
+  let create ~(content_length : int) : t =
+    { empty with content_length }
+
+  let is_content_length key =
+    String.equal (String.lowercase_ascii @@ String.trim key) "content-length" 
+
+  let is_content_type key =
+    String.equal (String.lowercase_ascii @@ String.trim key) "content-type" 
+
+  (* NOTE: We should never really recieve an invalid header, as
+     that would indicate a broken client implementation. Therefore,
+     we just bail out when we see an invalid header, as there's 
+     way we can really recover anyways. *)
+  type header_error =
+    | InvalidHeader of string
+    | InvalidContentLength of string
+
+  exception HeaderError of header_error
+
+  let () = Printexc.register_printer @@
+    function
+    | HeaderError (InvalidHeader err) -> Some (Format.asprintf "HeaderError: Invalid Header %s" err)
+    | HeaderError (InvalidContentLength n) -> Some (Format.asprintf "HeaderError: Invalid Content Length '%s'" n)
+    | _ -> None
+
+  (** Read the header section of an LSP message. *)
+  let read (io : io) : t Lwt.t =
+    let rec loop headers =
+      Lwt.bind (LwtIO.read_line io.ic) @@
+      function
+      | "" -> Lwt.return headers
+      | line ->
+        match String.split_on_char ~sep:':' @@ String.trim line with
+        | [key; value] when is_content_length key ->
+          let content_length =
+            match int_of_string_opt (String.trim value) with
+            | Some n -> n
+            | None -> raise (HeaderError (InvalidContentLength value))
+          in loop { headers with content_length }
+        | [key; value] when is_content_type key ->
+          let content_type = String.trim value in
+          loop { headers with content_type }
+        | [_; _] -> loop headers
+        | _ ->
+          raise (HeaderError (InvalidHeader line))
+    in
+    loop empty |> Lwt.map @@ fun headers ->
+    if headers.content_length < 0 then
+      raise (HeaderError (InvalidContentLength (string_of_int headers.content_length)))
+    else
+      headers
+
+  let write (io : io) (headers : t) : unit Lwt.t =
+    LwtIO.fprintf io.oc "Content-Type: %s\r\nContent-Length: %d\r\n\r\n" headers.content_type headers.content_length
+end
+
+let read_content (io : io) : string option Lwt.t =
+  let action =
+    let* header = Header.read io in
+    let len = header.content_length in
+    let buffer = Bytes.create len in
+    let rec loop bytes_read =
+      if bytes_read < len then
+        let* n = LwtIO.read_into io.ic buffer bytes_read (len - bytes_read) in
+        loop (bytes_read + n)
+      else
+        Lwt.return @@ Some (Bytes.to_string buffer)
+    in loop 0
+  in
+  Lwt.catch (fun () -> action) @@
+  function
+  | Sys_error _ -> Lwt.return None
+  | End_of_file -> Lwt.return None
+  | exn -> Lwt.fail exn
+
+let read_json (io : io) : Json.t option Lwt.t =
+  let+ contents = read_content io in
+  Option.map Json.of_string contents
+
+let recv (io : io) : Jsonrpc.packet option Lwt.t =
+  let+ json = read_json io in
+  json |> Option.map @@ fun json ->
+  let open Json.O in
+  let req json = Jsonrpc.Message (Jsonrpc.Message.either_of_yojson json) in
+  let resp json = Jsonrpc.Response (Jsonrpc.Response.t_of_yojson json) in
+  (req <|> resp) json
+
+let send (io : io) (packet : Jsonrpc.packet) : unit Lwt.t =
+  let json = Jsonrpc.yojson_of_packet packet in
+  let data = Json.to_string json in
+  let content_length = String.length data in
+  let header = Header.create ~content_length in
+  let* _ = Header.write io header in
+  let* _ = LwtIO.write io.oc data in
+  LwtIO.flush io.oc
+
diff --git a/src/server/LspLwt.mli b/src/server/LspLwt.mli
new file mode 100644
index 000000000..8d375af2c
--- /dev/null
+++ b/src/server/LspLwt.mli
@@ -0,0 +1,13 @@
+type io
+
+val init : unit -> io
+
+module Notation : sig
+  val (let*) : 'a Lwt.t -> ('a -> 'b Lwt.t) -> 'b Lwt.t
+  val (let+) : 'a Lwt.t -> ('a -> 'b) -> 'b Lwt.t
+  val (and*) : 'a Lwt.t -> 'b Lwt.t -> ('a * 'b) Lwt.t
+end
+
+val recv : io -> Jsonrpc.packet option Lwt.t
+val send : io -> Jsonrpc.packet -> unit Lwt.t
+val log  : io -> ('a, unit, string, unit Lwt.t) format4 -> 'a
diff --git a/src/server/Pos.ml b/src/server/Pos.ml
new file mode 100644
index 000000000..9cc1d6731
--- /dev/null
+++ b/src/server/Pos.ml
@@ -0,0 +1,46 @@
+open Basis
+open Frontend
+open Lsp.Types
+
+module CS = ConcreteSyntax
+
+type t = { row : int; col : int }
+
+type range = { start : t; stop: t }
+
+(* these functions might result into invalid positions such as
+   "row 10, col 0" or "row 1, col 100" (where there are only 99
+   characters at row 1), but the correctness of range lookup
+   should not be (hopefully) intact. *)
+let minus_one p = {p with col = p.col - 1}
+let plus_one p = {p with col = p.col + 1}
+let cut_range_after p r = {r with stop = minus_one p}
+let cut_range_before p r = {r with start = plus_one p}
+
+let compare p1 p2 = CCOrd.(int p1.row p2.row <?> (int, p1.col, p2.col))
+
+let of_lex_pos (pos : LexingUtil.position) : t =
+  { row = pos.pos_lnum; col = pos.pos_cnum - pos.pos_bol }
+
+let of_lsp_pos (pos : Position.t) : t =
+  { row = pos.line + 1; col = pos.character }
+
+let of_lex_span (span : LexingUtil.span) : range =
+  { start = of_lex_pos span.start; stop = of_lex_pos span.stop }
+
+let of_lsp_range (range : Range.t) : range =
+  { start = of_lsp_pos (range.start); stop = of_lsp_pos range.end_ }
+
+let to_lsp_pos (pos : t) : Position.t =
+  Position.create ~line:(pos.row - 1) ~character:pos.col
+
+let to_lsp_range (r : range) : Range.t =
+  Range.create ~start:(to_lsp_pos r.start) ~end_:(to_lsp_pos r.stop)
+
+let located (span : LexingUtil.span) : Range.t  =
+  to_lsp_range @@ of_lex_span span
+
+let pp_range fmt range =
+  Format.fprintf fmt "[%d:%d]-[%d:%d]"
+    range.start.row range.start.col
+    range.stop.row range.stop.col
diff --git a/src/server/Pos.mli b/src/server/Pos.mli
new file mode 100644
index 000000000..2e320baa0
--- /dev/null
+++ b/src/server/Pos.mli
@@ -0,0 +1,17 @@
+open Basis
+
+include SegmentTree.POSITION
+
+val of_lex_pos : LexingUtil.position -> t
+val of_lsp_pos : Lsp.Types.Position.t -> t
+
+val to_lsp_pos : t -> Lsp.Types.Position.t
+
+val of_lex_span : LexingUtil.span -> range
+val of_lsp_range : Lsp.Types.Range.t -> range
+
+val to_lsp_range : range -> Lsp.Types.Range.t
+
+val located : LexingUtil.span -> Lsp.Types.Range.t
+
+val pp_range : Format.formatter -> range -> unit
diff --git a/src/server/README.mkd b/src/server/README.mkd
new file mode 100644
index 000000000..aa42a1199
--- /dev/null
+++ b/src/server/README.mkd
@@ -0,0 +1,16 @@
+# Primitive Language Server for 😎tt
+
+## Setting for `coc.nvim`
+
+```json
+{
+  "languageserver": {
+    "cooltt-lsp": {
+      "command": "opam",
+      "args": ["exec", "--", "cooltt", "--mode", "server"],
+      "rootPatterns": ["cooltt-lib"],
+      "filetypes": ["cooltt"]
+    }
+  }
+}
+```
diff --git a/src/server/dune b/src/server/dune
new file mode 100644
index 000000000..166b2f72a
--- /dev/null
+++ b/src/server/dune
@@ -0,0 +1,8 @@
+(library
+ (name Server)
+ (libraries bantorra cooltt.basis cooltt.cubical cooltt.core cooltt.frontend lsp lwt lwt.unix)
+ (preprocess
+  (pps ppx_deriving.std))
+ (flags
+  (:standard -w -32-37-38 -warn-error -a+31))
+ (public_name cooltt.server))
\ No newline at end of file
diff --git a/test/Test.ml b/test/Test.ml
index 98f641d82..850e47f52 100644
--- a/test/Test.ml
+++ b/test/Test.ml
@@ -1,4 +1,5 @@
 open Frontend
+open Driver
 
 let header fname =
   String.make 20 '-' ^ "[" ^ fname ^ "]" ^ String.make 20 '-' ^ "\n"
@@ -7,7 +8,8 @@ let execute_file fname =
   if String.equal (Filename.extension fname) ".cooltt" then
     try
       let _ = print_string (header fname) in
-      ignore @@ Driver.load_file ~as_file:None ~debug_mode:false (`File fname)
+      let opts = { as_file = None; debug_mode = false; } in
+      ignore @@ Driver.load_file opts (`File fname)
     with
       e ->
       Format.eprintf "Could not load file %s@." fname;
diff --git a/vim/syntax/cooltt.vim b/vim/syntax/cooltt.vim
index 0a6de9240..006db420f 100644
--- a/vim/syntax/cooltt.vim
+++ b/vim/syntax/cooltt.vim
@@ -26,7 +26,7 @@ syn keyword coolttKeyw locked unlock zero suc nat in fst snd elim unfold general
 syn keyword coolttKeyw cof sub ext coe hcom com hfill V vproj with struct sig
 
 syn keyword coolttDecl def axiom let import
-syn keyword coolttCmd #normalize #print #quit #fail
+syn keyword coolttCmd #normalize #print #quit #fail #viz
 
 syn match   coolttSymb '=>\|[|,*×:;=≔_𝕀𝔽∂∧∨→⇒!]\|->\|tt\|ff\|⊤\|⊥'
 syn match   coolttSymb '\\/\|/\\'
diff --git a/zsh/_cooltt b/zsh/_cooltt
index 2ccfb2584..4c107060e 100644
--- a/zsh/_cooltt
+++ b/zsh/_cooltt
@@ -8,4 +8,5 @@ _arguments ':' \
   '(- :)--version[show version]' \
   '(-w --width)'{-w,--width=}'[specify width for pretty printing]:width:' \
   '(--debug)--debug[enable debug mode]' \
+  '(--server)--server=[enable cooltt server]:port:' \
   "1:CoolTT file:_files -g '*.cooltt'"