[Iris-Club] Classical version of Iris?

[Jeehoon Kang]

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

Best,
Jeehoon

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!

-- 
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/20160814/57fb2da4/attachment.html>