Is anyone else working on Iris in Lean?

Stream: Program verification

[Markus de Medeiros]

I've been slowly chipping away at implementing the foundations of Iris in Lean. My goal is to mechanize up to uPred and hook it up to iris-lean; as of now I've implemented a good chunk of the results about OFE's and I'm starting to move up to work on cameras.

This seems like the right place to ask: is anyone else continuing the iris-lean project or otherwise developing Iris in Lean? It would be great to combine our efforts if so :)

[Jireh Loreaux]

I believe @Mario Carneiro is the maintainer of iris-lean now.

[Sebastian Ullrich]

It's not Iris but perhaps https://github.com/verse-lab/splean is worth a look

[Shreyas Srinivas]

I am not actively working on this now, but it was on my todo list early to mid last year. Happy to contribute in anyway I can.

[Shreyas Srinivas]

Will you be porting heaplang?

[Markus de Medeiros]

If the project gets that far, then somebody should definitely do that! I'd probably port the language I work on in my day-to-day Rocq Iris work first, though :)

[Markus de Medeiros]

I don't think there's anything blocking someone from adding the definition of a language+operational semantics+weakestpre+tactics to the existing iris-lean (treating BI as axiomatic and not proving adequacy wrt. Lean). Idk if anyone is working on such a thing (maybe @Mario Carneiro knows?), but in principle that could be done without the model.

[Ira Fesefeldt]

I'd generally be interested in working on Iris in Lean, but I will likely not have any time for it until I finish my phd.

[Mario Carneiro]

@Markus de Medeiros @Ira Fesefeldt I'm not actively working on iris-lean, but PRs are certainly welcome.