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

Jeehoon Kang jeehoon.kang at sf.snu.ac.kr
Wed Dec 7 11:19:22 CET 2016


Dear Iris Club,

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...)

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

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

Best regards,
Jeehoon

-- 
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/20161207/f6532ba3/attachment.html>


More information about the Iris-Club mailing list