rachel/rachel.cafe
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

added dead links

Browse Source
This commit is contained in:
Rachel Lambda Samuelsson 2023-01-28 14:14:16 +01:00
parent 4d5eea06d8
commit 79f8700d41
1 changed files with 11 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
work.html
View File

@ -8,25 +8,25 @@ title: "work"
<h3>ongoing</h3>
<ul>
<li><a href="">implicitt</a> - An implementation of a dependent type system with first class implicit pi types, metavariables, and holes.</li>
<li><a href="">this website</a> - The project which never ends.</li>
<li><a href="https://githug.xyz/depsterr/implicitt">implicitt</a> - An implementation of a dependent type system with first class implicit pi types, metavariables, and holes.</li>
<li><a href="https://githug.xyz/depsterr/implicitt">this website</a> - The project which never ends.</li>
</ul>
<h3>completed</h3>
<ul>
<li><a href="">pi</a> - An implementation of type-in-type MLTT, with pi, sigma, identity, and natural number types.
<li><a href="">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="">viddl</a> - A web front-end for youtube-dl</li>
<li><a href="">kino</a> - A TUI client for browsing movies</li>
<li><a href="">bc</a> - A brainfuck compiler, outputting ELF binaries for 64-bit linux.</li>
<li><a href="">mpdart</a> - An album art display for the music player mpd</li>
<li><a href="">dbg.h</a> - A C header using macros and C11 generics in order to create greatly informative debug messages.</li>
<li><a href="https://githug.xyz/depsterr/pi">pi</a> - An implementation of type-in-type MLTT, with pi, sigma, identity, and natural number types.
<li><a href="https://githug.xyz/depsterr/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/depsterr/viddl">viddl</a> - A web front-end for youtube-dl</li>
<li><a href="https://githug.xyz/depsterr/kino">kino</a> - A TUI client for browsing movies</li>
<li><a href="https://github.com/depsterr/bc">bc</a> - A brainfuck compiler, outputting ELF binaries for 64-bit linux.</li>
<li><a href="https://githug.xyz/depsterr/mpdart">mpdart</a> - An album art display for the music player mpd</li>
<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="">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="">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>
<li><a href="https://githug.xyz/depsterr/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/depsterr/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>