33 results found Sort:
- Filter by Primary Language:
- OCaml (6)
- Python (5)
- Coq (4)
- Rust (3)
- Haskell (3)
- Standard ML (2)
- Emacs Lisp (2)
- TypeScript (1)
- Clojure (1)
- F* (1)
- Isabelle (1)
- Java (1)
- Scala (1)
- Agda (1)
- +
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
44,367 commits to master branch, last one 22 hours ago
A Proof-oriented Programming Language
Created
2014-04-03
37,870 commits to master branch, last one 16 hours ago
Agda is a dependently typed programming language / interactive theorem prover.
Created
2015-08-08
23,097 commits to master branch, last one 5 days ago
An introduction to programming language theory in Agda
Created
2017-03-10
2,971 commits to dev branch, last one a day ago
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 about a month ago
This repo is the new home of Proof General
Created
2015-09-21
9,446 commits to master branch, last one about a month ago
Verified Software Toolchain
Created
2014-11-21
7,697 commits to master branch, last one 2 months ago
Links to tools by subject
Created
2013-09-24
1 commits to main branch, last one about a year ago
Verification framework and tool for higher-order Scala programs
Created
2016-08-17
4,038 commits to main branch, last one 14 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 about a year ago
My personal repository of formally verified mathematics.
Created
2017-07-04
1,338 commits to main branch, last one 23 days ago
A proof assistant and a dependently-typed language
Created
2020-11-09
4,636 commits to main branch, last one 2 days ago
Proof assistant based on the λΠ-calculus modulo rewriting
Created
2017-09-10
3,803 commits to master branch, last one 2 days ago
Interactive Coq Proofs in Vim
Created
2017-05-31
595 commits to main branch, last one 2 months ago
LaTTe : a Laboratory for Type Theory experiments (in clojure)
Created
2015-03-04
440 commits to master branch, last one 11 months 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
😎TT
Created
2019-12-20
609 commits to main branch, last one about a year ago
An experimental proof assistant based on a type theory for synthetic ∞-categories.
Created
2020-11-26
798 commits to develop branch, last one a day ago
"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
A Platform for High-Level Parametric Hardware Specification and its Modular Verification
Created
2017-07-11
1,470 commits to rv32i branch, last one about a month ago
Coq Protocol Playground with Se(xp)rialization of Internal Structures.
Created
2016-05-26
1,100 commits to main branch, last one 7 days ago
Large Scale Type Systems (programming language)
Created
2021-09-10
1,414 commits to main branch, last one 15 hours ago
Jupyter kernel for Coq
Created
2018-12-26
155 commits to master branch, last one 10 months ago
A Rust/WASM implementation of homotopy.io
Created
2020-09-17
1,758 commits to master branch, last one 9 days ago
Athena is a modern, practical language for proof engineering & natural deduction.
Created
2022-05-02
116 commits to master branch, last one 2 days ago
This repository has no description...
Created
2016-08-10
1,559 commits to master branch, last one 16 days ago
Semi-Automated Python Proof Assistant
Created
2022-11-08
90 commits to main branch, last one 6 days ago
🦠 An experimental elaborator for dependent type theory using effects and handlers
Created
2022-04-23
85 commits to main branch, last one about a year ago
♾️ A library for universe levels and universe polymorphism
Created
2022-04-17
90 commits to main branch, last one about a month ago
Template for blueprint-driven formalization projects in Lean.
Created
2024-07-26
114 commits to main branch, last one 11 days ago