[Iris-Club] Some questions in the Iris 3.0 paper

Ralf Jung jung at mpi-sws.org
Wed Dec 7 11:47:31 CET 2016


Hi Jehoon,

> I have some questions on the Iris 3.0 paper ;-)
> 
> - Laws for timeless assertions in Figure 1:
>   Are the rules correct for arbitrary assertion P?  Or P needs to be
> timeless for the rules to be correct?  (Honestly I don't understand the
> rules...)

These rules are correct for all P.  The "timeless" in their name is
because they are used to prove things about timelessness. "\later-own"
is used to show that ownership of discrete COFE elements is timeless,
while "\later-timeless" is used to show that universal quantification,
implication and magic wand are timeless if their conclusion is timeless.

Indeed the rules look quite weird and don't convey much intuition on
their own.

> - Theorem 4.1: I think `e_i` is a misspelling of `e'_i`.

Good catch, thanks!

> - The "later-intro" rule is used without introduction. Is it intended?

We have the following remark in §2.6:

> Note that many of the usual rules for
> later, such as introduction and commutativity with other operators
> are derivable from the rules in Figure 1.

Indeed \later-Intro can be derived from Löb.  Doing so is a fun exercise ;)

Kind regards,
Ralf




More information about the Iris-Club mailing list