fcf
fcf copied to clipboard
adampetcher
Foundational Cryptography Framework for machine-checked proofs of cryptography.
Since FCF is useful and seems to have at least one maintainer (for example, @andres-erbsen), I suggest that FCF should be released via opam in the coq-released archive, and then...
In various tactics such as fcf_skip, the use of "intuition" leads to this warning in Coq 8.17: ``` Warning: "auto with *" was used through the default "intuition_solver" tactic. This...
There are a lot of deprecation warnings when compiling FCF with Coq 8.16. It might be worth fixing these, to save trouble in the future.
As described in PrincetonUniversity/VST#290, the use of `Qed` when creating typeclass instances makes it so that you can't evaluate expressions using the typeclass: ```coq Compute 1 ?= 1. = (let...
`I would prefer to keep the non-building files in the repo for the following reasons: They still can be useful illustrations (especially the examples). There may be some argument in...
`If you like, you can remove the entire ESPADA directory. I don't plan to maintain this proof. If you do this, create a ticket (assigned to me) reminding me to...
We need to fix the following copyright and license issues: 1) Give attribution and copyright ownership to contributors. At present, everything is still marked as copyright Adam Petcher 2) It...
Metadata
Owner
Metadata
Foundational Cryptography Framework for machine-checked proofs of cryptography.