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.
A purely functional programming language with first class types
Agda is a dependently typed programming language / interactive theorem prover.
A Proof-oriented Programming Language
Lean Theorem Prover
A modern proof language
A function definition package for Coq
Proof assistant based on the λΠ-calculus modulo rewriting
CoqHammer: An Automated Reasoning Hammer Tool for Rocq - Proof Automation for Dependent Type Theory
A friendly little systems language with first-class types. Very WIP! 🚧 🚧 🚧
Cedille, a dependently typed programming languages based on the Calculus of Dependent Lambda Eliminations
A proof assistant and a dependently-typed language
Lecture notes on univalent foundations of mathematics with Agda
Dependently Typed Lambda Calculus in Haskell
Contextual types meet mechanized metatheory!
Lecture notes for a short course on proving/programming in Coq via SSReflect.
MimIR is my Intermediate Representation
A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
A menagerie of cute implementations of modern typechecking algorithms
Add a description, image, and links to the dependent-types topic page so that developers can more easily learn about it.
To associate your repository with the dependent-types topic, visit your repo's landing page and select "manage topics."