diff --git a/data/bibliography.bib b/data/bibliography.bib
index 618f637ce..89c05f419 100644
--- a/data/bibliography.bib
+++ b/data/bibliography.bib
@@ -107,3 +107,42 @@ @book{Rocca:2004
 	publisher = {Springer},
 	title = {The Parametric Lambda Calculus},
 	year = {2004}}
+
+@inproceedings{Schafer:2015,
+  title={Autosubst: Reasoning with de Bruijn terms and parallel substitutions},
+  author={Sch{\"a}fer, Steven and Tebbi, Tobias and Smolka, Gert},
+  booktitle={Interactive Theorem Proving: 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings 6},
+  pages={359--374},
+  year={2015},
+  organization={Springer}
+}
+
+@techreport{Pfenning:1992,
+	author = {Pfenning, Frank},
+	institution = {Carnegie Mellon University},
+	number = {CMU-CS-92-186},
+	publisher = {Carnegie Mellon University},
+	title = {A Proof of the Church-Rosser Theorem and Its Representation in a Logical Framework},
+	year = {1992}}
+
+@article{Takahashi:1995,
+title = {Parallel Reductions in λ-Calculus},
+journal = {Information and Computation},
+volume = {118},
+number = {1},
+pages = {120-127},
+year = {1995},
+doi = {https://doi.org/10.1006/inco.1995.1057},
+author = {M. Takahashi}}
+
+@inproceedings{Nipkow:1996,
+    author = {Nipkow, Tobias},
+    title = {More Church-Rosser Proofs (in Isabelle/HOL)},
+    year = {1996},
+    publisher = {Springer-Verlag},
+    address = {Berlin, Heidelberg},
+    booktitle = {Proceedings of the 13th International Conference on Automated Deduction: Automated Deduction},
+    pages = {733–747},
+    numpages = {15},
+    series = {CADE-13}
+    }
diff --git a/src/plfa/part2/Confluence.lagda.md b/src/plfa/part2/Confluence.lagda.md
index 610831444..8bb75d6de 100644
--- a/src/plfa/part2/Confluence.lagda.md
+++ b/src/plfa/part2/Confluence.lagda.md
@@ -608,13 +608,13 @@ confluence L↠M₁ L↠M₂
 ## Notes
 
 This mechanized proof of confluence is based on several sources. The
-`subst-par` lemma is the "strong substitutivity" lemma of Shafer,
-Tebbi, and Smolka (ITP 2015). The proofs of `par-triangle`, `strip`,
+`subst-par` lemma is the "strong substitutivity" lemma of
+@Schafer:2015. The proofs of `par-triangle`, `strip`,
 and `par-confluence` are based on the notion of complete development
-by Takahashi (1995) and Pfenning's 1992 technical report about the
+by @Takahashi:1995 and the technical report by @Pfenning:1992 about the
 Church-Rosser theorem. In addition, we consulted Nipkow and
 Berghofer's mechanization in Isabelle, which is based on an earlier
-article by Nipkow (JAR 1996).
+paper by @Nipkow:1996.
 
 ## Unicode