diff --git a/src/core/t_ref.ml b/src/core/t_ref.ml
new file mode 100644
index 00000000..0eacacdb
--- /dev/null
+++ b/src/core/t_ref.ml
@@ -0,0 +1,50 @@
+(** Term reference *)
+
+open Sidekick_core_logic
+
+open struct
+  module Tr = Sidekick_trace
+end
+
+type t = Tr.entry_id
+type Const.view += Ref of t
+
+let ops : Const.Ops.t =
+  let pp out = function
+    | Ref x -> Fmt.fprintf out "(@[ref %a@])" Tr.Entry_id.pp x
+    | _ -> assert false
+  in
+
+  let equal a b =
+    match a, b with
+    | Ref a, Ref b -> Tr.Entry_id.equal a b
+    | _ -> false
+  in
+  let hash = function
+    | Ref a -> Hash.combine2 519 (Tr.Entry_id.hash a)
+    | _ -> assert false
+  in
+
+  let ser _sink = function
+    | Ref a -> "!", Ser_value.(int a)
+    | _ -> assert false
+  in
+  { Const.Ops.equal; pp; hash; ser }
+
+let ref (tst : Term.store) (r : t) ~ty : Term.t =
+  Term.const tst @@ Const.make (Ref r) ops ~ty
+
+let[@inline] as_ref t : t option =
+  match Term.view t with
+  | Term.E_const { Const.c_view = Ref r; _ } -> Some r
+  | _ -> None
+
+let const_decoders : Const.decoders =
+  [
+    ( "!",
+      ops,
+      Ser_decode.(
+        fun _dec_term ->
+          let+ i = int in
+          Ref i) );
+  ]
diff --git a/src/core/t_ref.mli b/src/core/t_ref.mli
new file mode 100644
index 00000000..5c5c48e0
--- /dev/null
+++ b/src/core/t_ref.mli
@@ -0,0 +1,27 @@
+(** Term reference *)
+
+open Sidekick_core_logic
+
+type t = Sidekick_trace.entry_id
+(** Reference to another term, by a unique ID in a trace.
+
+  This allows a trace to contain terms with explicit references
+  to other terms, but where these references have to be followed explicitly.
+  Thus, each term can be deserialized separately.
+
+  For example, a proof term for a given lemma might use references to previous
+  lemmas, instead of their direct proof terms; this allows a checker or
+  proof GUI to only read this particular lemma's proof into a term.
+*)
+
+type Const.view += private Ref of t
+
+val ref : Term.store -> t -> ty:Term.t -> Term.t
+(** [ref tst id ~ty] is the reference to entry [id] in a trace,
+    which must be
+    a term of type [ty]. *)
+
+val as_ref : Term.t -> t option
+(** [as_ref (ref tst id ~ty)] is [Some id]. *)
+
+val const_decoders : Const.decoders