๐Ÿ“• subnode [[@jakeisnt/theoremprover]] in ๐Ÿ“š node [[theoremprover]]
๐Ÿ“• text contributed by @jakeisnt ๐Ÿ”—

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 agdaMath 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!!!!!!!!!!!!!!!!!!!

Receiving pushes... (requires JavaScript)
Loading context... (requires JavaScript)
๐Ÿ“– stoas (collaborative spaces) for [[@jakeisnt/theoremprover]]