Verified Software Toolchain
-
Updated
Jul 9, 2024 - Coq
Verified Software Toolchain
My personal repository of formally verified mathematics.
A Platform for High-Level Parametric Hardware Specification and its Modular Verification
Coq Protocol Playground with Se(xp)rialization of Internal Structures.
A formalization of category theory in the Coq proof assistant.
Resources for "One Monad to Prove Them All"
A Coq library providing tactics to deal with hypothesis
A Coq framework to support structural design and proof of hardware cache-coherence protocols
Personal research notes
Simply-typed lambda calculus and extensions: termination, extrinsic/intrinsic representations, nominal binding techniques
My proofs for the Coq proof assistant
A formal specification and verification of Tree Sort algorithm in Coq
Collection of explainatory example proofs for popular proof assistants.
Add a description, image, and links to the proof-assistant topic page so that developers can more easily learn about it.
To associate your repository with the proof-assistant topic, visit your repo's landing page and select "manage topics."