diff --git a/README.md b/README.md
index f37f708..fbd99fb 100644
--- a/README.md
+++ b/README.md
@@ -22,6 +22,12 @@ A collection of articles & links
     - [Certified Programming with Dependent Types](http://adam.chlipala.net/cpdt/cpdt.pdf)
     - [Types and Programming Languages](https://basics.sjtu.edu.cn/~xiaojuan/tapl2016/files/Types+and+Programming+Languages.pdf)
 
+### Type-Theory
+- [An Introduction to Type Theory and Formal Semantics](https://staffwww.fullcoll.edu/aclifton/files/intro-to-type-theory.pdf)
+- [A Dependent Type Theory with Abstractable Names](https://www.cl.cam.ac.uk/~amp12/papers/deptta/deptta-preprint.pdf)
+- [Certified Programming with Dependent Types](http://adam.chlipala.net/cpdt/cpdt.pdf)
+
+
 ### Development
 
 - [CatchTS](https://catchts.com/) - A TypeScript blog
@@ -90,6 +96,7 @@ A collection of articles & links
 
 ## Off-Topic
 
+- [The CRAPL - an academic-strength open-source license](https://matt.might.net/articles/crapl/)
 - [GPR](https://integrated.ugcs.com/gpr) - Drone-powered geographical surveys
 - [DoE NEPA](https://www.energy.gov/nepa/nepa-documents) - Documents required by DoE for environmental impact survey
 - [If-Im-Gone](https://news.ycombinator.com/item?id=31943941) - Template cheat-sheet for your partner