[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,
Ralf

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