Zulip Chat Archive

Stream: Program verification

Topic: Correctness of a compiler for arithmetic expressions

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

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?

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.).

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.

Xi Wang (Oct 20 2020 at 00:43):

Thanks for the pointer!

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: Dec 20 2023 at 11:08 UTC