rossberg
commented
4 years ago Very nice, thank you for the pointer! I'm looking forward to seeing these integrated into the archive (although tail calls haven't landed in the standard yet, so we might want to keep those separate for the time being). I keep wondering whether we should make mechanisation efforts such as this more visible, e.g., by at least linking to them from somewhere, presumably the spec repo.
Apologies if this is a bad place to post this, I had a tough time deciding which repo would be most fitting.
For my CS Master's thesis I built upon @conrad-watt's Isabelle WebAssembly mechanization and added three proposals: non-trapping float to int, sign extension operators, and tail call. Conrad has (very understandably!) been busy finishing his own (PhD!) thesis, so this hasn't been extensively vetted by anyone better at Isabelle than I. Once he is more available we can hopefully integrate these changes into the published AFP proof.
The source for the mechanization can be found here: https://github.com/jacobmischka/wasm-isabelle
My thesis/writeup on the project and WebAssembly and mechanization as a whole can be found here: https://github.com/jacobmischka/uwm-masters-thesis/releases/tag/1.0.0
Sorry if this comes off as self-advertisement, that's not my intention at all, I just wanted to share my work in case it's deemed useful or interesting.
Thank you! I'm extremely grateful to have been a small part of this community, and hope I might be able to become a larger part now that I've finished my degree and have some more free time.