Programming Language Theory λΠ

• UpdatedDec 2, 2024
• CSS

A modern proof language

• UpdatedJan 22, 2025
• Haskell

Building a modern functional compiler from first principles. (http://dev.stephendiehl.com/fun/)

• UpdatedJan 11, 2021
• Haskell

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

• UpdatedDec 17, 2025
• Haskell

Lean Theorem Prover

• UpdatedOct 14, 2023
• C++

A Coq library for Homotopy Type Theory

• UpdatedNov 29, 2025
• Rocq Prover

A friendly little systems language with first-class types. Very WIP! 🚧 🚧 🚧

• UpdatedMay 16, 2021
• Rust

Experimental implementation of Cubical Type Theory

• UpdatedSep 21, 2023
• Haskell

Playing Sudoku in TypeScript while the type checker highlights mistakes.

• UpdatedAug 20, 2024
• TypeScript

Research on integrating datalog & lambda calculus via monotonicity types

• UpdatedJun 21, 2022
• TeX

A fast functional language based on two level type theory

• UpdatedJan 6, 2023
• Haskell

Programming language agnostic type construction language based on polynomials.

• UpdatedMay 29, 2024
• Idris

A menagerie of cute implementations of modern typechecking algorithms

• UpdatedDec 10, 2025
• Rust

My personal repository of formally verified mathematics.

• UpdatedDec 16, 2025
• Rocq Prover

A garden of small programming language implementations 🪴

• UpdatedDec 17, 2025
• OCaml

Logical manifestations of topological concepts, and other things, via the univalent point of view.

• UpdatedDec 14, 2025
• Agda

Research on theory of programming languages λ, compilers, interpreters, functional programming, formal methods, logic etc.

• UpdatedAug 30, 2024

😎TT

• UpdatedNov 20, 2025
• OCaml

Lecture notes on univalent foundations of mathematics with Agda

• UpdatedNov 17, 2025
• Agda

The People's Refinement Logic

• UpdatedJan 1, 2023
• Standard ML