agda/agda

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

Language: Haskell - Size: 148 MB - Last synced at: 2 days ago - Pushed at: 2 days ago - Stars: 2,654 - Forks: 376

FStarLang/FStar

A Proof-oriented Programming Language

Language: F* - Size: 752 MB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 2,854 - Forks: 239

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.

Language: OCaml - Size: 196 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 5,127 - Forks: 685

Deducteam/lambdapi

Proof assistant based on the λΠ-calculus modulo rewriting

Language: OCaml - Size: 38.9 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 335 - Forks: 37

idris-lang/Idris2

A purely functional programming language with first class types

Language: Idris - Size: 115 MB - Last synced at: 6 days ago - Pushed at: 6 days ago - Stars: 2,670 - Forks: 385

HigherOrderCO/Kind

A modern proof language

Language: Haskell - Size: 34.6 MB - Last synced at: 5 days ago - Pushed at: 5 months ago - Stars: 3,676 - Forks: 146

chasenorman/Canonical

Canonical is a performant sound and complete type inhabitation solver for dependent type theory.

Language: Lean - Size: 159 KB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 51 - Forks: 4

leanprover/lean3 📦

Lean Theorem Prover

Language: C++ - Size: 50.3 MB - Last synced at: 3 days ago - Pushed at: over 1 year ago - Stars: 2,152 - Forks: 218

chester-lang/chester

Trying to make a practical possibly unsound dependently typed language with algebraic effects

Language: Scala - Size: 58.5 MB - Last synced at: 6 days ago - Pushed at: 6 days ago - Stars: 7 - Forks: 1

brendanzab/language-garden

A garden of small programming language implementations 🪴

Language: OCaml - Size: 1.99 MB - Last synced at: 7 days ago - Pushed at: 7 days ago - Stars: 247 - Forks: 6

DimaSamoz/mezzo

A Haskell library for typesafe music composition

Language: Haskell - Size: 1.2 MB - Last synced at: 9 days ago - Pushed at: over 6 years ago - Stars: 363 - Forks: 12

dunhamsteve/newt

A toy dependent typed language.

Language: Agda - Size: 1.86 MB - Last synced at: 12 days ago - Pushed at: 13 days ago - Stars: 29 - Forks: 0

chasenorman/CanonicalLean

A Lean tactic for Canonical, a search procedure for terms in dependent type theory.

Language: Lean - Size: 8.79 MB - Last synced at: 13 days ago - Pushed at: 14 days ago - Stars: 69 - Forks: 4

tgrospic/typed-grid-rs

Compile time grid navigation

Language: Rust - Size: 74.2 KB - Last synced at: 14 days ago - Pushed at: 15 days ago - Stars: 0 - Forks: 1

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.

Size: 315 KB - Last synced at: 16 days ago - Pushed at: 16 days ago - Stars: 342 - Forks: 11

gfngfn/lw-staged-deptype

Language: Haskell - Size: 663 KB - Last synced at: 16 days ago - Pushed at: 17 days ago - Stars: 3 - Forks: 0

groupoid/anders

🧊 Модальний гомотопічний верифікатор математики

Language: OCaml - Size: 14.8 MB - Last synced at: 4 days ago - Pushed at: 17 days ago - Stars: 22 - Forks: 2

Lambda-Mountain-Compiler-Backend/LSTS

Large Scale Type Systems (programming language)

Size: 1.22 MB - Last synced at: 8 days ago - Pushed at: 20 days ago - Stars: 123 - Forks: 3

aya-prover/aya-dev

A proof assistant and a dependently-typed language

Language: Java - Size: 18.1 MB - Last synced at: 12 days ago - Pushed at: 12 days ago - Stars: 316 - Forks: 19

AnyDSL/MimIR

MimIR is my Intermediate Representation

Language: C++ - Size: 345 MB - Last synced at: 6 days ago - Pushed at: 6 days ago - Stars: 68 - Forks: 14

Coder-Spirit/nominal

Powerful nominal types for your Typescript project

Language: TypeScript - Size: 2.66 MB - Last synced at: 3 days ago - Pushed at: about 2 months ago - Stars: 85 - Forks: 1

rowscript/rowscript

RowScript programming language, making a better browser world

Language: JavaScript - Size: 1.87 MB - Last synced at: 16 days ago - Pushed at: 27 days ago - Stars: 121 - Forks: 1

Beluga-lang/Beluga

