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,367 commits to master branch, last one 22 hours ago
A modern proof language
Created
2018-07-13
274 commits to master branch, last one 5 days ago
A Proof-oriented Programming Language
Created
2014-04-03
37,870 commits to master branch, last one 16 hours ago
A purely functional programming language with first class types
Created
2020-05-17
3,767 commits to main branch, last one 13 days 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
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 7 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
270 commits to main branch, last one 5 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
🚧 (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,856 commits to main branch, last one 8 days ago
Lecture notes on univalent foundations of mathematics with Agda
Created
2019-03-20
1,048 commits to master branch, last one 7 months 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 5 days ago
Contextual types meet mechanized metatheory!
Created
2015-05-14
5,070 commits to master branch, last one 3 months ago
A garden of small programming language implementations 🪴
Created
2022-09-10
845 commits to main branch, last one 9 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,371 commits to master branch, last one 20 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,414 commits to main branch, last one 15 hours ago
Dependently Typed Lambda Calculus in Haskell
Created
2013-06-08
26 commits to master branch, last one 3 years ago
RowScript programming language, making a better browser world
Created
2021-07-24
939 commits to main branch, last one 5 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 10 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,873 commits to master branch, last one 20 days ago
First-class type families
Created
2018-07-09
167 commits to master branch, last one 3 months ago