A Dependently Typed Functional Programming Language

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

A fast, flexible, fused effect system for Haskell

Experimental implementation of Cubical Type Theory

Compiling to Categories

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

The home of the Glamorous Glambda interpreter

agda-mode for neovim

Play Minesweeper by formally proving your moves in Idris

an implementation of stuck macros

Demo for dependent types + runtime code generation

A wiki based on firm theoretical foundations

FRP library

A Haskell library for building incremental static site generators