Contextual types meet mechanized metatheory!

Language: OCaml - Size: 18.8 MB - Last synced at: 28 days ago - Pushed at: 28 days ago - Stars: 189 - Forks: 16

joelberkeley/spidr

Accelerated machine learning with dependent types

Language: Idris - Size: 1.51 MB - Last synced at: 19 days ago - Pushed at: 19 days ago - Stars: 95 - Forks: 5

konn/ghc-typelits-presburger

Presburger arithmetic solver for built-in type-level naturals

Language: Haskell - Size: 1.27 MB - Last synced at: 12 days ago - Pushed at: 6 months ago - Stars: 9 - Forks: 6

yiyunliu/mltt-consistency

Logical relation for predicative CC omega with booleans and an intensional identity type

Language: TeX - Size: 8 MB - Last synced at: 5 days ago - Pushed at: about 2 months ago - Stars: 13 - Forks: 3

andreasabel/helf

Haskell implementation of the Edinburgh Logical Framework

Language: Haskell - Size: 3.32 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 27 - Forks: 3

mattam82/Coq-Equations

A function definition package for Coq

Language: Coq - Size: 59 MB - Last synced at: 24 days ago - Pushed at: about 1 month ago - Stars: 230 - Forks: 48

owo-lang/minitt-rs

Dependently-typed lambda calculus, Mini-TT, extended and implemented in Rust

Language: Rust - Size: 336 KB - Last synced at: 24 days ago - Pushed at: over 4 years ago - Stars: 119 - Forks: 4

ionathanch/TTBFL

A logical relations model of a minimal type theory with bounded first-class universe levels mechanized in Lean.

Language: TeX - Size: 1.3 MB - Last synced at: 5 days ago - Pushed at: about 2 months ago - Stars: 19 - Forks: 1

ilyasergey/pnp

Lecture notes for a short course on proving/programming in Coq via SSReflect.

Language: Coq - Size: 6.47 MB - Last synced at: about 2 months ago - Pushed at: almost 4 years ago - Stars: 164 - Forks: 19

pikelet-lang/pikelet

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

Language: Rust - Size: 5.56 MB - Last synced at: about 2 months ago - Pushed at: about 4 years ago - Stars: 617 - Forks: 26

thamugadi/semantic-preservation

Attempt to prove semantic preservation (forward simulation) for a simple compiler.

Language: Coq - Size: 106 KB - Last synced at: 7 days ago - Pushed at: about 1 year ago - Stars: 11 - Forks: 0

sourcedennis/rust-pi-forall

A partial re-implementation of pi-forall in Rust

Language: Rust - Size: 77.1 KB - Last synced at: 5 days ago - Pushed at: over 2 years ago - Stars: 3 - Forks: 0

Lysxia/first-class-families

First-class type families

Language: Haskell - Size: 134 KB - Last synced at: 28 days ago - Pushed at: about 2 months ago - Stars: 87 - Forks: 13

martinescardo/HoTT-UF-Agda-Lecture-Notes

Lecture notes on univalent foundations of mathematics with Agda

Language: Agda - Size: 5.8 MB - Last synced at: about 2 months ago - Pushed at: about 1 year ago - Stars: 227 - Forks: 20

saki-lang/saki-dev

A simple scala-like dependent type programming language

Language: Scala - Size: 605 KB - Last synced at: about 2 months ago - Pushed at: 2 months ago - Stars: 17 - Forks: 2

bor0/gidti

Book: Introduction to Dependent Types with Idris

Size: 10.9 MB - Last synced at: about 1 month ago - Pushed at: over 2 years ago - Stars: 78 - Forks: 4

lukaszcz/coqhammer

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

Language: OCaml - Size: 2.49 MB - Last synced at: 24 days ago - Pushed at: 2 months ago - Stars: 228 - Forks: 32

SphericalPotatoInVacuum/DependoBuf

DependoBuf - a data serialization format with dependent types

Language: C++ - Size: 1.82 MB - Last synced at: about 2 months ago - Pushed at: 7 months ago - Stars: 16 - Forks: 1

magmide/magmide

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

Language: Coq - Size: 38.5 MB - Last synced at: 24 days ago - Pushed at: about 1 year ago - Stars: 823 - Forks: 13

EugeneLoy/coq_jupyter

Jupyter kernel for Coq

Language: Python - Size: 414 KB - Last synced at: about 1 month ago - Pushed at: 10 months ago - Stars: 95 - Forks: 8

