Submission for TYPES'25

Prevent your Mac from "upgrading" to Tahoe. A community-led effort to safely block unwanted macOS upgrades.

A Haskell library for Approximating Exact Real Numbers (AERN) based on interval computation. (aern2 is a rewrite of aern.)

Lean formalization of selected lemmas from "Term Rewriting and All That"

A programming language in Turkish where grammatical case and mood are part of the type system.

A new extraction system from Rocq to functional-style, memory-safe, thread-safe, readable, valid, performant, and modern C++.

An agda library for developing synthetic category theory - and other synthetic mathematics

Supports generation of websites with highlighted literate Agda code

A wrapper for the public API to the eBird database.

Access and Analyze eBird Status and Trends Data

Advent of Code 2025 in TypeScript (with visualizations!)

Agda parser for VNNLIB

Competitive Programmer's Handbook

A DSL for the internal language of a topos

A Library for Representing Recursive and Impure Programs in Coq

Formalisations of interesting models of QTT

Verified Program Extraction in Number Theory

Adventures in being positively negative when deciding things in Idris.

BB(5) paper

Hagenberg LaTeX Thesis Template

A hardware description language based on operational semantics

An arbitrary-precision differentiable programming language.

A modified version of Marshall with nondeterminism, partiality, and pattern matching

Lean formalization of the "Generalized Algebra" used in my PhD thesis

Slides for my viva