Nix and Haskell in production

This coq library aims to formalize a substantial body of mathematics using the univalent point of view.

Smart calendar with EInk display and Raspberry Pi

A minimal proof language.

HoTT in Lean 3

Literate Haskell support for Markdown

A next-gen functional language

LaTeX code for a paper on lean's type theory

Langton's Ant in Haskell

Spacemacs layer for the Lean Theorem Prover.

Coq library on rewriting theory and termination

Ramsey Theory

A re-do of the SimpleFP repo using de Bruijn index ABTs instead of HOAS

Python-powered simple starter Slack bot.

Univalence from scratch in Idris

Literature review of GHC's Core language, System FC

A JSON API server written in Haskell

python app/framework for 'all things ISBN' including metadata, descriptions, covers...

SDL2 tutorial code in Haskell

The home of the Glamorous Glambda interpreter

Core repository for Sawtooth Distributed Ledger

Bitmap & tilemap generation from a single example with the help of ideas from quantum mechanics

An interpreter for Gödel's System T

Programming Languages Zoo

papers of Per Martin Löf

A collection of resources for learning type theory and type theory adjacent fields.

Simple Minecraft-inspired program using Python and Pyglet

A fork of "Minecraft in 500 lines of python" intended to someday be used as a real engine, instead of as a learning example.