chameco/bramble

dependently-typed lisp with flexible compiler backends

Language: Haskell - Size: 73.2 KB - Last synced at: 10 days ago - Pushed at: about 6 years ago - Stars: 27 - Forks: 1

kevinclancy/SchemaTypes

Dependently typed schema language for MUMPS

Language: F# - Size: 2.91 MB - Last synced at: 8 days ago - Pushed at: 3 months ago - Stars: 1 - Forks: 0

yeslogic/fathom

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

Language: Rust - Size: 5.51 MB - Last synced at: 23 days ago - Pushed at: almost 2 years ago - Stars: 263 - Forks: 12

ilya-klyuchnikov/lambdapi

Dependently Typed Lambda Calculus in Haskell

Language: Haskell - Size: 66.4 KB - Last synced at: 2 months ago - Pushed at: over 4 years ago - Stars: 115 - Forks: 21

jespercockx/agda-core

A work-in-progress core language for Agda, in Agda

Language: Agda - Size: 465 KB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 48 - Forks: 3

uwplse/pumpkin-pi

An extension to PUMPKIN PATCH with support for proof repair across type equivalences.

Language: Coq - Size: 3.44 MB - Last synced at: 6 days ago - Pushed at: 2 months ago - Stars: 49 - Forks: 9

liesnikov/extensible-elaborator

prototype implementation of a dependently-typed language with an extendable constraints and accompanying materials

Language: TeX - Size: 34.9 MB - Last synced at: 2 months ago - Pushed at: about 1 year ago - Stars: 7 - Forks: 1

jackfoxy/DependentTypes

experiments with @robkuz LimitedValue type

Language: F# - Size: 734 KB - Last synced at: about 1 month ago - Pushed at: over 5 years ago - Stars: 71 - Forks: 3

jfdm/velo-lang

