dependent-types

Here are 225 public repositories matching this 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.

dependent-types coq theorem-proving proof-assistant

Updated Oct 22, 2022
OCaml

Kindelia / Kind2

Star

A next-gen functional language

dependent-types functional-programming lambda-calculus type-theory hacktoberfest theorem-prover formality moonad proof-language proof-languages

Updated Oct 21, 2022
Rust

FStarLang / FStar

Star

A Proof-oriented Programming Language

programming-language dependent-types ocaml theorem-proving verification f-sharp proof-assistant smt c-language fstar

Updated Oct 22, 2022
F*

leanprover / lean

Star

Lean Theorem Prover

programming-language dependent-types theorem-proving verification type-theory lean

Updated Aug 6, 2020
C++

agda / agda

Star

Agda is a dependently typed programming language / interactive theorem prover.

programming-language dependent-types proof-assistant type-theory agda

Updated Oct 22, 2022
Haskell

idris-lang / Idris2

Star

A purely functional programming language with first class types

dependent-types compiler hacktoberfest

Updated Oct 22, 2022
Idris

magmide / magmide

Star

A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.

dependent-types coq logic verification formal-methods type-safety formal-verification systems-programming

Updated Sep 4, 2022
Coq

pikelet-lang / pikelet

Star

A friendly little systems language with first-class types. Very WIP! 🚧

🚧

programming-language rust typechecker dependent-types compiler type-theory systems-language type-system systems-programming bidirectional-typechecking dependent-record-types dependent-records

Updated May 16, 2021
Rust

eashanhatti / peridot

Star

A fast functional language based on two level type theory

programming-language haskell dependent-types type-theory systems-language proglangs-discord

Updated Oct 9, 2022
Haskell

DimaSamoz / mezzo

Star

A Haskell library for typesafe music composition

haskell dependent-types midi music-composition haskell-library music-notation type-level-programming

Updated Mar 3, 2019
Haskell

cedille / cedille

Star

Cedille, a dependently typed programming languages based on the Calculus of Dependent Lambda Eliminations

programming-language dependent-types lambda-calculus dependent-intersections

Updated Feb 20, 2022
Agda

silt-lang / silt

Star

An in-progress fast, dependently typed, functional programming language implemented in Swift.

swift dependent-types compiler functional-programming

Updated Jul 2, 2019
Swift

HackerFoo / poprc

Sponsor

Star

A Compiler for the Popr Language

language dependent-types functional compiler concatenative verilog logic-programming non-deterministic partial-evaluators supercompiler linear-logic popr popr-compiler high-level-synthesis

Updated Jan 7, 2021
C

yeslogic / fathom

Star

🚧 (Alpha stage software) A declarative data definition language for formally specifying binary data formats. 🚧

language rust parser dependent-types compiler binary-data dsl declarative data-description-language type-system statically-typed type-checker binary-format dependent-record-types

Updated Oct 20, 2022
Rust

Deducteam / lambdapi

Star

Proof assistant based on the λΠ-calculus modulo rewriting

dependent-types proof-assistant rewriting proof-checker logical-framework

Updated Oct 20, 2022
OCaml

martinescardo / HoTT-UF-Agda-Lecture-Notes

Star

Lecture notes on univalent foundations of mathematics with Agda

dependent-types type-theory agda lecture-notes mltt homotopy-type-theory univalent-foundations univalent-mathematics hott-uf martin-lof-type-theory univalence-axiom function-extensionality propositional-truncation univalent-type-theory

Updated Sep 20, 2022
Agda

mattam82 / Coq-Equations

Star

A function definition package for Coq

programming-language dependent-types coq

Updated Oct 21, 2022
Coq

lukaszcz / coqhammer

Star

CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory

automation dependent-types coq verification hammer theorem-prover proof-search

Updated Sep 22, 2022
OCaml

ditto / ditto

Star

A Super Kawaii Dependently Typed Programming Language

programming-language dependent-types proof-assistant type-theory

Updated Jul 12, 2018
Haskell

Beluga-lang / Beluga

Star

Contextual types meet mechanized metatheory!

dependent-types ocaml lf beluga hoas

Updated Jul 28, 2022
OCaml

Improve this page

Add a description, image, and links to the dependent-types topic page so that developers can more easily learn about it.

Curate this topic

Add this topic to your repo

To associate your repository with the dependent-types topic, visit your repo's landing page and select "manage topics."

Learn more