Address @vidsinghal's comments

Author: MatthewDaggitt

paper/paper.bib

@@ -328,5 +328,11 @@ @article{10.1145/2034773.2034796
 keywords = {type classes, instance arguments, agda, ad hoc polymorphism}
 }
 
-  
-
+@inproceedings{wadler2018programming,
+  title={Programming language foundations in agda},
+  author={Wadler, Philip},
+  booktitle={Brazilian Symposium on Formal Methods},
+  pages={56--73},
+  year={2018},
+  organization={Springer}
+}

paper/paper.md

@@ -144,6 +144,10 @@ This allows users to specify instantiations of abstract parameters for whole mod
 A drawback is imports must be qualified when code is instantiated multiple times in the same scope.
 Parameterised modules are also used to safely and scalably embed non-constructive mathematics into a constructive setting.
 
+The README directory within the library contains both documentation on the general design decisions and
+examples of how to use the most common modules in the library to prove basic concepts.
+There are many excellent tutorials online that introduce both Agda and `agda-stdlib` together, with ``Programming Language Foundations in Agda'' [@wadler2018programming] being an example of one such tutorial.
+
 # Testing
 
 Correctness proofs do not remove the need for testing performance and features that cannot be reasoned about internally (such as the FFI and macros).