meow

4 files changed, 54 insertions, 17 deletions

diff --git a/computation/compilers.md b/computation/compilers.md
index b3b1769..b9db36d 100644
--- a/computation/compilers.md
+++ b/computation/compilers.md
@@ -1,8 +1,10 @@
-# Compilers
+# compilers
 
-Books and Courses
-- [Introduction to Compiler Construction](https://www.students.cs.ubc.ca/~cs-411/2022w2/book_top.html)
-- [Programming Languages, Application and Interpretation](https://www.plai.org/)
-
-Articles
+articles
 - [Compiler Optimizations Are Hard Because They Forget](https://faultlore.com/blah/oops-that-was-important/)
+- [A tutorial on how to write a compiler using LLVM](https://tomassetti.me/a-tutorial-on-how-to-write-a-compiler-using-llvm/)
+
+books and courses
+- [Programming Languages, Application and Interpretation](https://www.plai.org/)
+- [Introduction to Compiler Construction](https://www.students.cs.ubc.ca/~cs-411/2022w2/book_top.html)
+- [Design Your Own Language (book list)](https://slebok.github.io/dyol/books/index.html)
diff --git a/computation/effects.md b/computation/effects.md
index ac11fae..98312c5 100644
--- a/computation/effects.md
+++ b/computation/effects.md
@@ -7,6 +7,7 @@ posts
 - [From deliminated continuations to algebraic effects](https://blog.poisson.chat/posts/2023-01-02-del-cont-examples.html)
 - [OCaml Effects Tutorial](https://github.com/ocaml-multicore/ocaml-effects-tutorial)
 - [Simple functional effects with tag unions](https://www.youtube.com/watch?v=7SidSvJcPd0)
+- [Effect bibliography](https://github.com/yallop/effects-bibliography)
 
 papers
 - [What is algebraic about algebraic effects and handlers?](https://arxiv.org/abs/1807.05923)
diff --git a/computation/syntax.md b/computation/syntax.md
index 7dd776d..29e8c48 100644
--- a/computation/syntax.md
+++ b/computation/syntax.md
@@ -1,19 +1,19 @@
-# Syntax
+# syntax
 
-## Resources
-
-Articles
+articles
 - [An Overview of Lexing and Parsing](https://www.perl.com/pub/2012/10/an-overview-of-lexing-and-parsing.html/)
 - [Just write the #!%/* parser](https://tiarkrompf.github.io/notes/?/just-write-the-parser/)
 
-Books and Courses
-- [Compilers: Principles, Techniques, Tools](https://annas-archive.org/md5/90db32d070cfb70ca617e655d5c35529)
+books
+- [_Compilers: Principles, Techniques, Tools_](https://annas-archive.org/md5/90db32d070cfb70ca617e655d5c35529)
+
+## notation
 
-## Notation
+ebnf
 
-## Lexing
+## lexing
 
-## Parsing
+## parsing
 
 cover:
 - please please please lex
diff --git a/computation/types.md b/computation/types.md
index 2edfe7c..2124175 100644
--- a/computation/types.md
+++ b/computation/types.md
@@ -1,11 +1,45 @@
 # types! ah, wonderous types!
 
-## Resources
+posts
+- [How should I read type system notation?](https://langdev.stackexchange.com/questions/2692/how-should-i-read-type-system-notation/)
+- [Programming Language Theory resources](https://steshaw.org/plt/)
+
+books
+- [_**Types and Programming Languages**_](https://www.cis.upenn.edu/~bcpierce/tapl/) by Benjamin C. Pierce: the canonical type system text
+- [_Advanced Topics in Types and Programming Languages_](https://www.cis.upenn.edu/~bcpierce/attapl/) by Benjamin C. Pierce
 
-- *Types and Programming Languages* by Benjamin C. Pierce
 
 ## algebraic data types
 
 ## inductive types
 - https://en.wikipedia.org/wiki/Inductive_type
 
+## refinement types
+
+- [Liquid Haskell](https://ucsd-progsys.github.io/liquidhaskell/)
+- [Refinement Types in Liquid Haskell](https://ucsd-progsys.github.io/liquidhaskell-tutorial/)
+- [Refinement Types: A Tutorial](https://arxiv.org/abs/2010.07763)
+
+## dependent types
+
+usage
+- [Programming Language Foundations](https://jscoq.github.io/ext/sf/plf/full/toc.html)
+- [Programming Language Foundations in Agda](https://plfa.github.io/)
+
+languages
+- [Coq](https://coq.inria.fr/)
+- [Lean](https://lean-lang.org/)
+- [Agda](https://wiki.portal.chalmers.se/agda/pmwiki.php)
+- [Isabelle](https://isabelle.in.tum.de/)
+
+implementation
+- [Checking dependent types with normalization by evaluation](https://davidchristiansen.dk/tutorials/nbe/)
+- [Barebones lambda cube in OCaml](https://gist.github.com/Hirrolot/89c60f821270059a09c14b940b454fd6)
+- [Dependent types in 80 lines of code](https://gist.github.com/Hirrolot/27e6b02a051df333811a23b97c375196)
+
+papers
+- [Turnstile+: dependent type systems as macros](https://www.williamjbowman.com/resources/wjb2019-depmacros.pdf)
+
+## homotopy type theory
+
+- [*Homotopy Type Theory*](https://homotopytypetheory.org)