[Iris-Club] Several small questions on Iris

[Derek Dreyer]

We actually used "composability" sometimes in the parametric bisimulation
work as well:

https://people.mpi-sws.org/~dreyer/papers/rts-trans/tr.pdf

After thinking about it for a minute, I can't seem to determine any easily
explainable rationale for when I prefer to use "composability" vs.
"compositionality".

Derek

On Sat, Feb 4, 2017 at 11:42 PM, Jeehoon Kang <jeehoon.kang at sf.snu.ac.kr>
wrote:

> 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>
>
> --
> iris-club at lists.mpi-sws.org - Mailing List for the Iris Logic
> Management: https://lists.mpi-sws.org/listinfo/iris-club
> Unsubscribe: iris-club-unsubscribe at lists.mpi-sws.org
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mpi-sws.org/pipermail/iris-club/attachments/20170205/1b3ea106/attachment.html>