Stream: Coq users

Topic: low level langues formalized in Coq


view this post on Zulip Bas Spitters (May 08 2020 at 12:01):

This might turn into it's own topic, but let me put it here for now.
There are currently (at least) two low level languages formalized in Coq, jasmin and bedrock2.
I'm wondering how they compare. @Jason Gross ?
https://github.com/mit-plv/fiat-crypto/issues/783

view this post on Zulip Jason Gross (May 09 2020 at 18:26):

@Bas Spitters I don't have much interesting to say on this (I just replied to the issue). A good way of seeing how they compare might be seeing how much work it takes to port the bedrock2 backend for fiat-crypto to Jasmin


Last updated: Feb 01 2023 at 11:04 UTC