36 results found Sort:

667
4.9k
lgpl-2.1
104
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 developme...
Created 2011-02-17
45,091 commits to master branch, last one 10 hours ago
237
2.8k
apache-2.0
80
A Proof-oriented Programming Language
Created 2014-04-03
38,330 commits to master branch, last one 21 hours ago
367
2.6k
other
66
Agda is a dependently typed programming language / interactive theorem prover.
Created 2015-08-08
23,193 commits to master branch, last one 5 days ago
327
1.4k
cc-by-4.0
25
An introduction to programming language theory in Agda
Created 2017-03-10
2,987 commits to dev branch, last one 2 days ago
45
522
other
19
A port of Coq to Javascript -- Run Coq in your Browser
Created 2015-05-12
1,804 commits to v8.20+lsp branch, last one 4 months ago
91
499
gpl-3.0
13
This repo is the new home of Proof General
Created 2015-09-21
9,456 commits to master branch, last one 12 days ago
Verified Software Toolchain
Created 2014-11-21
7,704 commits to master branch, last one 25 days ago
54
367
apache-2.0
19
Verification framework and tool for higher-order Scala programs
Created 2016-08-17
4,067 commits to main branch, last one 13 days ago
A Coq IDE build on top of Proof General's Coq mode
Created 2015-02-15
905 commits to master branch, last one 2 years ago
36
299
other
14
Proof assistant based on the λΠ-calculus modulo rewriting
Created 2017-09-10
3,829 commits to master branch, last one 5 days ago
A proof assistant and a dependently-typed language
Created 2020-11-09
5,307 commits to main branch, last one 2 days ago
12
295
other
11
My personal repository of formally verified mathematics.
Created 2017-07-04
1,376 commits to main branch, last one 16 days ago
33
282
mit
7
Interactive Coq Proofs in Vim
Created 2017-05-31
597 commits to main branch, last one about a month ago
LaTTe : a Laboratory for Type Theory experiments (in clojure)
Created 2015-03-04
440 commits to master branch, last one about a year ago
The People's Refinement Logic
This repository has been archived (exclude archived)
Created 2016-01-05
1,013 commits to master branch, last one 5 years ago
14
222
apache-2.0
20
😎TT
Created 2019-12-20
609 commits to main branch, last one about a year ago
10
216
unknown
11
An experimental proof assistant based on a type theory for synthetic ∞-categories.
Created 2020-11-26
800 commits to develop branch, last one 2 months ago
12
206
apache-2.0
25
"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory
Created 2018-03-07
1,139 commits to master branch, last one 2 years ago
25
146
mit
14
A Platform for High-Level Parametric Hardware Specification and its Modular Verification
Created 2017-07-11
1,470 commits to rv32i branch, last one 4 months ago
Coq Protocol Playground with Se(xp)rialization of Internal Structures.
Created 2016-05-26
1,100 commits to main branch, last one 2 months ago
8
95
apache-2.0
5
Jupyter kernel for Coq
Created 2018-12-26
155 commits to master branch, last one about a year ago
A formalization of category theory in the Coq proof assistant.
Created 2015-10-14
160 commits to master branch, last one 4 years ago
7
92
bsd-3-clause
5
A Rust/WASM implementation of homotopy.io
Created 2020-09-17
1,761 commits to master branch, last one 2 months ago
8
91
gpl-3.0
5
An experimental unification-based programming language with logic-agnostic types, based on Girard's transcendental syntax
Created 2023-05-03
218 commits to master branch, last one a day ago
A Low Barrier Proof Assistant
Created 2022-11-08
176 commits to main branch, last one 2 days ago
Athena is a modern, practical language for proof engineering & natural deduction.
Created 2022-05-02
135 commits to master branch, last one 2 months ago
Template for blueprint-driven formalization projects in Lean.
Created 2024-07-26
131 commits to main branch, last one a day ago