From 71544a1564d33c32bb2d5db07cf9a7b4de430839 Mon Sep 17 00:00:00 2001
From: depsterr <depsterr@protonmail.com>
Date: Fri, 8 Dec 2023 19:22:56 +0100
Subject: [PATCH] update work page

---
 work.html | 13 +------------
 1 file changed, 1 insertion(+), 12 deletions(-)

diff --git a/work.html b/work.html
index 8fc8cc1..00e4717 100644
--- a/work.html
+++ b/work.html
@@ -6,13 +6,8 @@ title: "work"
 {% katexmm %}
 <h2>projects</h2>
 
-<h3>ongoing</h3>
 <ul>
   <li><a href="https://githug.xyz/rachel/rachel.cafe">this website</a> - The project which never ends.</li>
-</ul>
-
-<h3>completed</h3>
-<ul>
   <li><a href="https://githug.xyz/rachel/pi">pi</a> - An implementation of type-in-type MLTT, with pi, sigma, identity, and natural number types.
   <li><a href="https://githug.xyz/rachel/hm">hm</a> - An implementation of a Hindley-Milner type system with non-indexed inductive types. Strictly terminating, other than a hole in the positivity checker.</li>
   <li><a href="https://githug.xyz/rachel/viddl">viddl</a> - A web front-end for youtube-dl</li>
@@ -22,16 +17,10 @@ title: "work"
   <li><a href="https://github.com/depsterr/dbg.h">dbg.h</a> - A C header using macros and C11 generics in order to create greatly informative debug messages.</li>
 </ul>
 
-<h3>put off</h3>
-<ul>
-  <li><a href="https://githug.xyz/rachel/implicitt">implicitt</a> - 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.</li>
-  <li><a href="https://githug.xyz/rachel/cwfs">cwfs</a> - 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 <em>sometime</em> in the future.</li>
-  <li><a href="https://githug.xyz/rachel/secd">secd</a> - 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.</li>
-</ul>
-
 <h2>teaching assistant work</h2>
 <table>
   <tr><th>Role</th><th>Course</th><th>Duration</th></tr>
   <tr><td>Teaching Assistant</td><td>TDA555 - Introduction to functional programming</td><td>2022-08-22 - 2022-11-04</td></tr>
+  <tr><td>Teaching Assistant</td><td>TDA555 - Introduction to functional programming</td><td>2023-08-22 - 2023-11-04</td></tr>
 </table>
 {% endkatexmm %}