dependent-types
There are 255 repositories under dependent-types topic.
coq/coq
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 development of machine-checked proofs.
HigherOrderCO/Kind1
A next-gen functional language
FStarLang/FStar
A Proof-oriented Programming Language
idris-lang/Idris2
A purely functional programming language with first class types
agda/agda
Agda is a dependently typed programming language / interactive theorem prover.
leanprover/lean3
Lean Theorem Prover
magmide/magmide
A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
pikelet-lang/pikelet
A friendly little systems language with first-class types. Very WIP! 🚧 🚧 🚧
eashanhatti/peridot
A fast functional language based on two level type theory
cedille/cedille
Cedille, a dependently typed programming languages based on the Calculus of Dependent Lambda Eliminations
DimaSamoz/mezzo
A Haskell library for typesafe music composition
newca12/awesome-rust-formalized-reasoning
An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification.
Deducteam/lambdapi
Proof assistant based on the λΠ-calculus modulo rewriting
yeslogic/fathom
🚧 (Alpha stage software) A declarative data definition language for formally specifying binary data formats. 🚧
aya-prover/aya-dev
A proof assistant
silt-lang/silt
An in-progress fast, dependently typed, functional programming language implemented in Swift.
HackerFoo/poprc
A Compiler for the Popr Language
martinescardo/HoTT-UF-Agda-Lecture-Notes
Lecture notes on univalent foundations of mathematics with Agda
mattam82/Coq-Equations
A function definition package for Coq
lukaszcz/coqhammer
CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory
Beluga-lang/Beluga
Contextual types meet mechanized metatheory!
ditto/ditto
A Super Kawaii Dependently Typed Programming Language
ilyasergey/pnp
Lecture notes for a short course on proving/programming in Coq via SSReflect.
brendanzab/language-garden
A garden of small programming language implementations 🪴
cicada-lang/cicada-solo
Cicada Language (solo version)
ilya-klyuchnikov/ttlite
A SuperCompiler for Martin-Löf's Type Theory
owo-lang/minitt-rs
Dependently-typed lambda calculus, Mini-TT, extended and implemented in Rust
ilya-klyuchnikov/lambdapi
Dependently Typed Lambda Calculus in Haskell
leopiney/tensor-safe
A Haskell framework to define valid deep learning models and export them to other frameworks like TensorFlow JS or Keras.
andrew-johnson-4/LSTS
Large Scale Type Systems (programming language)
owo-lang/voile-rs
Dependently-typed row-polymorphic programming language, evolved from minitt-rs
cicada-lang/cicada-plct
Cicada Language (PLCT little team)
brendanzab/rust-nbe-for-mltt
Normalization by evaluation for Martin-Löf Type Theory with dependent records
EugeneLoy/coq_jupyter
Jupyter kernel for Coq
Lysxia/first-class-families
First-class type families
scott-fleischman/agda-from-nothing
A workshop on learning Agda with minimal prerequisites.