<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<br></div><div><br>-- <br><div class="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></div></div></div></div></div></div></div></div></div>