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

:(

Browse Source
This commit is contained in:
Rachel Lambda Samuelsson 2023-03-20 16:23:12 +01:00
parent 3263836cde
commit f77a4e5790
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
work.html
View File

@ -8,7 +8,6 @@ title: "work"
<h3>ongoing</h3> <h3>ongoing</h3>
<ul> <ul>
<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> <li><a href="https://githug.xyz/depsterr/implicitt">this website</a> - The project which never ends.</li>
</ul> </ul>
@ -25,6 +24,7 @@ title: "work"
<h3>put off</h3> <h3>put off</h3>
<ul> <ul>
<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. 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/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/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> <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> </ul>