Velo is a tiny language (STLC + Hutton's Razor with Bools) to showcase & explore efficient verified implementations in Idris2.

Language: Idris - Size: 1.08 MB - Last synced at: 3 months ago - Pushed at: about 2 years ago - Stars: 16 - Forks: 2

rzrn/anders

Anders: Cubical Type Checker

Language: OCaml - Size: 4.02 MB - Last synced at: 26 days ago - Pushed at: over 1 year ago - Stars: 24 - Forks: 1

qexat/inductive

inductive is a Python library that defines inductive data structures such as Peano numbers and linked lists.

Language: Python - Size: 242 KB - Last synced at: 6 days ago - Pushed at: 3 months ago - Stars: 7 - Forks: 0

owo-lang/voile-rs

Dependently-typed row-polymorphic programming language, evolved from minitt-rs

Language: Rust - Size: 818 KB - Last synced at: about 1 month ago - Pushed at: over 4 years ago - Stars: 97 - Forks: 5

cedille/cedille

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

Language: Agda - Size: 19.3 MB - Last synced at: 3 months ago - Pushed at: over 1 year ago - Stars: 374 - Forks: 27

ualib/agda-algebras

The Agda Universal Algebra Library (html docs available at the url below)

Language: Agda - Size: 65 MB - Last synced at: 2 months ago - Pushed at: 7 months ago - Stars: 33 - Forks: 7

konn/sized

Sized sequence data-types

Language: Haskell - Size: 614 KB - Last synced at: 2 months ago - Pushed at: 4 months ago - Stars: 11 - Forks: 1

propensive/cardinality

Dependently-typed range-checked numbers for Scala

Language: Scala - Size: 2.02 MB - Last synced at: 7 days ago - Pushed at: 4 months ago - Stars: 2 - Forks: 0

ggzor/specifying-verifying-tail-recursion

Source code for the paper "Specifying and Verifying a Transformation of Recursive Functions into Tail-Recursive Functions"

Language: TeX - Size: 2.5 MB - Last synced at: 6 days ago - Pushed at: over 2 years ago - Stars: 1 - Forks: 1

01mf02/kontroli-hs

Alternative implementation of the logical framework Dedukti

Language: Haskell - Size: 23.4 KB - Last synced at: 16 days ago - Pushed at: over 5 years ago - Stars: 1 - Forks: 0

tensor-fusion/Coquand-SML

A bidirectional dependent type checker in Standard ML

Language: Standard ML - Size: 9.77 KB - Last synced at: 4 months ago - Pushed at: 11 months ago - Stars: 1 - Forks: 0

brendanzab/agda-logic-playground

Messing around with propositional logic in Agda

Language: Agda - Size: 1.95 KB - Last synced at: about 14 hours ago - Pushed at: over 8 years ago - Stars: 1 - Forks: 0

mtumilowicz/scala3-dependent-types-polymorphic-functions-workshop

Introduction to typelevel programming: phantom types, dependent types, path dependent types and Curry-Howard isomorphism.

Language: Scala - Size: 324 KB - Last synced at: 4 months ago - Pushed at: 5 months ago - Stars: 1 - Forks: 0

vendethiel/dependent-printf

I'm terrible at this, eh.

Language: Agda - Size: 109 KB - Last synced at: 3 months ago - Pushed at: almost 11 years ago - Stars: 1 - Forks: 0

d-plaindoux/scalpel

Scalpel is a parser combinator library using path depend type capability

Language: Scala - Size: 63.5 KB - Last synced at: 3 months ago - Pushed at: 5 months ago - Stars: 1 - Forks: 0

yurrriq/cedille-playground

:notebook: Maybe someday useful and organized notes about Cedille.

Size: 8.79 KB - Last synced at: 3 months ago - Pushed at: over 6 years ago - Stars: 2 - Forks: 0

andreasabel/red-black-tree-left-leaning

Left-leaning red-black trees in Agda (insertion and deletion) with static ordering and balancing invariants

Language: Agda - Size: 151 KB - Last synced at: 16 days ago - Pushed at: 4 months ago - Stars: 2 - Forks: 0

Kamirus/coq-course

Coq course materials with my solutions

Language: Coq - Size: 1.31 MB - Last synced at: 2 months ago - Pushed at: about 5 years ago - Stars: 2 - Forks: 0

sudonatalie/thesis

My now-completed Master's thesis.

Language: TeX - Size: 5.39 MB - Last synced at: 2 months ago - Pushed at: over 6 years ago - Stars: 2 - Forks: 0

taktoa/inference

Experiments in dependent type inference

Language: Haskell - Size: 57.6 KB - Last synced at: 3 months ago - Pushed at: about 8 years ago - Stars: 3 - Forks: 1

propensive/typonym

Collections raised to the type-level in Scala

Language: Scala - Size: 646 KB - Last synced at: 7 days ago - Pushed at: 5 months ago - Stars: 3 - Forks: 0

CrowdHailer/eyg

Explicit concurrency for intelligible parallel programing.

Language: Rust - Size: 73.2 KB - Last synced at: about 1 month ago - Pushed at: about 5 years ago - Stars: 3 - Forks: 0

leostera/libra

:balance_scale: A Lisp Parser in Idris

Language: Idris - Size: 438 KB - Last synced at: 2 months ago - Pushed at: about 8 years ago - Stars: 3 - Forks: 0

sigma-andex/scala-fast-vect

Fast 🐆, type-safe vectors for Scala

Language: Scala - Size: 12.7 KB - Last synced at: 3 months ago - Pushed at: over 2 years ago - Stars: 4 - Forks: 0

DmytroMitin/arend-exercises

Size: 3.91 KB - Last synced at: 4 months ago - Pushed at: over 6 years ago - Stars: 4 - Forks: 0

gspia/fcf-containers

fcf-containers add tools that can be used with first-class-families

Language: Haskell - Size: 209 KB - Last synced at: about 1 month ago - Pushed at: about 2 years ago - Stars: 5 - Forks: 2

bracevac/dotter

Towards richer dependent types for DOT

Language: Coq - Size: 365 KB - Last synced at: 2 months ago - Pushed at: over 4 years ago - Stars: 5 - Forks: 0

dannywillems/master-thesis

My master thesis on RML : In French.

Language: TeX - Size: 7.1 MB - Last synced at: 2 months ago - Pushed at: almost 3 years ago - Stars: 5 - Forks: 0

wilbowma/cur-control

An implementation of control operators for Cur.

Language: Racket - Size: 15.6 KB - Last synced at: 4 months ago - Pushed at: almost 8 years ago - Stars: 7 - Forks: 1

DanilaFe/maypop

Dependently typed programming language implemented in Literate Haskell.

Language: Haskell - Size: 774 KB - Last synced at: 2 months ago - Pushed at: almost 4 years ago - Stars: 7 - Forks: 0

tofu-tf/cherry

Universal Data design and transform language core

Language: Scala - Size: 104 KB - Last synced at: 2 months ago - Pushed at: 7 months ago - Stars: 8 - Forks: 4

chameco/reliquary

Concatenative dependently-typed functional programming language

Language: Haskell - Size: 73.2 KB - Last synced at: 10 days ago - Pushed at: about 8 years ago - Stars: 9 - Forks: 0

oisdk/type-indexed-queues

Queues with verified and unverified versions

Language: Haskell - Size: 17.9 MB - Last synced at: 15 days ago - Pushed at: about 8 years ago - Stars: 9 - Forks: 0

timjb/idris-pfds

Purely functional data structures in Idris

Language: Idris - Size: 37.1 KB - Last synced at: 3 months ago - Pushed at: over 7 years ago - Stars: 10 - Forks: 1

simongregersen/DepSec

A library for static information-flow control in Idris

Language: Idris - Size: 18.6 KB - Last synced at: 3 months ago - Pushed at: over 6 years ago - Stars: 10 - Forks: 0

steshaw/lennart-lambda-cube

Lennart Augustsson's lamda cube

Language: Haskell - Size: 20.5 KB - Last synced at: about 1 month ago - Pushed at: almost 9 years ago - Stars: 12 - Forks: 3

gallais/idris-tmustache

Total Logic-Less Templating Library

Language: Idris - Size: 56.6 KB - Last synced at: 3 months ago - Pushed at: over 7 years ago - Stars: 13 - Forks: 1

appliedfm/vstyle

A style guide for Coq

Size: 646 KB - Last synced at: 2 months ago - Pushed at: over 3 years ago - Stars: 18 - Forks: 0

ziman/ttstar

Dependently typed core calculus with erasure

Language: Idris - Size: 3.25 MB - Last synced at: 3 months ago - Pushed at: almost 4 years ago - Stars: 19 - Forks: 0

jonsterling/coq-guarded-computational-type-theory

Language: Coq - Size: 421 KB - Last synced at: about 1 month ago - Pushed at: about 7 years ago - Stars: 21 - Forks: 1

jaredloomis/Idris-HoTT

Homotopy Type Theory proofs in Idris

Language: Idris - Size: 3.91 KB - Last synced at: 3 months ago - Pushed at: about 6 years ago - Stars: 22 - Forks: 1

DmytroMitin/AUXify

Introduces macro/meta annotations @ aux, @ self, @ instance, @ apply, @ delegated, @ syntax and String-based type class LabelledGeneric

Language: Scala - Size: 13.9 MB - Last synced at: 2 months ago - Pushed at: almost 5 years ago - Stars: 29 - Forks: 3

ThoughtWorksInc/feature.scala

Access Scala language features on the type-level

Language: Scala - Size: 501 KB - Last synced at: about 2 months ago - Pushed at: 10 months ago - Stars: 31 - Forks: 3

konn/type-natural

Type-level well-kinded natural numbers.

Language: Haskell - Size: 555 KB - Last synced at: 22 days ago - Pushed at: 6 months ago - Stars: 34 - Forks: 12

jonascarpay/convoluted

Dependently typed convolutional neural networks

Language: Haskell - Size: 98.6 KB - Last synced at: 2 months ago - Pushed at: about 8 years ago - Stars: 35 - Forks: 1

gallettilance/magnificATS

Collection of ATS goodness

Language: ATS - Size: 20.2 MB - Last synced at: 4 months ago - Pushed at: over 5 years ago - Stars: 35 - Forks: 2

sir-wabbit/leibniz

Leibniz equivalence and Liskov substitutability library for Scala.

Language: Scala - Size: 190 KB - Last synced at: 25 days ago - Pushed at: about 3 years ago - Stars: 37 - Forks: 4

doofin/differentiable-idris

dependent types meets deep learning

Language: Idris - Size: 51.8 KB - Last synced at: 5 days ago - Pushed at: over 6 years ago - Stars: 43 - Forks: 7

WhatisRT/meta-cedille

Minimalistic dependent type theory with syntactic metaprogramming

Language: Agda - Size: 945 KB - Last synced at: 8 days ago - Pushed at: 12 months ago - Stars: 57 - Forks: 0

scott-fleischman/agda-from-nothing

A workshop on learning Agda with minimal prerequisites.

Language: Agda - Size: 422 KB - Last synced at: 2 months ago - Pushed at: about 9 years ago - Stars: 85 - Forks: 6