- Mountain View, California, Earth
- http://blog.strake.me.uk/
Starred repositories
minimalist pure lazy functional programming language (pythonic haskell)
An interactive tour of type inference algorithms, powered by `ghc-wasm-meta`.
Automatically deriving control-flow graph generators from operational semantics
A fully-modern text-based browser, rendering to TTY and browsers
Answering the question nobody asked: what if you wanted to text your friends using only ARP?
Linux Status and Configuration application for Mini-Box.com Open UPS, Open UPS 2 and NUC UPS
This is a 3d-printable supporting frame for three perpendicular electromagnetic coils as a handheld probe.
A list of Free Software network services and web applications which can be hosted on your own servers
✨ A repository of all the spells from D&D that could possibly be tweaked and twanged. Stored in markdown.
A syntax for unions of constraints in Haskell
Replib: generic programming & Unbound: generic treatment of binders
What if we built the same frustrating type checker over and over again? For science.
A universe of scope- and type-safe syntaxes (syntices?). Includes generic implementation of type-preserving renaming/substitution with all the proofs you could possibly need.
Accessing Agda's interaction mode via command line & external tactic for Agda.
wherein I implement several substructural logics in Agda
Agda formalisation of the Introduction to Homotopy Type Theory
A slow-paced introduction to reflection in Agda. ---Tactics!
The theory of algebraic graphs formalised in Agda
A Scope-and-Type Safe Universe of Syntaxes with Binding, Their Semantics and Proofs
PhD research ;; What's the difference between a typeclass/trait and a record/class/struct? Nothing really, or so I argue.