diff --git a/work.html b/work.html
index cecf952..c723c07 100644
--- a/work.html
+++ b/work.html
@@ -8,7 +8,6 @@ title: "work"
ongoing
- - implicitt - An implementation of a dependent type system with first class implicit pi types, metavariables, and holes.
- this website - The project which never ends.
@@ -25,6 +24,7 @@ title: "work"
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.