Add bibliography for ADTs

src/bib/scala-with-cats.bib

@@ -128,3 +128,100 @@ @article{10.1145/3158130
 numpages = {29},
 keywords = {implicit parameters, Scala, Dotty}
 }
+
+
+@Book{felleisen18:htdp,
+  author          = {Matthias Felleisen and Robert Bruce Findler and Matthew Flatt and Shriram Krishnamurthi},
+  title           = {How to Design Programs, Second Edition},
+  year            = {2018},
+  subtitle     = {An Introductino to Programming and Computing},
+  publisher    = {The MIT Press},
+  isbn         = 9780262534802,
+  url          = {https://htdp.org/}}
+
+
+@InProceedings{10.1007/3540543961_7,
+author="Meijer, Erik
+and Fokkinga, Maarten
+and Paterson, Ross",
+editor="Hughes, John",
+title="Functional programming with bananas, lenses, envelopes and barbed wire",
+booktitle="Functional Programming Languages and Computer Architecture",
+year="1991",
+publisher="Springer Berlin Heidelberg",
+address="Berlin, Heidelberg",
+pages="124--144",
+abstract="We develop a calculus for lazy functional programming based on recursion operators associated with data type definitions. For these operators we derive various algebraic laws that are useful in deriving and manipulating programs. We shall show that all example functions in Bird and Wadler's ``Introduction to Functional Programming'' can be expressed using these operators.",
+isbn="978-3-540-47599-6",
+url={https://ris.utwente.nl/ws/portalfiles/portal/6142049/meijer91functional.pdf}
+}
+
+@article{10.1093/comjnl/12.1.41,
+    author = {Burstall, R. M.},
+    title = "{Proving Properties of Programs by Structural Induction}",
+    journal = {The Computer Journal},
+    volume = {12},
+    number = {1},
+    pages = {41-48},
+    year = {1969},
+    month = {02},
+    abstract = "{This paper discusses the technique of structural induction for proving theorems about programs. This technique is closely related to recursion induction but makes use of the inductive definition of the data structures handled by the programs. It treats programs with recursion but without assignments or jumps. Some syntactic extensions to Landin's functional programming language ISWIM are suggested which make it easier to program the manipulation of data structures and to develop proofs about such programs. Two sample proofs are given to demonstrate the technique, one for a tree sorting algorithm and one for a simple compiler for expressions.}",
+    issn = {0010-4620},
+    doi = {10.1093/comjnl/12.1.41},
+    url = {https://doi.org/10.1093/comjnl/12.1.41},
+    eprint = {https://academic.oup.com/comjnl/article-pdf/12/1/41/885019/12-1-41.pdf},
+}
+
+@article{GIBBONS_2021,
+ title={How to design co-programs},
+ volume={31},
+ DOI={10.1017/S0956796821000113},
+ journal={Journal of Functional Programming},
+ author={Gibbons, Jeremy},
+ year={2021},
+ pages={e15}
+}
+
+@inproceedings{10.1145/289423.289455,
+author = {Gibbons, Jeremy and Jones, Geraint},
+title = {The under-appreciated unfold},
+year = {1998},
+isbn = {1581130244},
+publisher = {Association for Computing Machinery},
+address = {New York, NY, USA},
+url = {https://doi.org/10.1145/289423.289455},
+doi = {10.1145/289423.289455},
+abstract = {Folds are appreciated by functional programmers. Their dual, unfolds, are not new, but they are not nearly as well appreciated. We believe they deserve better. To illustrate, we present (indeed, we calculate) a number of algorithms for computing the breadth-first traversal of a tree. We specify breadth-first traversal in terms of level-order traversal, which we characterize first as a fold. The presentation as a fold is simple, but it is inefficient, and removing the inefficiency makes it no longer a fold. We calculate a characterization as an unfold from the characterization as a fold; this unfold is equally clear, but more efficient. We also calculate a characterization of breadth-first traversal directly as an unfold; this turns out to be the 'standard' queue-based algorithm.},
+booktitle = {Proceedings of the Third ACM SIGPLAN International Conference on Functional Programming},
+pages = {273–279},
+numpages = {7},
+keywords = {anamorphism, breadth-first, co-induction, fold, functional programing, level-order, program calculation, traversal, unfold},
+location = {Baltimore, Maryland, USA},
+series = {ICFP '98}
+}
+
+@article{10.1145/291251.289455,
+author = {Gibbons, Jeremy and Jones, Geraint},
+title = {The under-appreciated unfold},
+year = {1998},
+issue_date = {Jan. 1999},
+publisher = {Association for Computing Machinery},
+address = {New York, NY, USA},
+volume = {34},
+number = {1},
+issn = {0362-1340},
+url = {https://doi.org/10.1145/291251.289455},
+doi = {10.1145/291251.289455},
+abstract = {Folds are appreciated by functional programmers. Their dual, unfolds, are not new, but they are not nearly as well appreciated. We believe they deserve better. To illustrate, we present (indeed, we calculate) a number of algorithms for computing the breadth-first traversal of a tree. We specify breadth-first traversal in terms of level-order traversal, which we characterize first as a fold. The presentation as a fold is simple, but it is inefficient, and removing the inefficiency makes it no longer a fold. We calculate a characterization as an unfold from the characterization as a fold; this unfold is equally clear, but more efficient. We also calculate a characterization of breadth-first traversal directly as an unfold; this turns out to be the 'standard' queue-based algorithm.},
+journal = {SIGPLAN Not.},
+month = {sep},
+pages = {273–279},
+numpages = {7},
+keywords = {anamorphism, breadth-first, co-induction, fold, functional programing, level-order, program calculation, traversal, unfold}
+}
+
+@Unpublished{mcbride01:deriv,
+  author          = {Conor McBride},
+  title           = {The Derivative of a Regular Type is its Type of One-Hole Contexts},
+  date            = 2001,
+  url          = {http://strictlypositive.org/diff.pdf}}

src/pages/adt/conclusions.md

@@ -23,22 +23,21 @@ Below are some references that you might find useful if you want to dig in furth
 
 Algebraic data types are standard in introductory material on functional programming. 
 Structural recursion is certainly extremely common in functional programming, but strangely seems to rarely be explicitly defined as I've done here.
-I learned about both from [How to Design Programs](https://htdp.org/).
+I learned about both from *How to Design Programs* [@felleisen18:htdp].
 
 I'm not aware of any approachable yet thorough treatment of either algebraic data types or structural recursion.
 Both seem to have become assumed background of any researcher in the field of programming languages,
 and relatively recent work is caked in layers of mathematics and obtuse notation that I find difficult reading.
-The infamous [Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire][banana] is an example of such work.
+The infamous *Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire* [@10.1007/3540543961_7] is an example of such work.
 I suspect the core ideas of both date back to at least the emergence of computability theory in the 1930s, well before any digital computers existed.
 
-The earliest reference I've found to structural recursion is [Proving Properties of Programs by Structural Induction][structural-induction], which dates to 1969. 
+The earliest reference I've found to structural recursion is *Proving Properties of Programs by Structural Induction* [@10.1093/comjnl/12.1.41]. 
 Algebraic data types don't seem to have been fully developed, along with pattern matching, until [NPL][npl] in 1977. 
 NPL was quickly followed by the more influential language [Hope][hope], which spread the concept to other programming languages.
 
-Corecursion is a bit better documented in the contemporary literature. [How to Design Co-Programs][htdc] covers the main idea we have looked at here. 
-[The Under-Appreciated Unfold][unfold] discusses uses of `unfold`. 
+Corecursion is a bit better documented in the contemporary literature. *How to Design Co-Programs* [@GIBBONS_2021] covers the main ideas we have looked at here, while @10.1145/291251.289455 discusses uses of `unfold`.
 
-[The Derivative of a Regular Type is its Type of One-Hole Contexts][deriv] describes the derivative of algebraic data types.
+*The Derivative of a Regular Type is its Type of One-Hole Contexts* [@mcbride01:deriv] describes the derivative of algebraic data types.