[Iris-Club] Iris on top of "real-world" languages

Robbert Krebbers mail at robbertkrebbers.nl
Thu Oct 11 13:46:18 CEST 2018

Hi Gregory,

To mention another more "real-world" (albeit now low-level) language, 
there are currently some ideas circling around to make heap_lang (the 
default language used in the Iris repo) more like OCaml, by adding 
pattern matching and mutable arrays/records, see e.g. 


On 10/10/18 10:39 PM, Gregory Malecha wrote:
> Hello --
> I'm wondering how much work there has been applying Iris to reason about 
> "real-world" languages. I was really impressed with the RustBelt work, 
> and was wondering if there has been any work applying it to build 
> program logics on top of languages such as C, C++, Rust, or even assembly.
> Any pointers would be greatly appreciated. Even if there isn't any work 
> right now, if there is anyone interested either in producing or 
> consuming this sort of work, it would be great to know about interest.
> Thank you.
> -- 
> gregory malecha
> gmalecha.github.io <https://gmalecha.github.io>

More information about the Iris-Club mailing list