Stream: Program verification
Topic: Concrete semantics
Simon Hudon (May 18 2020 at 15:11):
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 (May 19 2020 at 06:56):
Simon Hudon (May 19 2020 at 13:15):
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 (May 21 2020 at 18:44):
Did anyone manage to write the proofs about constant folding in chapter 3?
Spencer Killen (May 29 2020 at 19:57):
There's some overlap between Concrete Semantics and https://github.com/blanchette/logical_verification_2020/raw/master/hitchhikers_guide.pdf
Karl Palmskog (Jun 27 2020 at 16:51):
Simon Hudon (Jun 27 2020 at 18:36):
I hadn't seen it, thanks for the reference!
Last updated: May 08 2021 at 22:13 UTC