cakeml icon indicating copy to clipboard operation
cakeml copied to clipboard
verified publisher icon CakeML

Export CakeML proofs in OpenTheory format

Open xrchz opened this issue 7 years ago • 1 comments

(Explicitly doing work hinted at in #321). The proofs in particular to package up and export would include the compiler correctness proof (at the machine-code level) and the OpenTheory reader implementation proof. Possible assignees: @michaelsproul, @oskarabrahamsson, @IlmariReissumies -- any interest?

xrchz avatar Aug 25 '18 05:08 xrchz

@digama0 do you have an alternative format for proof recording that might work better for this?

xrchz avatar Dec 09 '24 12:12 xrchz