====== Interesting Coq Projects ======

{{htmlmetatags>
metatag-media-og:image=({ :a:coq:coq-logo-large.png?400|})
metatag-og:title=(Interesting Coq Projects)
}}

This is a collection of Coq projects I find particularly interesting for one reason or another.

===== Projects =====

{|
! Name
! Categories
! Notes
|-
| [[https://softwarefoundations.cis.upenn.edu/|Software Foundations]] || Theory of Computation, High-Assurance Computing || In my opinion, the greatest resource for learning Coq (or the foundations of verification in general). Completely free, incredibly easy to read, no confusing notation, and the textbook source is Coq files that you can download and work in. 
|-
| [[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.
|}

===== My Projects =====


{|
! Name
! Categories
! Notes
|- 
| [[https://github.com/CharlesAverill/Software-Foundations-Checklist/|Software Foundations]] || Theory of Computation, High-Assurance Computing || My solutions are not public due to an explicit request by the authors not to publish solutions. The linked repository is the list of exercises I've completed.
|-
| [[https://github.com/CharlesAverill/volpic/|VOLPIC]] || High-Assurance Computing || A verification pipeline for Pascal source code. 
|-
| ''memset'' || High-Assurance Computing || Verified the correctness of the ''memset'' function on Arm32 platforms. The proof is not yet public.
|-
| [[https://github.com/CharlesAverill/HCLT/|Haskell Curry's Living Thesis]] || Theory of Computation || An in-progress Coq implementation of Haskell Curry's Ph.D. thesis. This project is between refactors at the moment, I'm having a hard time deciding how close I want the proofs to be to their originals. Curry does not use constructivist logic for his proofs here, causing the trouble.
|-
| [[https://github.com/CharlesAverill/CoqPhysicsExperiments/|Coq Physics Experiments]] || Physics || A collection of attempts at formalizing some mathematics required for physical systems. A large portion of it was initially written as I followed along with Terence Tao's "Analysis I". This is generally un-maintained. 
|}