Research language for array processing in the Haskell/ML family

A programming language in Turkish where grammatical case and mood are part of the type system.

Minimal implementations for dependent type checking and elaboration

A demo implementation of a simple dependently-typed language

Experimental implementation of Cubical Type Theory

A Haskell library for typesafe music composition

An experimental proof assistant based on a type theory for synthetic ∞-categories.

Grammatical Framework core: compiler, shell & runtimes

Implementation of Univalence in Cubical Sets

Effective Algebraic Topology in Haskell

A language based on homotopy type theory with an interval

yacctt: Yet Another Cartesian Cubical Type Theory

Mirror of Epigram 2, by Conor McBride, et al.

⭕️ N2O: Haskell Application Server

Deprecated

A non-interactive proof assistant using the Haskell type system

A small NuPRL style proof assistant

An intensely interactive, graphical theorem prover based on natural deduction

Haskell library of algebraic topology

A Whitespace-Based Dependently Typed Functional Programming Language

Haskell implementation of a version of cubical type theory developed for my master thesis

A dependently-typed language with indexed inductive types supported.

A network-compatable rewrite of the Ace of Spades 0.* clients in Haskell

A Haskell library to parse/serialize Executable and Linkable Format (ELF)

Simple LCF-style proof assistant for ZFC

A HM based type inference written in Haskell

Yet another typechecker for a dependently typed language.