effectfully

haskell-challenges. Code challenges to solve with Haskell

sketches. A Haskell blog

inference-in-agda. A tutorial on how Agda infers things

OTT. Observational Type Theory as an Agda library

Generic. A library for doing generic programming in Agda

STLC. Dependently typed Algorithm M and friends

Cubes. A dependently typed type checker for a TT with intervals

random-stuff. Agda

prefolds. Composable monadic short-circuiting streaming folds

Eff. Experiments with effect systems

Categories. Some basic category theory

leetcode-haskell. Haskell

proto-tt. Agda

tiny-lang. Haskell

Beauty-and-the-Beast. A toy supercompiler for STLC with numbers and lists

ECC. A shallow embedding of Luo's ECC into Agda.

blog. Agda

hoppy-cpp. Haskell

Ouroboros. Agda

Big-Step-Normalization. Agda

monad-var. Generic operations over variables

haskell-challenges. Code challenges to solve with Haskell

agda-html-to-md. A tiny tool that takes output of `htmlize` and turns it into a markdown text consumable by `pandoc`

Stub. Haskell

req-blowup. Haskell

prettyprinter-configurable. Haskell

DataData. Agda

haskell-ffi-example. Haskell

yandex-direct. Haskell