Differences
This shows you the differences between two versions of the page.
| |
| a:coq:projects [2024/03/27 21:18] – created charles | a:coq:projects [2024/03/27 21:33] (current) – [Projects] charles |
|---|
| |- | |- |
| | [[https://personal.utdallas.edu/~hamlen/hamlen19feast.pdf|Source-free, Machine-checked Validation of Native Code in Coq]] || High-Assurance Computing || A platform for verifying the correctness of binary code. The below-mentioned ''memset'' proof was written in (a much more recent version of) this system. | | [[https://personal.utdallas.edu/~hamlen/hamlen19feast.pdf|Source-free, Machine-checked Validation of Native Code in Coq]] || High-Assurance Computing || A platform for verifying the correctness of binary code. The below-mentioned ''memset'' proof was written in (a much more recent version of) this system. |
| | |- |
| | | [[https://metacoq.github.io/|MetaCoq]] || Theory of Computation || "MetaCoq is a project formalizing Coq in Coq and providing tools for manipulating Coq terms and developing certified plugins (i.e. translations, compilers or tactics) in Coq." |
| |- | |- |
| | [[https://dash.harvard.edu/handle/1/38811518|A Formalization of Elements of Special Relativity in Coq]] || Physics || So far, the only paper I've seen exploring axiomatic physics in Coq. The code is painfully undocumented and I have not been able to find the author on any other platforms. | | [[https://dash.harvard.edu/handle/1/38811518|A Formalization of Elements of Special Relativity in Coq]] || Physics || So far, the only paper I've seen exploring axiomatic physics in Coq. The code is painfully undocumented and I have not been able to find the author on any other platforms. |
