37 results found Sort:
- Filter by Primary Language:
- OCaml (6)
- Rust (5)
- Haskell (4)
- Coq (4)
- Agda (3)
- TypeScript (3)
- C++ (2)
- Idris (2)
- Python (1)
- C (1)
- Scala (1)
- Swift (1)
- F* (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
43,106 commits to master branch, last one 13 hours ago
A next-gen functional language
Created
2018-07-13
619 commits to master branch, last one 15 days ago
A Proof-oriented Programming Language
Created
2014-04-03
36,750 commits to master branch, last one 3 days ago
A purely functional programming language with first class types
Created
2020-05-17
3,663 commits to main branch, last one 21 hours ago
Agda is a dependently typed programming language / interactive theorem prover.
Created
2015-08-08
22,532 commits to master branch, last one 2 days ago
Lean Theorem Prover
This repository has been archived
(exclude archived)
Created
2013-07-17
13,725 commits to master branch, last one 7 months 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 2 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 2 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
251 commits to main branch, last one a day ago
Proof assistant based on the λΠ-calculus modulo rewriting
Created
2017-09-10
3,787 commits to master branch, last one 14 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 proof assistant
Created
2020-11-09
4,234 commits to main branch, last one a day 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,819 commits to main branch, last one 3 days ago
Lecture notes on univalent foundations of mathematics with Agda
Created
2019-03-20
1,048 commits to master branch, last one about a month ago
CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory
Created
2018-01-31
591 commits to coq8.19 branch, last one about a month ago
Contextual types meet mechanized metatheory!
Created
2015-05-14
5,063 commits to master branch, last one 24 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 2 years ago
A garden of small programming language implementations 🪴
Created
2022-09-10
718 commits to main branch, last one about a month ago
Cicada Language (solo version)
Created
2021-03-28
6,370 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
Dependently Typed Lambda Calculus in Haskell
Created
2013-06-08
26 commits to master branch, last one 3 years 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
Large Scale Type Systems (programming language)
Created
2021-09-10
1,376 commits to main branch, last one 2 months ago
Cicada Language (PLCT little team)
Created
2022-08-07
1,864 commits to master branch, last one 14 days ago
Normalization by evaluation for Martin-Löf Type Theory with dependent records
Created
2018-11-20
421 commits to master branch, last one about a year ago
Jupyter kernel for Coq
Created
2018-12-26
155 commits to master branch, last one 4 months ago
First-class type families
Created
2018-07-09
166 commits to master branch, last one about a month ago
A pedagogic implementation of abstract bidirectional elaboration for dependent type theory.
Created
2020-10-15
101 commits to main branch, last one 2 years ago