diff --git a/README.md b/README.md
index 33eee5c..3ae90e2 100644
--- a/README.md
+++ b/README.md
@@ -12,3 +12,11 @@ A dependently typed system
   * Universe Polymorphism
 
   * Cumulative Universes(?)
+
+# References
+
+Some of the material I found helpful in groking dependent type checking:
+
+* Coquand, Thierry. “An Algorithm for Type-Checking Dependent Types.” Science of Computer Programming 26, no. 1–3 (May 1996): 167–77. https://doi.org/10.1016/0167-6423(95)00021-6.
+
+* Brady, Edwin. "SPLV20 course notes". GitHub. https://github.com/edwinb/SPLV20