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

[Robbert Krebbers]

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. 
https://gitlab.mpi-sws.org/FP/iris-coq/issues/124#note_30625

Robbert

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