dependent-types
There are 279 repositories under dependent-types topic.
rocq-prover/rocq
The Rocq Prover is an interactive theorem prover, or proof assistant. 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/Kind
A modern proof 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! 🚧 🚧 🚧
ehatti/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
aya-prover/aya-dev
A proof assistant and a dependently-typed language
sdiehl/typechecker-zoo
A menagerie of cute implementations of modern typechecking algorithms
brendanzab/language-garden
A garden of small programming language implementations 🪴
yeslogic/fathom
🚧 (Alpha stage software) A declarative data definition language for formally specifying binary data formats. 🚧
HackerFoo/poprc
A Compiler for the Popr Language
silt-lang/silt
An in-progress fast, dependently typed, functional programming language implemented in Swift.
mattam82/Coq-Equations
A function definition package for Coq
martinescardo/HoTT-UF-Agda-Lecture-Notes
Lecture notes on univalent foundations of mathematics with Agda
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.
cicada-lang/cicada-solo
Cicada Language (solo version)
Lambda-Mountain-Compiler-Backend/LSTS
Large Scale Type Systems: ML/C Hybrid Programming Language
rowscript/rowscript
RowScript programming language, making a better browser world
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.
owo-lang/voile-rs
Dependently-typed row-polymorphic programming language, evolved from minitt-rs
brendanzab/rust-nbe-for-mltt
Normalization by evaluation for Martin-Löf Type Theory with dependent records
joelberkeley/spidr
Accelerated machine learning with dependent types
EugeneLoy/coq_jupyter
Jupyter kernel for Coq