From 62a642671a412f4911ff096569c8ec59f4206f9b Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Tue, 22 Sep 2020 15:38:53 +0200
Subject: [PATCH] Elaborated on value typing judgement

---
 papers/CPP21.md                        | 4 ++--
 theories/logrel/term_typing_judgment.v | 9 ++++++++-
 2 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/papers/CPP21.md b/papers/CPP21.md
index 151b50a..9c77769 100644
--- a/papers/CPP21.md
+++ b/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
diff --git a/theories/logrel/term_typing_judgment.v b/theories/logrel/term_typing_judgment.v
index 73de0d0..96d96a2 100644
--- a/theories/logrel/term_typing_judgment.v
+++ b/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 := {}.
-- 
GitLab