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.

• UpdatedJul 18, 2025
• Haskell

Lean Theorem Prover

• UpdatedOct 14, 2023
• C++

A Coq library for Homotopy Type Theory

• UpdatedJul 15, 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

My personal repository of formally verified mathematics.

• UpdatedJul 15, 2025
• Rocq Prover

A garden of small programming language implementations 🪴

• UpdatedJul 18, 2025
• OCaml

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

• UpdatedJul 17, 2025
• Agda

😎TT

• UpdatedOct 21, 2023
• OCaml

The People's Refinement Logic

• UpdatedJan 1, 2023
• Standard ML

Lecture notes on univalent foundations of mathematics with Agda

• UpdatedApr 16, 2024
• Agda

"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory

• UpdatedMar 25, 2022
• OCaml

Exercises from Benjamin Pierce's "Types and Programming Languages" textbook + extras!

• UpdatedJul 26, 2020
• Rust