diff --git a/deptypes2/dtlc.ml b/deptypes2/dtlc.ml
new file mode 100644
index 0000000..0a3ceba
--- /dev/null
+++ b/deptypes2/dtlc.ml
@@ -0,0 +1,112 @@
+type kind = Star | Box
+
+type expr =
+  | Var of string
+  | App of expr * expr
+  | Lam of string * ty * expr
+  | Pi of string * ty * expr (* dependent arrow type *)
+  | Kind of kind
+
+and ty = expr
+
+let app f a = App (f, a)
+
+let rec string_of_kind = function Star -> "*" | Box -> "[]"
+
+let rec string_of_t = function
+  | Var x -> x
+  | App (f, a) -> Printf.sprintf "(%s %s)" (string_of_t f) (string_of_t a)
+  | Lam (s, t, e) ->
+      Printf.sprintf "(λ%s:%s. %s)" s (string_of_t t) (string_of_t e)
+  | Pi (s, t, e) ->
+      Printf.sprintf "(Π%s:%s. %s)" s (string_of_t t) (string_of_t e)
+  | Kind k -> string_of_kind k
+
+module S = Set.Make (struct
+  type t = string
+
+  let compare = compare
+end)
+
+let rec fv = function
+  | Var x -> S.singleton x
+  | App (e1, e2) -> S.union (fv e1) (fv e2)
+  | Lam (x, t, e) | Pi (x, t, e) -> S.(union (fv t) (fv e |> remove x))
+  | Kind _ -> S.empty
+
+let rec freshen x used = if S.mem x used then freshen (x ^ "'") used else x
+
+let subst v x e =
+  let rec go subs expr =
+    match expr with
+    | Var x -> ( match List.assoc_opt x subs with Some r -> r | None -> expr)
+    | App (e1, e2) -> App (go subs e1, go subs e2)
+    | Lam (s, t, b) | Pi (s, t, b) ->
+        if s = v then expr
+        else if S.mem s (fv x) then
+          let s' = freshen s (S.union (fv x) (fv b)) in
+          Lam (s', go subs t, go ((s, Var s') :: subs) b)
+        else Lam (s, go subs t, go subs b)
+    | Kind _ -> expr
+  in
+  go [ (v, x) ] e
+
+let alpha_eq e1 e2 =
+  let fresh =
+    let next = ref 0 in
+    fun () ->
+      incr next;
+      !next
+  in
+  let rec cmp n1 n2 e1 e2 =
+    match (e1, e2) with
+    | Var x, Var y -> (
+        match (List.assoc_opt x n1, List.assoc_opt y n2) with
+        | Some n, Some m -> n = m
+        | None, None -> x = y
+        | _ -> false)
+    | App (e11, e12), App (e21, e22) -> cmp n1 n2 e11 e21 && cmp n1 n2 e12 e22
+    | Lam (s1, t1, b1), Lam (s2, t2, b2) | Pi (s1, t1, b1), Pi (s2, t2, b2) ->
+        let s = fresh () in
+        cmp n1 n2 t1 t2 && cmp ((s1, s) :: n1) ((s2, s) :: n2) b1 b2
+    | Kind k1, Kind k2 -> k1 = k2
+    | _ -> false
+  in
+  cmp [] [] e1 e2
+
+let rec nf e =
+  let app f rest = List.fold_left app f (List.map nf rest) in
+  let rec spine = function
+    | App (f, a), sp -> spine (f, a :: sp)
+    | Lam (s, _, e), a :: sp -> spine (subst s a e, sp)
+    | Lam (s, t, e), [] -> Lam (s, nf t, nf e)
+    | Pi (s, t, e), sp -> app (Pi (s, nf t, nf e)) sp
+    | f, sp -> app f sp
+  in
+  spine (e, [])
+
+let abeq e1 e2 = alpha_eq (nf e1) (nf e2)
+
+let ( >>= ) = Option.bind
+
+let rec tyck ctx = function
+  | Var x -> List.assoc_opt x ctx
+  | App (f, a) -> (
+      tyck ctx f >>= function
+      | Pi (x, t1, t2) ->
+          tyck ctx a >>= fun ta ->
+          if abeq ta t1 then Some (subst x a t2) else None
+      | _ -> None)
+  | Lam (s, t, b) ->
+      tyck ctx t >>= fun _t_well_formed ->
+      tyck ((s, t) :: ctx) b >>= fun tb ->
+      let rt = Pi (s, t, tb) in
+      tyck ctx rt >>= fun _rt_well_formed -> Some rt
+  | Pi (s, t, b) -> (
+      tyck_nf ctx t >>= fun k_t ->
+      tyck_nf ((s, t) :: ctx) b >>= fun k_tb ->
+      match (k_t, k_tb) with Kind _, Kind _ -> Some k_tb | _ -> None)
+  | Kind Star -> Some (Kind Box)
+  | Kind Box -> None
+
+and tyck_nf ctx e = tyck ctx e >>= fun e -> Some (nf e)
diff --git a/deptypes2/dune b/deptypes2/dune
new file mode 100644
index 0000000..11435c8
--- /dev/null
+++ b/deptypes2/dune
@@ -0,0 +1,4 @@
+(library
+ (name deptypes2)
+ (inline_tests)
+ (preprocess (pps ppx_inline_test ppx_expect)))
diff --git a/deptypes2/pmlc.ml b/deptypes2/pmlc.ml
new file mode 100644
index 0000000..cd16b84
--- /dev/null
+++ b/deptypes2/pmlc.ml
@@ -0,0 +1,30 @@
+type ty = Arrow of ty * ty | TVar of string
+
+type kind = KArrow of kind * kind | Star
+
+type expr =
+  | Var of string
+  | App of expr * expr
+  | Lam of string * ty * expr
+  | TLam of string * kind * expr
+  | TApp of expr * ty
+
+let rec string_of_ty = function
+  | Arrow (l, r) -> Printf.sprintf "(%s->%s)" (string_of_ty l) (string_of_ty r)
+  | TVar v -> v
+
+let rec string_of_kind = function
+  | Star -> "*"
+  | KArrow (l, r) ->
+      Printf.sprintf "(%s->%s)" (string_of_kind l) (string_of_kind r)
+
+let rec string_of_expr = function
+  | Var x -> x
+  | App (f, a) -> Printf.sprintf "(%s %s)" (string_of_expr f) (string_of_expr a)
+  | Lam (s, t, e) ->
+      Printf.sprintf "(λ%s:%s. %s)" s (string_of_ty t) (string_of_expr e)
+  | TLam (s, k, e) ->
+      Printf.sprintf "(Λ%s:%s. %s)" s (string_of_kind k) (string_of_expr e)
+  | TApp (e, t) -> Printf.sprintf "(%s[%s])" (string_of_expr e) (string_of_ty t)
+
+let ( >>= ) = Option.bind
diff --git a/deptypes2/stlc.ml b/deptypes2/stlc.ml
new file mode 100644
index 0000000..e5a8370
--- /dev/null
+++ b/deptypes2/stlc.ml
@@ -0,0 +1,31 @@
+type ty = Base | Arrow of ty * ty
+
+type expr = Var of string | App of expr * expr | Lam of string * ty * expr
+
+let rec string_of_ty = function
+  | Base -> "B"
+  | Arrow (l, r) -> Printf.sprintf "(%s->%s)" (string_of_ty l) (string_of_ty r)
+
+let rec string_of_expr = function
+  | Var x -> x
+  | App (f, a) -> Printf.sprintf "(%s %s)" (string_of_expr f) (string_of_expr a)
+  | Lam (s, t, e) ->
+      Printf.sprintf "(λ%s:%s. %s)" s (string_of_ty t) (string_of_expr e)
+
+let ( >>= ) = Option.bind
+
+let rec tyck ctx = function
+  | Var x -> List.assoc_opt x ctx
+  | App (f, a) -> (
+      tyck ctx f >>= function
+      | Arrow (t1, t2) ->
+          tyck ctx a >>= fun ta -> if t1 = ta then Some t2 else None
+      | _ -> None)
+  | Lam (s, t1, b) ->
+      tyck ((s, t1) :: ctx) b >>= fun t2 -> Some (Arrow (t1, t2))
+
+let%expect_test _ =
+  tyck []
+    (Lam ("x", Arrow (Base, Base), Lam ("y", Base, App (Var "x", Var "y"))))
+  |> Option.get |> string_of_ty |> prerr_string;
+  [%expect "((B->B)->(B->B))"]
diff --git a/deptypes2/ulc.ml b/deptypes2/ulc.ml
new file mode 100644
index 0000000..d8f54fe
--- /dev/null
+++ b/deptypes2/ulc.ml
@@ -0,0 +1,184 @@
+type expr = Var of string | App of expr * expr | Lam of string * expr
+
+let app e1 e2 = App (e1, e2)
+
+let rec string_of_expr = function
+  | Var x -> x
+  | App (f, a) -> Printf.sprintf "(%s %s)" (string_of_expr f) (string_of_expr a)
+  | Lam (s, e) -> Printf.sprintf "(λ%s. %s)" s (string_of_expr e)
+
+module S = Set.Make (struct
+  type t = string
+
+  let compare = compare
+end)
+
+let rec freevars = function
+  | Var x -> S.singleton x
+  | App (e1, e2) -> S.union (freevars e1) (freevars e2)
+  | Lam (x, e) -> S.remove x (freevars e)
+
+let rec freshen x used = if S.mem x used then freshen (x ^ "'") used else x
+
+let subst v x e =
+  let rec go subs expr =
+    match expr with
+    | Var u -> ( match List.assoc_opt u subs with Some e -> e | None -> expr)
+    | App (e1, e2) -> App (go subs e1, go subs e2)
+    | Lam (s, b) ->
+        if s = v then expr
+        else if S.mem s (freevars x) then
+          (* We have a case like [y->s] (\s. y). If we perform a direct substitution
+             we go from referencing "s" in a narrower scope to a tighter scope. So
+             instead, generate a fresh variable name for s. *)
+          let s' = freshen s (S.union (freevars x) (freevars b)) in
+          Lam (s', go ((s, Var s') :: subs) b)
+        else Lam (s, go subs b)
+  in
+  go [ (v, x) ] e
+
+let%expect_test _ =
+  subst "y" (Var "s") (Lam ("s", Var "y")) |> string_of_expr |> prerr_string;
+  [%expect "(λs'. s)"]
+
+let%expect_test _ =
+  subst "y" (Var "s") (Lam ("s", Lam ("s", App (Var "s", Var "y"))))
+  |> string_of_expr |> prerr_string;
+  [%expect "(λs'. (λs'. (s' s)))"]
+
+let%expect_test _ =
+  subst "x" (Var "y") (Lam ("x", Var "x")) |> string_of_expr |> prerr_string;
+  [%expect "(λx. x)"]
+
+let%expect_test _ =
+  subst "x" (Lam ("z", App (Var "z", Var "w"))) (Lam ("y", Var "x"))
+  |> string_of_expr |> prerr_string;
+  [%expect "(λy. (λz. (z w)))"]
+
+(** Yields the weak-head normal form of an expression.
+    Only beta redexes along the left-hand spine of the expression are reduced,
+    leaving arguments "into" the spine untouched.
+       ((\x. x) (\x. x)) ((\y. y) z)
+    -> (\x. x) ((\y. y) z)
+    -> (\y. y) z
+    -> z
+ *)
+let whnf e =
+  let rec spine e sp =
+    match (e, sp) with
+    | App (f, a), rest -> spine f (a :: rest)
+    | Lam (s, e), a :: rest -> spine (subst s a e) rest
+    | f, rest -> List.fold_left app f rest
+  in
+  spine e []
+
+let%expect_test _ =
+  whnf
+    (App
+       ( App (Lam ("x", Var "x"), Lam ("x", Var "x")),
+         App (Lam ("y", Var "y"), Var "z") ))
+  |> string_of_expr |> print_string;
+  [%expect "z"]
+
+let%expect_test _ =
+  whnf (App (Var "x", App (Lam ("y", Var "y"), Var "z")))
+  |> string_of_expr |> print_string;
+  [%expect "(x ((λy. y) z))"]
+
+let alpha_eq e1 e2 =
+  let fresh =
+    let next = ref 0 in
+    fun () ->
+      incr next;
+      !next
+  in
+  let rec cmp n1 n2 e1 e2 =
+    match (e1, e2) with
+    | Var x, Var y -> (
+        match (List.assoc_opt x n1, List.assoc_opt y n2) with
+        | Some n, Some m -> n = m
+        | None, None -> x = y
+        | _ -> false)
+    | App (e11, e12), App (e21, e22) -> cmp n1 n2 e11 e21 && cmp n1 n2 e12 e22
+    | Lam (s1, b1), Lam (s2, b2) ->
+        let s = fresh () in
+        cmp ((s1, s) :: n1) ((s2, s) :: n2) b1 b2
+    | _ -> false
+  in
+  cmp [] [] e1 e2
+
+let%test _ =
+  let fn x y = Lam (x, App (Lam (y, App (Var y, Var x)), Var x)) in
+  alpha_eq (fn "x" "y") (fn "z" "x")
+
+(** Yields the normal form of an expression, containing no beta redexes at
+    all, by way of normal-order reduction (which is complete, see
+    https://en.wikipedia.org/wiki/Beta_normal_form).
+       nf (x ((\y. y) z))
+    -> App x (nf ((\y. y) z))
+    -> App x z
+ *)
+let rec nf1 e =
+  let rec spine e sp =
+    match (e, sp) with
+    | App (f, a), rest -> spine f (a :: rest)
+    | Lam (s, e), [] -> Lam (s, nf1 e)
+    | Lam (s, e), a :: rest -> spine (subst s a e) rest
+    | f, rest -> List.fold_left app f (List.map nf1 rest)
+  in
+  spine e []
+
+exception NoRule
+
+let rec nf = function
+  | App (f, a) -> (
+      let f = nf f in
+      match f with Lam (s, e) -> nf (subst s a e) | _ -> App (f, nf a))
+  | Lam (s, e) -> Lam (s, nf e)
+  | e -> e
+
+let%expect_test _ =
+  nf (App (Var "x", Var "y")) |> string_of_expr |> print_string;
+  [%expect "(x y)"]
+
+let%expect_test _ =
+  nf (App (Var "x", App (Lam ("y", Var "y"), Var "z")))
+  |> string_of_expr |> print_string;
+  [%expect "(x z)"]
+
+let%expect_test _ =
+  nf (Lam ("x", App (Lam ("y", Var "y"), Var "z")))
+  |> string_of_expr |> print_string;
+  [%expect "(λx. z)"]
+
+let%expect_test _ =
+  let trip = Lam ("w", App (App (Var "w", Var "w"), Var "w")) in
+  nf (App (Lam ("x", Var "z"), App (trip, trip)))
+  |> string_of_expr |> print_string;
+  [%expect "z"]
+
+(** Alpha-beta equality *)
+let ab_eq e1 e2 = alpha_eq (nf e1) (nf e2)
+
+let one = Lam ("s", Lam ("z", App (Var "s", Var "z")))
+
+let two = Lam ("s", Lam ("z", App (Var "s", App (Var "s", Var "z"))))
+
+let plus =
+  Lam
+    ( "m",
+      Lam
+        ( "n",
+          Lam
+            ( "s",
+              Lam
+                ( "z",
+                  App
+                    ( App (Var "m", Var "s"),
+                      App (App (Var "n", Var "s"), Var "z") ) ) ) ) )
+
+let%expect_test _ =
+  nf (App (App (plus, one), one)) |> string_of_expr |> print_string;
+  [%expect "(λs. (λz. (s (s z))))"]
+
+let%test _ = ab_eq (App (App (plus, one), one)) two
diff --git a/lambdapi/dtlc.ml b/lambdapi/dtlc.ml
new file mode 100644
index 0000000..5c5a9dd
--- /dev/null
+++ b/lambdapi/dtlc.ml
@@ -0,0 +1,200 @@
+type name = Global of string | Local of int | Quote of int
+
+type term_infer =
+  | Annot of term_check * term_check
+  | Star
+  | Pi of term_check * term_check
+  | Bound of int
+  | Free of name
+  | App of term_infer * term_check
+  | Nat
+  | NatElim of term_check * term_check * term_check * term_check
+
+and term_check =
+  | Infer of term_infer
+  | Lam of term_check
+  | Zero
+  | Succ of term_check
+
+let string_of_term t =
+  let rec goi = function
+    | Annot (t, ty) -> Printf.sprintf "(%s :: %s)" (goc t) (goc ty)
+    | Star -> "*"
+    | Pi (d, b) -> Printf.sprintf "(Π: %s. %s)" (goc d) (goc b)
+    | Bound i -> string_of_int i
+    | Free (Global n) -> n
+    | Free (Local i) -> string_of_int i
+    | Free (Quote i) -> string_of_int i
+    | App (ti, tc) -> Printf.sprintf "(%s %s)" (goi ti) (goc tc)
+    | Nat -> "Nat"
+    | NatElim (m, mz, ms, n) ->
+        Printf.sprintf "(natElim %s %s %s %s)" (goc m) (goc mz) (goc ms) (goc n)
+  and goc = function
+    | Infer ti -> goi ti
+    | Lam tc -> Printf.sprintf "(λ. %s)" (goc tc)
+    | Zero -> "0"
+    | Succ n -> Printf.sprintf "(S %s)" (goc n)
+  in
+  goc t
+
+type value =
+  | VLam of (value -> value)
+  | VStar
+  | VPi of value * (value -> value)
+  | VNeutral of neutral
+  | VNat
+  | VZero
+  | VSucc of value
+
+and neutral =
+  | NFree of name
+  | NApp of neutral * value
+  | NNatElim of value * value * value * neutral
+
+let vfree n = VNeutral (NFree n)
+
+let vapp f v =
+  match f with
+  | VLam f -> f v
+  | VNeutral n -> VNeutral (NApp (n, v))
+  | _ -> failwith "application not applicable"
+
+(* eval *)
+
+let rec eval_infer env = function
+  | Annot (e, _) -> eval_check env e
+  | Star -> VStar
+  | Pi (dom, b) -> VPi (eval_check env dom, fun x -> eval_check (x :: env) b)
+  | Bound i -> List.nth env i
+  | Free x -> vfree x
+  | App (e1, e2) -> vapp (eval_infer env e1) (eval_check env e2)
+  | Nat -> VNat
+  | NatElim (m, mz, ms, n) ->
+      let mz = eval_check env mz in
+      let ms = eval_check env ms in
+      let rec solve = function
+        | VZero -> mz
+        | VSucc n1 -> vapp (vapp ms n1) (solve n1)
+        | VNeutral n -> VNeutral (NNatElim (eval_check env m, mz, ms, n))
+        | _ -> failwith "invalid value in nat eliminator"
+      in
+      solve (eval_check env n)
+
+and eval_check env = function
+  | Infer it -> eval_infer env it
+  | Lam b -> VLam (fun x -> eval_check (x :: env) b)
+  | Zero -> VZero
+  | Succ n -> VSucc (eval_check env n)
+
+(* quote *)
+
+let bindfree i = function Quote k -> Bound (i - k - 1) | x -> Free x
+
+let rec quote i = function
+  | VLam f -> Lam (quote (i + 1) (f (vfree (Quote i))))
+  | VStar -> Infer Star
+  | VPi (d, b) -> Infer (Pi (quote i d, quote (i + 1) (b (vfree (Quote i)))))
+  | VNeutral n -> Infer (quote_neutral i n)
+  | VNat -> Infer Nat
+  | VZero -> Zero
+  | VSucc k -> Succ (quote i k)
+
+and quote_neutral i = function
+  | NFree x -> bindfree i x
+  | NApp (n, v) -> App (quote_neutral i n, quote i v)
+  | NNatElim (m, ms, mz, n) ->
+      NatElim (quote i m, quote i ms, quote i mz, Infer (quote_neutral i n))
+
+let vquote = quote 0
+
+(* typecheck *)
+
+type ty = ETy of value
+
+type context = (name * ty) list
+
+let ( >>= ) = Result.bind
+
+let rec subst_infer o n tm =
+  let rec go = function
+    | Annot (e, t) -> Annot (subst_check o n e, t)
+    | Star -> Star
+    | Pi (d, b) -> Pi (subst_check o n d, subst_check (o + 1) n b)
+    | Bound x -> if o = x then n else Bound x
+    | Free n -> Free n
+    | App (e1, e2) -> App (go e1, subst_check o n e2)
+    | Nat -> Nat
+    | NatElim (m, mz, ms, k) ->
+        NatElim
+          ( subst_check o n m,
+            subst_check o n mz,
+            subst_check o n ms,
+            subst_check o n k )
+  in
+  go tm
+
+and subst_check o n = function
+  | Infer it -> Infer (subst_infer o n it)
+  | Lam b -> Lam (subst_check (o + 1) n b)
+  | Zero -> Zero
+  | Succ k -> Succ (subst_check o n k)
+
+let rec type_infer i ctx = function
+  | Annot (e, ty) ->
+      type_check i ctx ty VStar >>= fun _ ->
+      let ety = eval_check [] ty in
+      type_check i ctx e ety >>= fun _ -> Ok ety
+  | Star -> Ok VStar
+  | Pi (dom, b) ->
+      type_check i ctx dom VStar >>= fun _ ->
+      let edom = eval_check [] dom in
+      type_check (i + 1)
+        ((Local i, ETy edom) :: ctx)
+        (subst_check 0 (Free (Local i)) b)
+        VStar
+      >>= fun _ -> Ok VStar
+  | Bound _ -> Error "impossible state: bound variable never expected"
+  | Free x -> (
+      match List.assoc_opt x ctx with
+      | Some (ETy ty) -> Ok ty
+      | _ -> Error "bad type for free var")
+  | App (e1, e2) -> (
+      type_infer i ctx e1 >>= function
+      | VPi (d, b) ->
+          type_check i ctx e2 d >>= fun _ -> Ok (b (eval_check [] e2))
+      | _ -> Error "LHS of application must be function type")
+  | Nat -> Ok VStar
+  | NatElim (m, mz, ms, n) ->
+      type_check i ctx m (VPi (VNat, fun _ -> VStar)) >>= fun _ ->
+      let mval = eval_check [] m in
+      type_check i ctx mz (vapp mval VZero) >>= fun _ ->
+      type_check i ctx ms
+        (VPi (VNat, fun k -> VPi (vapp mval k, fun _ -> vapp mval (VSucc k))))
+      >>= fun _ ->
+      type_check i ctx n VNat >>= fun _ ->
+      let nval = eval_check [] n in
+      Ok (vapp mval nval)
+
+and type_check i ctx e ty =
+  match (e, ty) with
+  | Infer it, ety ->
+      type_infer i ctx it >>= fun ity ->
+      if vquote ity = vquote ety then Ok ()
+      else
+        Error
+          (Printf.sprintf "inferred type %s does not match checked type %s"
+             (string_of_term (vquote ity))
+             (string_of_term (vquote ety)))
+  | Lam b, VPi (t1, t2) ->
+      type_check (i + 1) ((Local i, ETy t1) :: ctx)
+        (subst_check 0 (Free (Local i)) b)
+        (t2 (vfree (Local i)))
+  | Zero, VNat -> Ok ()
+  | Succ k, VNat -> type_check i ctx k VNat
+  | a, b ->
+      Error
+        (Printf.sprintf "type mismatch: cannot check %s as %s"
+           (string_of_term a)
+           (string_of_term (vquote b)))
+
+let tyck ctx tm = type_infer 0 ctx tm
diff --git a/lambdapi/dune b/lambdapi/dune
new file mode 100644
index 0000000..2d356e1
--- /dev/null
+++ b/lambdapi/dune
@@ -0,0 +1,4 @@
+(library
+ (name lambdapi)
+ (inline_tests)
+ (preprocess (pps ppx_inline_test ppx_expect)))
diff --git a/lambdapi/stlc.ml b/lambdapi/stlc.ml
new file mode 100644
index 0000000..aeaf9b5
--- /dev/null
+++ b/lambdapi/stlc.ml
@@ -0,0 +1,143 @@
+type name = Global of string | Local of int | Quote of int
+
+type kind = KStar
+
+type ty = TFree of name | TFun of ty * ty
+
+type term_infer =
+  | Annot of term_check * ty
+  | Bound of int
+  | Free of name
+  | App of term_infer * term_check
+
+and term_check = Infer of term_infer | Lam of term_check
+
+type value = VLam of (value -> value) | VNeutral of neutral
+
+and neutral = NFree of name | NApp of neutral * value
+
+let vfree n = VNeutral (NFree n)
+
+let vapp f v =
+  match f with VLam f -> f v | VNeutral n -> VNeutral (NApp (n, v))
+
+(* eval *)
+
+let rec eval_infer env = function
+  | Annot (e, _) -> eval_check env e
+  | Bound i -> List.nth env i
+  | Free x -> vfree x
+  | App (e1, e2) -> vapp (eval_infer env e1) (eval_check env e2)
+
+and eval_check env = function
+  | Infer it -> eval_infer env it
+  | Lam b -> VLam (fun x -> eval_check (x :: env) b)
+
+(* typecheck *)
+
+type info = HasKind of kind | HasType of ty
+
+type context = (name * info) list
+
+let ( >>= ) = Result.bind
+
+let rec kind_check ctx ty k =
+  match (ty, k) with
+  | TFree x, KStar -> (
+      match List.assoc_opt x ctx with
+      | Some (HasKind KStar) -> Ok ()
+      | _ -> Error "bad kind for free type")
+  | TFun (t1, t2), KStar ->
+      kind_check ctx t1 KStar >>= fun _ -> kind_check ctx t2 KStar
+
+let rec subst_infer o n tm =
+  let rec go = function
+    | Annot (e, t) -> Annot (subst_check o n e, t)
+    | Bound x -> if o = x then n else Bound x
+    | Free n -> Free n
+    | App (e1, e2) -> App (go e1, subst_check o n e2)
+  in
+  go tm
+
+and subst_check o n = function
+  | Infer it -> Infer (subst_infer o n it)
+  | Lam b -> Lam (subst_check (o + 1) n b)
+
+let rec type_infer i ctx = function
+  | Annot (e, ty) ->
+      kind_check ctx ty KStar >>= fun _ ->
+      type_check i ctx e ty >>= fun _ -> Ok ty
+  | Bound _ -> Error "impossible state: bound variable never expected"
+  | Free x -> (
+      match List.assoc_opt x ctx with
+      | Some (HasType ty) -> Ok ty
+      | _ -> Error "bad type for free var")
+  | App (e1, e2) -> (
+      type_infer i ctx e1 >>= function
+      | TFun (t1, t2) -> type_check i ctx e2 t1 >>= fun _ -> Ok t2
+      | _ -> Error "LHS of application must be function type")
+
+and type_check i ctx e ty =
+  match (e, ty) with
+  | Infer it, ety ->
+      type_infer i ctx it >>= fun ity ->
+      if ity = ety then Ok ()
+      else Error "inferred type does not match checked type"
+  | Lam b, TFun (t1, t2) ->
+      type_check (i + 1)
+        ((Local i, HasType t1) :: ctx)
+        (subst_check 0 (Free (Local i)) b)
+        t2
+  | _ -> Error "type mismatch"
+
+let tyck ctx tm = type_infer 0 ctx tm
+
+(* quote *)
+
+let bindfree i = function Quote k -> Bound (i - k - 1) | x -> Free x
+
+let rec quote i = function
+  | VLam f -> Lam (quote (i + 1) (f (vfree (Quote i))))
+  | VNeutral n -> Infer (quote_neutral i n)
+
+and quote_neutral i = function
+  | NFree x -> bindfree i x
+  | NApp (n, v) -> App (quote_neutral i n, quote i v)
+
+let vquote = quote 0
+
+(* test *)
+
+let tfree a = TFree (Global a)
+
+let free x = Infer (Free (Global x))
+
+let id = Lam (Infer (Bound 0))
+
+let const = Lam (Lam (Infer (Bound 1)))
+
+let term1 = App (Annot (id, TFun (tfree "a", tfree "a")), free "y")
+
+let term2 =
+  App
+    ( App
+        ( Annot
+            ( const,
+              TFun
+                ( TFun (tfree "b", tfree "b"),
+                  TFun (tfree "a", TFun (tfree "b", tfree "b")) ) ),
+          id ),
+      free "y" )
+
+let ctx1 = [ (Global "y", HasType (tfree "a")); (Global "a", HasKind KStar) ]
+
+let ctx2 = ctx1 @ [ (Global "b", HasKind KStar) ]
+
+let%test _ = eval_infer [] term1 |> vquote = Infer (Free (Global "y"))
+
+let%test _ = eval_infer [] term2 |> vquote = id
+
+let%test _ = tyck ctx1 term1 = Ok (TFree (Global "a"))
+
+let%test _ =
+  tyck ctx2 term2 = Ok (TFun (TFree (Global "b"), TFree (Global "b")))