[Iris-Club] Distinguishing persistent and duplicate resources

Ralf Jung jung at mpi-sws.org
Wed Jul 17 14:07:01 CEST 2019

Hi Jeehoon,

to follow up on that:  We *could* make `exists q, l |->{q} v` persistent if we
were to give up on being able to commute existential quantifiers with the
persistence modality.  Specifically, we would lose

  <pers> exists x, P |- exists x, <pers> P

Clearly, if `exists q, l |->{q} v` is persistent that rule makes no sense. Joe
actually proposed an implementation of this at
<https://gitlab.mpi-sws.org/iris/iris/merge_requests/132>, but that also loses a
few other proof rules and is part of the more general question about the "right"
axioms for persistence and the "core" operation in resource algebras.

Kind regards,

On 13.07.19 06:56, Lars Birkedal wrote:
> 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>

Website: https://people.mpi-sws.org/~jung/

More information about the Iris-Club mailing list