section 3 updates

jfp-paper/defs.tex

@@ -116,6 +116,8 @@
 \newcommand{\unrollty}[1]{\texttt{unroll}_{#1}\,\,}
 \newcommand{\defupcast}[2]{\langle\kern-1ex~\langle{#2}\uarrow{#1}\rangle\kern-1ex~\rangle}
 \newcommand{\defdncast}[2]{\langle\kern-1ex~\langle{#1}\darrow{#2}\rangle\kern-1ex~\rangle}
+\newcommand{\admupcast}[2]{\llparenthesis{#2}\uarrow{#1}\rrparenthesis}
+\newcommand{\admdncast}[2]{\llparenthesis{#1}\darrow{#2}\rrparenthesis}
 
 \newcommand{\result}{\text{result}}
 \newcommand{\Set}{\text{Set}}

jfp-paper/reviews/todo.org

@@ -31,7 +31,7 @@ what is *approximational reasoning*?
 *line -7: at this point, *complex values* and *complex stacks* are unclear.
 
 
-** Old Section 2: Axiomatics
+** TODO Old Section 2: Axiomatics
    1. [ ] move trivial details into an appendix. In particular, full
       page figures of congruence rules where one feels obliged to
       check if anything happens.
@@ -117,11 +117,9 @@ what is *approximational reasoning*?
         - [X] @17: F1+1 --> F(1+1)
 
 
-** TODO Old Section 3: Theorems
-
-
-*** TODO
-1. [ ] Theorem 1 (specification of casts is a universal property) is a
+** DONE Old Section 3: Theorems
+*** DONE 
+1. [X] Theorem 1 (specification of casts is a universal property) is a
    little quick. Can you explain that better?  Also, the theorem
    relies on the fact that your precision relation is such that a
    variable x is less precise than a value V. Again, it was never the
@@ -137,12 +135,11 @@ what is *approximational reasoning*?
    functions, can be implemented correctly by other means. Can you
    bridge that gap for the reader?
 
-3. [-] Section 3.4 shows downcasts are necessarily stacks.  What would
+3. [ ] Section 3.4 shows downcasts are necessarily stacks.  What would
    that theorem tell us if, rather than a CBPV-based calculus, we were
    in an ordinary cast calculus (probably with effects? to compare
    apples to apples?) ?
 
-
 *** DONE ##page 21, lemma 3.2
    - [X] In UpL, it seems like A' needs some upper bound in the assumption.
    - [X] In DnL, B' needs a lower bound, and the typing should be B \sqsubseteq B'.
@@ -154,34 +151,34 @@ what is *approximational reasoning*?
    - [X] It should be made clear that this is the program of the upcoming subsection.
 *** DONE #page 23, thm 4
      - [X] item 1: blob: FA --> blob: FA' (2x)
-*** TODO #page 24
-1. [ ] @-10: there is an inline-example here that should be worked out in more detail: the
+*** DONE #page 24
+1. [X] @-10: there is an inline-example here that should be worked out in more detail: the
    example should demonstrate the two ways of casting A1 x A2 -> B
 
 2. [X]  @-1: last cast should be <<UB \swarrow UB'>> (double brackets)
    (if you don't wish to make this distinction, you should say this explicitly)
-*** TODO ##page 25, def 3
-    1. This definition is pretty sloppy and could be made more formal by using the notation
+*** DONE ##page 25, def 3
+    1. [X] This definition is pretty sloppy and could be made more formal by using the notation
     C[Xi,Yj] introduced below.
-    Right after the definition (or along with it), I would define the instantiation and
-    abbreviation used in line @-3.
-    This could be used to make the statement of lemma 3.4 more formal; the actual proof is
-    trivial.
-    2. [ ] @-10: it's confusing to use the same i to range over independent ranges.
+    - Right after the definition (or along with it), I would define the instantiation and
+      abbreviation used in line @-3.
+    - [ ] This could be used to make the statement of lemma 3.4 more formal; the actual proof is
+      trivial.
+    1. [X] @-10: it's confusing to use the same i to range over independent ranges.
        I'm not sure why this is called a *complex value*. According to def 2, it should be a
-    stack.
-    3. [ ] Same at @-2
-*** TODO #page 26
-1. [ ] @3: not a complex value according to 2.1
+       stack.
+    2. [X] Same at @-2
+*** DONE #page 26
+1. [X] @3: not a complex value according to 2.1
 
-*** TODO ##page 27
-1. [ ] @-8: the << notation >> is only defined for types of the form UB, so what is this supposed
+*** DONE ##page 27
+1. [X] @-8: the << notation >> is only defined for types of the form UB, so what is this supposed
    to mean? It looks ok in principle, but I'm confused by the notation (which seems to be
    used inconsistently)
-*** TODO #page 28
-1. [ ] @4, @5 more of the same confusion
-*** TODO #page 29
-1. [ ] @-6 *taking having* ?
+*** DONE #page 28
+1. [X] @4, @5 more of the same confusion
+*** DONE #page 29
+1. [X] @-6 *taking having* ?
 *** DONE #page 30
 1. [X] @2 first line doesn't make sense
 2. [X] @12: equiprecision for *:B --- S[S'/*] (not x')