[Iris-Club] Several small questions on Iris

[Jeehoon Kang]

Dear Iris Club,


As usual, I have several small questions on Iris :)


First things first, here are references:
- [1] Iris 3.0 paper
- [2] Iris 3.0 appendix


Now questions:

- 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?

- 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?

- What is "c" in the definition of AG(T) [2, S3.5, p11]?

- 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."

- I think "Res" in the definition of the interpretation of entailment in
[2, p20], should be "M".

- 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.)

- typo: "ruels" in [2, p22]

- typo: "Stateof" in [2, p24] (rather than "State of")


Best regards,
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/20170131/bccfe21b/attachment.html>