<div dir="ltr"><div><div><div><div><div>Dear Iris Club,<br><br></div>I have some questions on the Iris 3.0 paper ;-)<br><br>- Laws for timeless assertions in Figure 1:<br></div><div>  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...)<br></div><div><br></div>- Theorem 4.1: I think `e_i` is a misspelling of `e'_i`.<br><br></div>- The "later-intro" rule is used without introduction. Is it intended?<br><br></div>Best regards,<br></div>Jeehoon<br><br><div><div><div><div><div><div>-- <br><div class="gmail_signature"><div dir="ltr"><a href="http://sf.snu.ac.kr/jeehoon.kang" target="_blank">Jeehoon Kang (Ph.D. student)</a><div><a href="http://sf.snu.ac.kr" target="_blank">Software Foundations Laboratory</a><div><a href="http://www.snu.ac.kr" target="_blank">Seoul National University</a></div></div></div></div>
</div></div></div></div></div></div></div>