Parsing, analyzing, and comparing source code across many languages

A Dependently Typed Functional Programming Language

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

💥💻💥 A data-parallel functional programming language

Lenses, Folds, and Traversals - Join us on web.libera.chat #haskell-lens

Haskell to VHDL/Verilog/SystemVerilog compiler

Liquid Types For Haskell

Crucible is a library for symbolic simulation of imperative programs

A full stack, reactive architecture for general purpose programming. Algebraic and monadically composable primitives for concurrency, parallelism, event handling, transactions, multithreading, Web,…

Experimental implementation of Cubical Type Theory

Compiling to Categories

Networks of composable stream transducers

Parser combinators with highlighting, slicing, layout, literate comments, Clang-style diagnostics and the kitchen sink

Fake dependent types in Haskell using singletons

Open source binary analysis tools.

Developer tools for Haskell

A friendly effect system for Haskell

Heterogeneous automatic differentiation ("backpropagation") in Haskell

A small implementation of higher-order unification

Symbolic formula representation and solver interaction library

higher order dependently typed logic programing

Extensible Effects: An Alternative to Monad Transformers

Generic Programming using True Sums of Products

yacctt: Yet Another Cartesian Cubical Type Theory

Refinement Types for Scripting Languages

Library of categories, with categorical constructions on them

A language-generic implementation of equality saturation in Haskell

Provides Data.Void, which is in base since ghc 7.8 or so

A type theory based theorem proving library