Elaborated on value typing judgement

papers/CPP21.md

@@ -12,8 +12,8 @@
 - The disjunction of the compute client list invariant is encoded using a boolean
   flag, as it makes mechanisation easier.
 - The mechanisation employs a typing judgement for values (`ltyped_val`),
-  for technical reasons.
-
+  for technical reasons. More details on this is found in
+  [theories/logrel/term_typing_judgment.v](../theories/logrel/term_typing_judgment.v)
 ## Examples
 
 - The parallel receive example in Section 4 can be found in

theories/logrel/term_typing_judgment.v

@@ -42,7 +42,14 @@ Section ltyped.
   Qed.
 End ltyped.
 
-(* TODO: Elaborate on why this is needed *)
+(** Expressions and values are defined mutually recursive in HeapLang,
+which means that only after a step of reduction we get that e.g.
+Pair (Val v1, Val v2) = PairV (v1,v2).
+This makes typing of values tricky, for technical reasons.
+To circumvent this, we make use of the following typing judgement for values,
+that lets us type check values without requiring reduction steps.
+The value typing judgement subsumes the typing judgement on expressions,
+as made precise by the [ltyped_val_ltyped] lemma. *)
 Definition ltyped_val `{!heapG Σ} (v : val) (A : ltty Σ) : iProp Σ :=
   tc_opaque (■ ltty_car A v)%I.
 Instance: Params (@ltyped_val) 3 := {}.

[Robbert Krebbers]

Coq doc, don't use = for reduction. Say X reduces to Y.