Zulip Chat Archive

Stream: Program verification

Topic: Concrete semantics


view this post on Zulip 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

view this post on Zulip John Hui (May 19 2020 at 06:56):

I'm interested!

view this post on Zulip 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

view this post on Zulip Simon Hudon (May 21 2020 at 18:44):

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

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Jun 27 2020 at 16:51):

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

view this post on Zulip 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