[Iris-Club] Intention of later(False) in timeless predicate

Jeehoon Kang jeehoon.kang at sf.snu.ac.kr
Mon Aug 22 07:00:17 CEST 2016

Dear Iris Club,

In the Iris 2.0 documentation, the timeless predicate is defined as follows
(page 11):
Γ |- timeless(P) <=> Γ | later(P) |- P ∨ later(False)

I guess the intention of the later(False) disjunct is allowing more
predicates to be timeless.  But I am not sure which rule of "Laws for the
later modality" (page 14) requires the later(False) disjunct.  May I ask is
it really used?

Thank you,

Jeehoon Kang (Ph.D. student) <http://sf.snu.ac.kr/jeehoon.kang>
Software Foundations Laboratory <http://sf.snu.ac.kr>
Seoul National University <http://www.snu.ac.kr>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mpi-sws.org/pipermail/iris-club/attachments/20160822/7d14273a/attachment.html>

More information about the Iris-Club mailing list