Lean mathematical components library
-
Updated
Aug 20, 2021 - Lean
#
formal-proofs
Here are 35 public repositories matching this topic...
十分钟魔法练习
java
tutorial
functional-programming
lambda-calculus
monad
hkt
adt
formal-verification
formal-proofs
-
Updated
Feb 13, 2021 - HTML
formally verified category theory library
-
Updated
Jun 23, 2020 - Idris
Coq encoding of ZFC and formalization of the textbook Elements of Set Theory
-
Updated
Aug 19, 2021 - Coq
A proof-producing SMT/McSat solver, handling polymorphic first-order logic, and using an SMT/McSat core extended using Tableaux, Superposition and Rewriting.
-
Updated
Feb 4, 2020 - OCaml
The Principia Rewrite
latex
coq
logic
latex-packages
formal-mathematics
coq-ecosystem
formal-proofs
formal-logic
history-of-philosophy
-
Updated
Jun 24, 2021 - Coq
A Coq library providing tactics to deal with hypothesis
-
Updated
Jul 6, 2021 - Coq
Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]
coq
proof
formal-proofs
primitive-recursive-functions
ordinal-notations
hydra-battles
discrete-maths
-
Updated
Aug 20, 2021 - Coq
some simple&naive formal proof of trivial Number Theory, using Agda/Coq, just to practice skills
-
Updated
Feb 10, 2019 - Agda
Formalization of temporal logic in Coq
-
Updated
Dec 15, 2019 - Coq
Formalized quantum computing in Lean theorem prover
-
Updated
Mar 6, 2021 - Lean
-
Updated
Oct 16, 2019 - Lean
-
Updated
Jan 10, 2019 - Lean
CafeOBJ proof of Key Secrecy of PACE with OTS/CafeOBJ.
-
Updated
Apr 1, 2021 - AMPL
Compiling Concurrency Correctly—Verifying Software Transactional Memory
-
Updated
Aug 21, 2017 - TeX
Aris: a logic engine/formal proof interface; 2nd generation, successor to the C version of Aris.
-
Updated
Jun 30, 2020 - Java
An implementation of Algorithm W in Idris with a complete proof
-
Updated
Apr 2, 2019 - Idris
matroids in lean
-
Updated
Dec 21, 2020 - Lean
Paxos algorithm specified and proved in TLA+/PlusCal, with separate processes and invariants for proposers and acceptors.
distributed-systems
verification
paxos
formal-verification
tla
formal-specification
formal-proofs
pluscal
tlaplus
-
Updated
Sep 19, 2018 - TLA
Local mirror of Featherweight OCL entry of the Archive of Formal Proofs (AFP).
-
Updated
Mar 11, 2021 - Isabelle
Coq course materials with my solutions
-
Updated
Mar 29, 2020 - Coq
Group Theory (Second Sylow Theorem) formalized in Naproche.
-
Updated
Mar 14, 2020 - FreeMarker
Examples to get some practice on functional programming and formal proofs
-
Updated
Feb 28, 2019 - Agda
proof
proof-assistant
formal-methods
isabelle
formal-verification
isabelle-hol
itp
interactive-theorem-proving
formal-proofs
-
Updated
Dec 7, 2020 - Isabelle
Extended concepts and for testing software, combining technologies such as Unit / Integration Tests, Interface Testing or Formal Methods such as Model Checking.
testing
unit-testing
integration-testing
software
model-checking
formal-methods
formal-verification
formal-specification
formal-proofs
interface-testing
-
Updated
Apr 17, 2020
Web-based natural deduction proof assistant
-
Updated
Oct 26, 2020 - JavaScript
A formal specification and verification of Tree Sort algorithm in Coq
algorithms
coq
proof-assistant
sorting-algorithms
sorting-algorithms-implemented
formal-verification
formal-proofs
-
Updated
Jul 6, 2020 - Coq
Solutions to Coq exercises from Formal proof: an Introduction to Type Theory class in 2018/1
-
Updated
Sep 28, 2019 - Coq
Improve this page
Add a description, image, and links to the formal-proofs topic page so that developers can more easily learn about it.
Add this topic to your repo
To associate your repository with the formal-proofs topic, visit your repo's landing page and select "manage topics."