[Iris-Club] Classical version of Iris?
jeehoon.kang at sf.snu.ac.kr
Sun Aug 14 14:08:52 CEST 2016
Dear Iris Club,
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.
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 (https://www.cs.cmu.edu/~jcr/copenhagen08.pdf) that
verification of safe memory disposal requires classical separation logic..
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
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...
More information about the Iris-Club