<div dir="ltr"><div><div><div>I have more questions...<br><br><br>- "we can use the maps ξ and ξ^{−1} in the logic to convert" [2, S8.1, p26]: I think by using ξ and ξ^{−1} in the Iris logic you actually extends the base logic, and we no longer cannot say that Iris is an instantiation of the base logic. I know it is a somewhat pedantic comment; I just want to know the motivation of the explanation in [2, S8.1].<br><br>- typo? "composeability" [2, S8.1, p25] for "composability"<br><br>- On composability [2, S8.1, p25]: why don't you just product over all possible bifunctor \Sigma? In that way you can just assume "the" family of functors, and composability is no longer an issue. (I currently am guessing it is related to universe size or impredicativity problem in Coq..)<br><br>- "STATE" [2, S8.2, p27] is used without definition: "Finally, STATE is used to provide ..."<br><br>- The view shifts for normal update modality is used in the (VS-UPDATE) and (VS-TIMELESS) rules without definition [2, S8.2, p28]. (There is only one possible interpretation of it, though..)<br><br>- For the physical state interpretation function, [1] uses "I" and [2] uses "S" as the ranging meta-variable. I think it would be nice for the two documents to use the same symbol here.<br><br>- In the definition of "legal return value" [2, p29], T'' is not constrained at all.<br><br></div>- In [2, S8.5, p32], I couldn't understand the following sentence: "Using (vs-trans) and (Ht-atomic) (or the corresponding proof rules for fancy updates and weakest preconditions), we can show that it is possible to open an accessor around any view shift and any atomic expression." May I ask what did you mean by this sentence?<br><br><br></div>Thank you,<br></div>Jeehoon<br><div><div><div><br><br></div></div></div></div><div class="gmail_extra"><br><div class="gmail_quote">2017-01-31 21:02 GMT+01:00 Jeehoon Kang <span dir="ltr"><<a href="mailto:jeehoon.kang@sf.snu.ac.kr" target="_blank">jeehoon.kang@sf.snu.ac.kr</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div><div><div><div><div><div><div>Dear Iris Club,<br><br><br></div>As usual, I have several small questions on Iris :)<br><br><br></div><div>First things first, here are references:<br></div><div>- [1] Iris 3.0 paper<br></div><div>- [2] Iris 3.0 appendix<br></div><br></div><br>Now questions:<br><br>- I don't understand why it is okay *not* to have "Own(\iota,
\gamma_{EN})" at the conclusion of the rules (WSAT-ALLOC) and
(INV-ALLOC) [1]. More specifically, why is it okay to "forget" the fact that
the "\iota" invariant is enabled when it is created?<br><br>- Why "K" should be countably infinite for the CMRA construction of finite partial function [2, S3.4, p11]? More precisely, why not (possibly) uncountably infinite K?<br></div><br></div>- What is "c" in the definition of AG(T) [2, S3.5, p11]?<br><br></div>- I don't quite understand what "Variable conventions." means [2, S4.1]: "We assume that, if a term occurs multiple times in a rule, its free variables are exactly those binders which are available at every occurrence."<br><br></div>- I think "Res" in the definition of the interpretation of entailment in [2, p20], should be "M".<br><br></div><div>- It seems the semantics of "\Gamma | P => Q" and "\Gamma | P |- Q" are much related [2]. I wonder if the notion of logical entailment can be encoded with the semantics of implications. (Yes, I know it is a program logic newbie question :-) I just want to know the motivation behind the concept of logical entailment.)<br></div><div><br></div>- typo: "ruels" in [2, p22]<br><br>- typo: "Stateof" in [2, p24] (rather than "State of")<br><div><div><div><div><div><div><div><div><div><div><br><br></div><div>Best regards,<br></div><div>Jeehoon<span class="HOEnZb"><font color="#888888"><br></font></span></div><span class="HOEnZb"><font color="#888888"><div><br>-- <br><div class="m_-3545009562457396355gmail_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></font></span></div></div></div></div></div></div></div></div></div></div>
</blockquote></div><br><br clear="all"><br>-- <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>