41 results found Sort:
- Filter by Primary Language:
- Haskell (6)
- Rust (6)
- OCaml (6)
- Agda (4)
- Coq (4)
- TypeScript (3)
- Idris (2)
- C++ (2)
- F* (1)
- Python (1)
- C (1)
- Scala (1)
- Swift (1)
- Java (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,676 commits to master branch, last one 3 days ago
A modern proof language
Created
2018-07-13
279 commits to master branch, last one 21 days ago
A Proof-oriented Programming Language
Created
2014-04-03
37,960 commits to master branch, last one 4 days ago
A purely functional programming language with first class types
Created
2020-05-17
3,788 commits to main branch, last one 3 days ago
Agda is a dependently typed programming language / interactive theorem prover.
Created
2015-08-08
23,157 commits to master branch, last one 7 days ago
Lean Theorem Prover
This repository has been archived
(exclude archived)
Created
2013-07-17
13,725 commits to master branch, last one about a year ago
A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
Created
2020-08-21
195 commits to main branch, last one 9 months ago
A friendly little systems language with first-class types. Very WIP! 🚧 🚧 🚧
Created
2017-12-19
1,071 commits to main branch, last one 3 years ago
Cedille, a dependently typed programming languages based on the Calculus of Dependent Lambda Eliminations
Created
2018-06-22
1,817 commits to master branch, last one 3 years ago
An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification.
Created
2021-04-10
276 commits to main branch, last one 3 days ago
A proof assistant and a dependently-typed language
Created
2020-11-09
5,082 commits to main branch, last one a day ago
Proof assistant based on the λΠ-calculus modulo rewriting
Created
2017-09-10
3,809 commits to master branch, last one 11 days ago
🚧 (Alpha stage software) A declarative data definition language for formally specifying binary data formats. 🚧
Created
2015-01-09
2,650 commits to main branch, last one about a year ago
A Compiler for the Popr Language
Created
2012-10-07
1,802 commits to master branch, last one 3 years ago
A function definition package for Coq
Created
2009-10-27
1,858 commits to main branch, last one 24 days ago
CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory
Created
2018-01-31
597 commits to coq8.20 branch, last one about a month ago
Lecture notes on univalent foundations of mathematics with Agda
Created
2019-03-20
1,048 commits to master branch, last one 8 months ago
Contextual types meet mechanized metatheory!
Created
2015-05-14
5,070 commits to master branch, last one 5 months ago
A garden of small programming language implementations 🪴
Created
2022-09-10
901 commits to main branch, last one 4 days ago
Lecture notes for a short course on proving/programming in Coq via SSReflect.
Created
2014-05-20
437 commits to master branch, last one 3 years ago
Cicada Language (solo version)
Created
2021-03-28
6,372 commits to master branch, last one 5 days ago
A SuperCompiler for Martin-Löf's Type Theory
Created
2013-10-15
527 commits to master branch, last one 2 years ago
Large Scale Type Systems (programming language)
Created
2021-09-10
1,422 commits to main branch, last one 29 days ago
Dependently Typed Lambda Calculus in Haskell
Created
2013-06-08
26 commits to master branch, last one 4 years ago
RowScript programming language, making a better browser world
Created
2021-07-24
944 commits to main branch, last one 12 days ago
A Haskell framework to define valid deep learning models and export them to other frameworks like TensorFlow JS or Keras.
Created
2018-10-08
118 commits to master branch, last one 3 years ago
Jupyter kernel for Coq
Created
2018-12-26
155 commits to master branch, last one 11 months ago
Normalization by evaluation for Martin-Löf Type Theory with dependent records
Created
2018-11-20
421 commits to master branch, last one 2 years ago
Cicada Language (PLCT little team)
Created
2022-08-07
1,874 commits to master branch, last one 5 days ago
First-class type families
Created
2018-07-09
167 commits to master branch, last one 4 months ago