[Iris-Club] Typos (, I think,) in the Iris 2.0 documentation

[Jeehoon Kang]

Dear Iris Club,

I think the following is typos for
http://plv.mpi-sws.org/iris/appendix-2.0.pdf .  Would anyone please confirm
or deny?

Many of them are really minor; but as a novice I was not confident with my
understanding, and not sure that those are really typos.  On the other
hand, some of them are rather a question or call for clarification than
just typos..  For both cases any kind of resolutions by the authors will
really help me to read the document.

- Page 2: "Note that \mathcal{COFE} is cartesian closed:": I think the
following definition (Definition 6) saying something different from
cartesian closedness..

- Page 2: "if its action F1 on arrows": I think "F1" here is a little bit
confusing.  What exactly does it mean?

- Page 7: the (FPFN-ALLOC) rule does not require K to be infinite, but I
think it should be.  I guess "Given some countable K" is a typo for "Given
some infinitely countable K".  May I ask it is indeed the case?

- Page 8: "Given a cofe T" -> "Given a COFE T"

- Page 9: "we construct a monoid modeling": in fact you are modeling an RA,
which is evident from the fact the "the core is no a homomorphism."

- Page 9: in what sense "↑(S, T)" is the closure?  I mean, is it minimal
w.r.t. the closedness?  If so, is it obvious?

- Page 10: "when e1 reduces to e" -> "when e1 reduces to e2"

- Page 10: "Exp^n" -> "Expr^n"

- Page 10: in the machine reduction rules, σ's subscripts ae wrong in the
conclusion: σ should be σ_1 and σ' should be σ_2.

- Page 15: it is not a typo; but I think it is a little bit hard to parse
the conclusion of (WP-LIFT-STEP); may I ask if you could insert some
redundant parentheses?

- Page 16: in the interpretation of logical implication, I think
[[...]]_r(a) should be [[...]]_r(b).

- Page 17: "if F is locally contractive, then so is ResF." What is F?

- Page 19: in the interpretation of entailment, [[Gamma | Theta | Q]]
should be [[Gamma | Theta | P]], I think.

- Page 19: what is the meaning if ": 2" in the box?

- Page 20: "corresponding type.." two dots.


Later I would like to come up with more semantic questions :-)

Thank you,
Jeehoon

-- 
Jeehoon Kang (Ph.D. student) <http://sf.snu.ac.kr/jeehoon.kang>
Software Foundations Laboratory <http://sf.snu.ac.kr>
Seoul National University <http://www.snu.ac.kr>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mpi-sws.org/pipermail/iris-club/attachments/20160809/5fc4f2da/attachment.html>