<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">
Dear Jeehon,
<div class="">See my paper with Ales Bizjak</div>
<div class=""> <a href="http://cs.au.dk/~birke/papers/box-modality-conf.pdf" class="">http://cs.au.dk/~birke/papers/box-modality-conf.pdf</a></div>
<div class="">which among other things show that you cannot get</div>
<div class="">a well-behaved box modality that picks out exactly the duplicable</div>
<div class="">resources.</div>
<div class="">I’ll try to add the paper to the <a href="http://iris-project.org" class="">
iris-project.org</a> page.</div>
<div class="">Best,</div>
<div class="">Lars</div>
<div class=""><br class="">
<div class="">
<div style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0); font-family: Helvetica; font-size: 14px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px; text-decoration: none;">
—<br class="">
Lars Birkedal<br class="">
Professor, Villum Investigator<br class="">
Head of Logic and Semantics Group<br class="">
Department of Computer Science<br class="">
Aarhus University<br class="">
<a href="http://www.cs.au.dk/~birke" class="">www.cs.au.dk/~birke</a><br class="">
birkedal@cs.au.dk</div>
</div>
<div><br class="">
<blockquote type="cite" class="">
<div class="">On 13 Jul 2019, at 03.20, Jeehoon Kang <<a href="mailto:jeehoon.kang@kaist.ac.kr" class="">jeehoon.kang@kaist.ac.kr</a>> wrote:</div>
<br class="Apple-interchange-newline">
<div class="">
<div dir="ltr" class="">
<div class="">Dear Iris Club,</div>
<div class=""><br class="">
</div>
<div class="">In the "Iris From the Ground Up" journal paper, it's said that persistent and duplicable resources are different things. There's an example: "exists q, l |->_q v" is duplicable, but not persistent (p15,
<a href="https://people.mpi-sws.org/~dreyer/papers/iris-ground-up/paper.pdf" target="_blank" class="">
https://people.mpi-sws.org/~dreyer/papers/iris-ground-up/paper.pdf</a>).</div>
<div class=""><br class="">
</div>
<div class="">But are there any technical reasons why the example should not be persistent?</div>
<div class="">The resource "lost" the information on q, so we can never be able to take it back completely, anyway.</div>
<div class="">In that sense, maybe we can say it's persistent?<br class="">
</div>
<div class=""><br class="">
</div>
<div class="">
<div dir="ltr" class="gmail-m_-8571025026107835115gmail_signature">
<div class="">Thanks,</div>
<div class="">Jeehoon</div>
</div>
</div>
</div>
-- <br class="">
<a href="mailto:iris-club@lists.mpi-sws.org" class="">iris-club@lists.mpi-sws.org</a> - Mailing List for the Iris Logic<br class="">
Management: <a href="https://lists.mpi-sws.org/listinfo/iris-club" class="">https://lists.mpi-sws.org/listinfo/iris-club</a><br class="">
Unsubscribe: <a href="mailto:iris-club-unsubscribe@lists.mpi-sws.org" class="">iris-club-unsubscribe@lists.mpi-sws.org</a><br class="">
</div>
</blockquote>
</div>
<br class="">
</div>
</body>
</html>