[Iris-Club] Several small questions on Iris

[Jeehoon Kang]

Thank you for answering all the questions I have asked.  Always your
answers enlightened me a lot :)  Here are the remaining questions to the
answers.



On ξ and ξ^{−1}: I agree that it is not worth an issue to examine further.
I realized that what I wanted to ask is: how it is done in Coq?



Indeed, if you do that in Coq, you get a universe conflict.  And I think
> that's not just superficial; if you do the same in set theory, you would
> get the same problem -- the "CMRA of all CMRAs" can't contain itself, or
> else Russel comes and hits you with his paradox.
>

But you anyway need to provide the list of CMRAs, right?  Then the list of
CMRAs can also be interpreted as a CMRA, while it does not incur universe
size problem.  I would like to ask if we could do the same technique here:
just define the logic with the product of all CMRAs (whose size is less
than something), and let users to use only those CMRAs that are small
enough.

I am quite sure my explanation is bad :-\  maybe it would be better for me
to contribute to Iris in this respect (or learn why it is difficult to do
that by actually doing some proofs in Coq).  I will return to this subject
as soon as I am used to iris-coq.



On composability: what about "compositionality" as said in the parametric
(bi)simulation works?



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/20170204/b08328a3/attachment.html>