[Iris-Club] Distinguishing persistent and duplicate resources

[Lars Birkedal]

Dear Jeehon,
See my paper with Ales Bizjak
   http://cs.au.dk/~birke/papers/box-modality-conf.pdf
which among other things show that you cannot get
a well-behaved box modality that picks out exactly the duplicable
resources.
I’ll try to add the paper to the iris-project.org<http://iris-project.org> page.
Best,
Lars

—
Lars Birkedal
Professor, Villum Investigator
Head of Logic and Semantics Group
Department of Computer Science
Aarhus University
www.cs.au.dk/~birke<http://www.cs.au.dk/~birke>
birkedal at cs.au.dk

On 13 Jul 2019, at 03.20, Jeehoon Kang <jeehoon.kang at kaist.ac.kr<mailto:jeehoon.kang at kaist.ac.kr>> wrote:

Dear Iris Club,

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, https://people.mpi-sws.org/~dreyer/papers/iris-ground-up/paper.pdf).

But are there any technical reasons why the example should not be persistent?
The resource "lost" the information on q, so we can never be able to take it back completely, anyway.
In that sense, maybe we can say it's persistent?

Thanks,
Jeehoon
--
iris-club at lists.mpi-sws.org<mailto: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<mailto: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/20190713/aa444bfa/attachment.html>