Zulip Chat Archive

Stream: Program verification

Topic: Correctness of a compiler for arithmetic expressions


view this post on Zulip Xi Wang (Oct 15 2020 at 20:10):

Just for fun, coded up the proof from the 1967 paper "Correctness of a compiler for arithmetic expressions" in Lean: https://github.com/xiw/arithcc

view this post on Zulip Simon Hudon (Oct 15 2020 at 20:45):

Nice! I think that could be the kind of stuff we put in the mathlib archive directory. @Rob Lewis What do you think?

view this post on Zulip Xi Wang (Oct 19 2020 at 21:21):

@Simon Hudon That would be awesome! Let me know if there's anything I can help with (splitting into smaller files, or merging the example into one file, etc.).

view this post on Zulip Simon Hudon (Oct 19 2020 at 21:43):

Are you familiar with the pull request (PR) process? You can have a look here: https://leanprover-community.github.io/contribute/index.html

It will show you have to create a version of mathlib that contains your code, it will let mathlib contributors and maintainers comment on it and suggest improvements.

view this post on Zulip Xi Wang (Oct 20 2020 at 00:43):

Thanks for the pointer!

view this post on Zulip Simon Hudon (Oct 20 2020 at 00:47):

Please let me know when you make that pull request or if you need more


Last updated: May 08 2021 at 21:09 UTC