1 files changed, 50 insertions, 0 deletions
diff --git a/plt/types.md b/plt/types.md
new file mode 100644
index 0000000..d0e1729
--- /dev/null
+++ b/plt/types.md
@@ -0,0 +1,50 @@
+---
+layout: plt
+title: computation/types
+---
+
+# types! ah, wonderous types!
+
+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
+
+
+## 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)