Here are
85 public repositories
matching this topic...
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
Updated
Aug 10, 2020
OCaml
Verification system for effectful programs
Agda is a dependently typed programming language / interactive theorem prover.
Updated
Aug 10, 2020
Haskell
Introduction to programming language theory in Agda
A port of Coq to Javascript -- Run Coq in your Browser
Updated
Aug 8, 2020
JavaScript
This repo is the new home of Proof General
Updated
Jul 1, 2020
Emacs Lisp
IDE extensions for Proof General's Coq mode
Updated
Jul 29, 2020
Emacs Lisp
Links to tools by subject
The People's Refinement Logic
Updated
Nov 4, 2019
Standard ML
LaTTe : a Laboratory for Type Theory experiments (in clojure)
Updated
Jul 29, 2020
Clojure
"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory
Updated
Jan 10, 2020
OCaml
A Super Kawaii Dependently Typed Programming Language
Updated
Jul 12, 2018
Haskell
A selection of formal proofs in Coq.
Proof assistant based on the λΠ-calculus modulo rewriting
Updated
Aug 10, 2020
OCaml
A formalization of category theory in the Coq proof assistant.
Interactive Coq Proofs in Vim
Updated
Aug 8, 2020
Python
Coq Protocol Playground with Se(xp)rialization of Internal Structures.
Updated
Jul 23, 2020
OCaml
Placeholder for the OwO compiler
Updated
Feb 20, 2019
Rust
Updated
Aug 3, 2020
OCaml
A JavaScript propositional logic and resolution library
Updated
Sep 19, 2017
JavaScript
Towards changing things and see if it proofs
Updated
Jun 28, 2020
Scala
Updated
Feb 27, 2020
Python
Updated
Aug 10, 2020
Isabelle
Proof automation – for Agda, in Agda.
Model finder for higher-order logic
Updated
Jan 13, 2020
OCaml
Type-level well-kinded natural numbers.
Updated
Jun 22, 2020
Haskell
Resources for "One Monad to Prove Them All"
Fitch style proof constructor
Updated
Jul 21, 2020
JavaScript
A non-interactive proof assistant using the Haskell type system
Updated
Apr 11, 2020
Haskell
super tiny implementation of higher-order logic proof assistant in lean
Updated
Sep 29, 2019
Lean
Improve this page
Add a description, image, and links to the
proof-assistant
topic page so that developers can more easily learn about it.
Curate this topic
Add this topic to your repo
To associate your repository with the
proof-assistant
topic, visit your repo's landing page and select "manage topics."
Learn more
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session.
You signed out in another tab or window. Reload to refresh your session.