[Iris-Club] Typos (, I think,) in the Iris 2.0 documentation
Jeehoon Kang
jeehoon.kang at sf.snu.ac.kr
Tue Aug 9 15:05:48 CEST 2016
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>
More information about the Iris-Club
mailing list