<div dir="ltr">Thank you for the detailed explanation.  After reading it I am almost convinced that the logic really should be named Iris.. and want to buy you a cup of beer!<div><br></div><div>> <span style="font-size:14px">I decided it was better not to name a logic after my wife.</span></div><div><span style="font-size:14px">I will keep that in my mind for the case that I could be married to someone :-)</span></div><div><span style="font-size:14px"><br></span></div><div><span style="font-size:14px">Probably in a near future I will come up with more questions on the Iris logic and its semantic domains, and possibly the Coq formalization.  Thank you for running a mailing list for newbies.</span></div><div><span style="font-size:14px"><br></span></div><div><span style="font-size:14px">Best,</span></div><div><span style="font-size:14px">Jeehoon</span></div><div><span style="font-size:14px"><br></span></div></div><div class="gmail_extra"><br><div class="gmail_quote">2016-08-04 18:01 GMT+09:00 Ralf Jung <span dir="ltr"><<a href="mailto:jung@mpi-sws.org" target="_blank">jung@mpi-sws.org</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi,<br>
<span class=""><br>
> 1. CMRA stands for "complete metric resource algebra" (or something<br>
> like that: we could never find a very suitable acronym).<br>
<br>
</span>Yeah, that was my original thinking... the acronym never really made<br>
sense, but at least it was pronounceable. ;)<br>
<span class=""><br>
> 2. The logic was originally called ROSE (standing for "resources,<br>
> ownership, separation, and I don't know what the E stood for")<br>
<br>
</span>"E" was for "encapsulation".<br>
<br>
Kind regards,<br>
Ralf<br>
<div class="HOEnZb"><div class="h5"><br>
<br>
--<br>
<a href="mailto:iris-club@lists.mpi-sws.org">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/listinfo/iris-club</a><br>
Unsubscribe: <a href="mailto:iris-club-unsubscribe@lists.mpi-sws.org">iris-club-unsubscribe@lists.mpi-sws.org</a><br>
</div></div></blockquote></div><br><br clear="all"><div><br></div>-- <br><div class="gmail_signature" data-smartmail="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>