<div dir="ltr">We actually used "composability" sometimes in the parametric bisimulation work as well:<div><br></div><div><a href="https://people.mpi-sws.org/~dreyer/papers/rts-trans/tr.pdf" target="_blank">https://people.mpi-sws.org/~<wbr>dreyer/papers/rts-trans/tr.pdf</a><br></div><div><br></div><div>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".</div><div><br></div><div>Derek</div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, Feb 4, 2017 at 11:42 PM, Jeehoon Kang <span dir="ltr"><<a href="mailto:jeehoon.kang@sf.snu.ac.kr" target="_blank">jeehoon.kang@sf.snu.ac.kr</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><span class="m_-6264338119179934930m_-4848948806966818729gmail-m_-9204929174622241972gmail-"></span>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.<br><br><br><br>On <span class="m_-6264338119179934930m_-4848948806966818729gmail-m_-9204929174622241972gmail-">ξ 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?<br></span><br><br><br><div><div class="gmail_extra"><div class="gmail_quote"><span><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
Indeed, if you do that in Coq, you get a universe conflict.  And I think<br>
that's not just superficial; if you do the same in set theory, you would<br>
get the same problem -- the "CMRA of all CMRAs" can't contain itself, or<br>
else Russel comes and hits you with his paradox.<br></blockquote><div><br></div></span><div>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.<br><br></div><div>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.<br></div><div><br><br><br></div><div>On composability: what about "compositionality" as said in the parametric (bi)simulation works?<br clear="all"></div></div><br><br><br></div><span><div class="gmail_extra">Best regards,<br></div><div class="gmail_extra">Jeehoon<br></div><div class="gmail_extra"><br><br>-- <br><div class="m_-6264338119179934930m_-4848948806966818729gmail-m_-9204929174622241972gmail_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></span></div></div>
<br>--<br>
<a href="mailto:iris-club@lists.mpi-sws.org" target="_blank">iris-club@lists.mpi-sws.org</a> - Mailing List for the Iris Logic<br>
Management: <a href="https://lists.mpi-sws.org/listinfo/iris-club" rel="noreferrer" target="_blank">https://lists.mpi-sws.org/list<wbr>info/iris-club</a><br>
Unsubscribe: <a href="mailto:iris-club-unsubscribe@lists.mpi-sws.org" target="_blank">iris-club-unsubscribe@lists.mp<wbr>i-sws.org</a><br>
<br></blockquote></div><br></div></div>