# Theorem prover

https://github.com/wilbowma/cur formal specification and verification of hardware dependently typed programming language with compile time malloc/free https://github.com/GaloisInc/lean-llvm llvm support for lean theorem prover https://github.com/gallais/generic-syntax agda repo for a type safe universe of syntaxes https://github.com/crypto-agda/protocols shallow embedding of protocols with agda dependent types https://github.com/cedille/cedille https://github.com/vasilisp/inez constraint solver

HOL Interactive Theorem Prover The E Theorem Prover Software Foundations Vellvm - Verifying the LLVM - Galois, Inc. rntz/datafun: Research on integrating datalog & lambda calculus via monoton wrightverification/README.md at master · patio11/wrightverification Verification Mentoring Workshop: Session 1 - YouTube

lvm/build-supercollider: A dead simple script that builds and installs Supe A formally verified high-level synthesis tool based on CompCert and written [2010.00774] Proof Repair Across Type Equivalences tevador/RandomX: Proof of work algorithm based on random code execution https://hol-theorem-prover.org/ http://acl2s.ccs.neu.edu/acl2s/doc/ homotopy type theory in agda Math a little taste of dependent types 4. Propositional Logic in Lean — Logic and Proof 0.1 documentation

https://itp19.cecs.pdx.edu/ conference on interactive theorem proving : )

https://plv.csail.mit.edu/blog/ blog from adam chlipapa's lab! http://www.cse.chalmers.se/research/group/logic/publications.html

https://www.stephanboyer.com/ a great article for approaching theorem proving is featured here. Look to learn from this as needed!

# math cir

Math an entire undergraduate math cirriculum in the lean theorem prover!!!!!!!!!!!!!!!!!!!