Concrete semantics

Stream: Program verification

[Simon Hudon]

Last year, I created a channel called #concrete semantics semantics to form a reading group for the Concrete Semantics book and translate it collectively in Lean. It never really caught on but if people in this stream are interested, we can try again

[John Hui]

I'm interested!

[Simon Hudon]

Awesome! Let's start with chapter 1 and see how we do. I've already done chapter 1, so let me know if you hit any obstacle

[Simon Hudon]

Did anyone manage to write the proofs about constant folding in chapter 3?

[Spencer Killen]

There's some overlap between Concrete Semantics and https://github.com/blanchette/logical_verification_2020/raw/master/hitchhikers_guide.pdf

[Karl Palmskog]

Maybe you have already seen https://github.com/lukaszcz/COQ-IMP https://arxiv.org/abs/1808.06413

[Simon Hudon]

I hadn't seen it, thanks for the reference!