SAIL to Lean

Stream: Program verification

[Jakob von Raumer]

Does anyone know of any efforts to have SAIL specs export to Lean?

[Andrés Goens]

I know that @Siddharth Bhat was looking into it, not sure what the current status is though

[Siddharth Bhat]

I would CC @Tobias Grosser on this. There is a general interest from our group, but it’s not on our critical path at the moment.

[Tobias Grosser]

I am interested, indeed and am currently in conversations how to build this best.

[Tobias Grosser]

:smile:

[Jakob von Raumer]

Written in ML like the other backends?

[Alexander Hicks]

I've spoken to some people from about this as it's relevant for a project I'm working on and there are plans to get some work done on this, specifically adding support for Lean to the RISC-V SAIL spec. @Tobias Grosser what are your current plans?

[Tobias Grosser]

Hi @Alexander Hicks, I have a postdoc who just started looking into this. Happy to coordinate here.

[Tobias Grosser]

@Hugo Pompougnac, this might interest you.

[Tobias Grosser]

@Alexander Hicks, happy to arrange for a call to chat about this.

[Alexander Hicks]

I'll send you an e-mail :smile: @Tobias Grosser

[Jakob von Raumer]

Jakob von Raumer said:

Written in ML like the other backends?

I kind of asked this because I think writing a backend that spits out a Lean file is imho less desirable than writing a SAIL parser in Lean and writing a Lean syntax extension to access the generated terms