<div dir="ltr">Dear Iris Club,<div><br></div><div>I think the following is typos for <a href="http://plv.mpi-sws.org/iris/appendix-2.0.pdf">http://plv.mpi-sws.org/iris/appendix-2.0.pdf</a> .  Would anyone please confirm or deny?</div><div><br></div><div>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.</div><div><br></div><div>- Page 2: "Note that \mathcal{COFE} is cartesian closed:": I think the following definition (Definition 6) saying something different from cartesian closedness..</div><div><br></div><div>- Page 2: "if its action F1 on arrows": I think "F1" here is a little bit confusing.  What exactly does it mean?</div><div><br></div><div>- 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?</div><div><br></div><div>- Page 8: "Given a cofe T" -> "Given a COFE T"</div><div><br></div><div>- 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."</div><div><br></div><div>- 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?</div><div><br></div><div>- Page 10: "when e1 reduces to e" -> "when e1 reduces to e2"</div><div><br></div><div>- Page 10: "Exp^n" -> "Expr^n"</div><div><br></div><div>- Page 10: in the machine reduction rules, σ's subscripts ae wrong in the conclusion: σ should be σ_1 and σ' should be σ_2.</div><div><br></div><div>- 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?</div><div><br></div><div>- Page 16: in the interpretation of logical implication, I think [[...]]_r(a) should be [[...]]_r(b).</div><div><br></div><div>- Page 17: "if F is locally contractive, then so is ResF." What is F?</div><div><br></div><div>- Page 19: in the interpretation of entailment, [[Gamma | Theta | Q]] should be [[Gamma | Theta | P]], I think.</div><div><br></div><div>- Page 19: what is the meaning if ": 2" in the box?</div><div><br></div><div>- Page 20: "corresponding type.." two dots.</div><div><br></div><div><br></div><div>Later I would like to come up with more semantic questions :-)</div><div><br></div><div>Thank you,</div><div>Jeehoon</div><div><div><br></div>-- <br><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><a href="http://sf.snu.ac.kr/jeehoon.kang" target="_blank">Jeehoon Kang (Ph.D. student)</a><div><a href="http://sf.snu.ac.kr" target="_blank">Software Foundations Laboratory</a><div><a href="http://www.snu.ac.kr" target="_blank">Seoul National University</a></div></div></div></div>
</div></div>