diff --git a/doc/report/applications.tex b/doc/report/applications.tex
index 05604dffd895e7bfc6a688a13ff5e3ff614cafc4..9728a95d3a2c07bbdfe6b015a4eaebcf419cf160 100644
--- a/doc/report/applications.tex
+++ b/doc/report/applications.tex
@@ -148,7 +148,7 @@ proof of concept implementations.
     study in mathematics particular attractive for use in computer
     algebra systems (CAS)~\cite{groebner}. This query is asking for
     concrete implementations of Gröbner Bases that match the definition
-    in the Archive of Formal Proofs (AFP).
+    in the Archive of Formal Proofs~(AFP)~\cite{afp}.
 
     We do have ULO/RDF exports for the AFP~\cite{uloisabelle}. Stated
     like this, we can probably assume that $\mathcal{Q}_4$ is a query
diff --git a/doc/report/references.bib b/doc/report/references.bib
index 74d92ba94d4db24aca50342ae6720416d7146dab..517f834d4dfbb97835836b1ae70a3202ae49fcdb 100644
--- a/doc/report/references.bib
+++ b/doc/report/references.bib
@@ -115,4 +115,9 @@
     organization = {Dublin Core Metadata Initiative},
     urldate = {2020-06-30},
     url = {https://www.dublincore.org/schemas/rdfs/},
+}
+@online{afp,
+    title={Archive of Formal Proofs},
+    urldate = {2020-07-01},
+    url = {https://www.isa-afp.org/},
 }
\ No newline at end of file