adding bibliography entries in Confluence chapter (#907)

* adding bibliography entries * [pre-commit.ci] auto fixes from pre-commit.com hooks for more information, see https://pre-commit.ci * Run pre-commit hooks. --------- Co-authored-by: pre-commit-ci[bot] <66853113+pre-commit-ci[bot]@users.noreply.github.com> Co-authored-by: Wen Kokke <[email protected]>
plfa · Sep 11, 2023 · 68ec4b9 · 68ec4b9
1 parent da5b10b
commit 68ec4b9
Show file tree

Hide file tree

Showing 2 changed files with 43 additions and 4 deletions.
diff --git 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
@@ -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