diff --git a/work.html b/work.html
index c723c07..8fc8cc1 100644
--- a/work.html
+++ b/work.html
@@ -8,25 +8,25 @@ title: "work"
ongoing
completed
- - pi - An implementation of type-in-type MLTT, with pi, sigma, identity, and natural number types.
-
- hm - An implementation of a Hindley-Milner type system with non-indexed inductive types. Strictly terminating, other than a hole in the positivity checker.
- - viddl - A web front-end for youtube-dl
- - kino - A TUI client for browsing movies
+ - pi - An implementation of type-in-type MLTT, with pi, sigma, identity, and natural number types.
+
- hm - An implementation of a Hindley-Milner type system with non-indexed inductive types. Strictly terminating, other than a hole in the positivity checker.
+ - viddl - A web front-end for youtube-dl
+ - kino - A TUI client for browsing movies
- bc - A brainfuck compiler, outputting ELF binaries for 64-bit linux.
- - mpdart - An album art display for the music player mpd
+ - mpdart - An album art display for the music player mpd
- dbg.h - A C header using macros and C11 generics in order to create greatly informative debug messages.
put off
- - implicitt - An implementation of a dependent type system with first class implicit pi types, metavariables, and holes. Put off cause I put too large a scope on a learning project and overworked myself. Hopefully I'll pick this up again sometime.
- - cwfs - A formalisation of categories with families in cubical agda. Put off due to the extensional nature of the theory making formalisation a pain. I plan to retry with natural models sometime in the future.
- - secd - An implementation of a VM designed as a compilation target for languages based on the lambda calculus. Put off due to not wanting to work out implementation details or write more C. I hope to use what I learned for optimized evaluation of closures in a dependent type system some day.
+ - implicitt - An implementation of a dependent type system with first class implicit pi types, metavariables, and holes. Put off cause I put too large a scope on a learning project and overworked myself. Hopefully I'll pick this up again sometime.
+ - cwfs - A formalisation of categories with families in cubical agda. Put off due to the extensional nature of the theory making formalisation a pain. I plan to retry with natural models sometime in the future.
+ - secd - An implementation of a VM designed as a compilation target for languages based on the lambda calculus. Put off due to not wanting to work out implementation details or write more C. I hope to use what I learned for optimized evaluation of closures in a dependent type system some day.
teaching assistant work