<div dir="ltr">Dear Iris Club,<div><br></div><div>In the ICFP 2016 paper is said "Iris is an intuitionistic separation logic, which gives rise to the monotonicity requirement".  I wonder if someone is developing a classical version of Iris.</div><div><br></div><div>Background: I heard (from some of the Iris authors ;-) that Iris is related the RustBelt project which aims to verify "unsafe" Rust programs, which (I guess) involves verification of safe memory disposal.  And I just learned from a classic textbook (<a href="https://www.cs.cmu.edu/~jcr/copenhagen08.pdf">https://www.cs.cmu.edu/~jcr/copenhagen08.pdf</a>) that verification of safe memory disposal requires classical separation logic..</div><div><div><br></div><div>Best,</div><div>Jeehoon</div><div><br></div><div><div>PS. Sorry for cluttering everyone's inbox by sending a lot of emails..  I will at least try to say something useful.  Thank you for answering all the questions!</div></div><div><br></div>-- <br><div class="gmail_signature" data-smartmail="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>