- Gothenburg, Sweden
-
Interested in type theory, category theory and univalent foundations.
- Joined on Jan 22, 2022
the sources for my website
Updated 7 days ago
A “proof assistant” with holes and implicit arguments. Being developed to learn about elaboration, meta variables and OCaml.
Updated 1 week ago
A hindley-milner typechecker with inductive types.
Updated 1 week ago
Updated 3 weeks ago
A literate formalization of categories with families in cubical agda.
Updated 3 months ago
A typechecker for intensional MLTT without elaboration.
Updated 4 months ago
A vm designed to run functional languages. Unfinished and (currently) abandoned.
Updated 4 months ago
An application for viewing album art of the song currently playing in mpd
Updated 4 months ago
A web front-end for youtube-dl
Updated 4 months ago
A tui client for browsing yts.mx
Updated 4 months ago
"modern" haskell implementation of the algorithm described in the paper of the same name.
Updated 9 months ago