From ad9e54a7f55a893a4f588de27ebf18e7237a6005 Mon Sep 17 00:00:00 2001 From: depsterr Date: Mon, 16 May 2022 17:49:56 +0200 Subject: [PATCH] add some references to useful material in the readme --- README.md | 8 ++++++++ 1 file changed, 8 insertions(+) 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