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.
A Proof-oriented Programming Language
Agda is a dependently typed programming language / interactive theorem prover.
An introduction to programming language theory in Agda
A port of Coq to Javascript -- Run Coq in your Browser
This repo is the new home of Proof General
Verified Software Toolchain
Links to tools by subject
A Coq IDE build on top of Proof General's Coq mode
Verification framework and tool for higher-order Scala programs
My personal repository of formally verified mathematics.
A proof assistant and a dependently-typed language
Proof assistant based on the λΠ-calculus modulo rewriting
LaTTe : a Laboratory for Type Theory experiments (in clojure)
The People's Refinement Logic
😎TT
"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory
An experimental proof assistant based on a type theory for synthetic ∞-categories.
A Super Kawaii Dependently Typed Programming Language
Add a description, image, and links to the proof-assistant topic page so that developers can more easily learn about it.
To associate your repository with the proof-assistant topic, visit your repo's landing page and select "manage topics."