#+TITLE: Theorem prover https://github.com/wilbowma/cur [[https://github.com/project-oak/oak-hardware][formal specification and verification of hardware]] [[https://github.com/u2zv1wx/neut][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 [[https://hol-theorem-prover.org/][HOL Interactive Theorem Prover]] [[https://wwwlehre.dhbw-stuttgart.de/~sschulz/E/E.html][The E Theorem Prover]] [[https://softwarefoundations.cis.upenn.edu/][Software Foundations]] [[https://galois.com/blog/2018/07/vellvm-verifying-the-llvm/][Vellvm - Verifying the LLVM - Galois, Inc.]] [[https://github.com/rntz/datafun][rntz/datafun: Research on integrating datalog & lambda calculus via monoton]] [[https://github.com/patio11/wrightverification/blob/master/README.md][wrightverification/README.md at master · patio11/wrightverification]] [[https://m.youtube.com/watch?feature=youtu.be&t=4674&v=ZkDC4aizsqQ][Verification Mentoring Workshop: Session 1 - YouTube]] [[https://github.com/lvm/build-supercollider][lvm/build-supercollider: A dead simple script that builds and installs Supe]] [[https://www.reddit.com/r/ProgrammingLanguages/comments/hx442x/a_formally_verified_highlevel_synthesis_tool/][A formally verified high-level synthesis tool based on CompCert and written]] [[https://arxiv.org/abs/2010.00774][[2010.00774] Proof Repair Across Type Equivalences]] [[https://github.com/tevador/RandomX][tevador/RandomX: Proof of work algorithm based on random code execution]] https://hol-theorem-prover.org/ http://acl2s.ccs.neu.edu/acl2s/doc/ [[https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/index.html][homotopy type theory in agda]] [[file:math.org][Math]] [[https://www.youtube.com/watch?app=desktop&v=VxINoKFm-S4][a little taste of dependent types]] [[https://leanprover.github.io/logic_and_proof/propositional_logic_in_lean.html#exercises][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 [[file:math.org][Math]] [[https://leanprover-community.github.io/undergrad.html][an entire undergraduate math cirriculum in the lean theorem prover!!!!!!!!!!!!!!!!!!!]]