A minimal development of SSA theory

A project to map out the relations between different equational theories of Magmas.

Functional choreographic programming in Haskell

Repository for formalization of the Polynomial Freiman Ruzsa conjecture (and related results)

🦠 Reusable components based on algebraic effects

antifunext

Ongoing Lean formalisation of the proof of Fermat's Last Theorem

Algebraic effects in the Bluefin effect system

Unlock your displays on your Mac! Flexible HiDPI scaling, XDR/HDR extra brightness, virtual screens, DDC control, extra dimming, PIP/streaming, EDID override and lots more!

Examples showing best practices for using Coq notations and custom entries [maintainer=@bcpierce00]

Malfunctional Programming

Slides and handwritten notes on the course on models of programming languages

Graph Theory [maintainers=@chdoc,@damien-pous]

DOOM on the reMarkable

An interactive theorem prover for string diagrams

The MLton repository

Cooperative-threaded access to relational data

A library of mechanised undecidability proofs in the Coq proof assistant.

Learning FPGA, yosys, nextpnr, and RISC-V

Denotational Semantics of the Untyped Lambda Calculus

Total Parser Combinators in Coq [maintainer=@womeier]

Finite probability theory in Coq

Envision a future where every student can read all the code of a teaching operating system.

egg is a flexible, high-performance e-graph library

A deterministic parser with fused lexing

A formalisation of the Calculus of Constructions

Streaming client for OCaml's Memprof

Interactive memory profiler based on Memtrace

A more maintainable, easier to share version of the infamous http://mindprod.com/jgloss/unmain.html