@phdthesis(thesis-bayley,
 author       = {Ian Bayley},
 year         = {2001},
 title        = {Generic Operations on Nested Datatypes},
 school       = {University of Oxford},
)
@book(coqart,
 author       = {Yves Bertot and Pierre Cast{\'e}ran},
 year         = {2004},
 title        = {Interactive theorem proving and program development. Coq'Art: The Calculus of inductive constructions.},
 doi          = {10.1007/978-3-662-07964-5},
)
@inproceedings(bird-meertens-nested,
 author       = {Richard Bird and Lambert Meertens},
 year         = {1998},
 title        = {Nested datatypes},
 editor       = {Johan Jeuring},
 booktitle    = {Mathematics of Program Construction},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {52--67},
 doi          = {10.1007/BFb0054285},
)
@article(fold-bird-paterson,
 author       = {Richard Bird and Ross Paterson},
 year         = {1999},
 title        = {Generalised Folds for Nested Datatypes},
 journal      = {Formal Aspects of Computing},
 volume       = {11},
 number       = {2},
 pages        = {200\IeC{\textendash}222},
 doi          = {10.1007/s001650050047},
)
@article(dagand-mcbride-2014,
 author       = {Pierre-Evariste Dagand and Conor McBride},
 year         = {2014},
 title        = {Transporting functions across ornaments},
 journal      = {Journal of Functional Programming},
 volume       = {24},
 number       = {2-3},
 pages        = {316\IeC{\textendash}383},
 doi          = {10.1017/S0956796814000069},
)
@inproceedings(meta-carte-2,
 author       = {Benjamin Delaware and Bruno C. d. S. Oliveira and Tom Schrijvers},
 year         = {2013},
 title        = {Meta-Theory \`{a} La Carte},
 booktitle    = {Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
 series       = {POPL '13},
 publisher    = {Association for Computing Machinery},
 address      = {New York, NY, USA},
 pages        = {207\IeC{\textendash}218},
 doi          = {10.1145/2429069.2429094},
)
@article(Fu2018,
 author       = {Peng Fu and Peter Selinger},
 title        = {Dependently Typed Folds for Nested Data Types},
 eprint       = {1806.05230v1},
)
@techreport(ralf1998,
 author       = {Ralf Hinze},
 year         = {1998},
 title        = {Numerical Representations as Higher-Order Nested Datatypes},
 type         = {Technical Report},
)
@techreport(ralf1999a,
 author       = {Ralf Hinze},
 year         = {1999},
 title        = {Efficient Generalized Folds},
 type         = {Technical Report},
)
@article(hinze-paterson-2006,
 author       = {Ralf Hinze and Ross Paterson},
 year         = {2006},
 title        = {Finger trees: a simple general-purpose data structure},
 journal      = {Journal of Functional Programming},
 volume       = {16},
 number       = {2},
 pages        = {197\IeC{\textendash}217},
 doi          = {10.1017/S0956796805005769},
)
@inproceedings(deriving-haskel,
 author       = {Magalh\~{a}es, Jos\'{e} Pedro and Atze Dijkstra and Johan Jeuring and Andres L\"{o}h},
 year         = {2010},
 title        = {A Generic Deriving Mechanism for Haskell},
 booktitle    = {Proceedings of the Third ACM Haskell Symposium on Haskell},
 series       = {Haskell '10},
 publisher    = {Association for Computing Machinery},
 address      = {New York, NY, USA},
 pages        = {37\IeC{\textendash}48},
 doi          = {10.1145/1863523.1863529},
)
@article(fold-martin-gibbons-bayley,
 author       = {Clare Martin and Jeremy Gibbons and Ian Bayley},
 year         = {2004},
 title        = {Disciplined, efficient, generalised folds for nested datatypes},
 journal      = {Formal Asp. Comput.},
 volume       = {16},
 pages        = {19--35},
 doi          = {10.1007/s00165-003-0013-6},
)
@inproceedings(agda,
 author       = {Ulf Norell},
 year         = {2009},
 title        = {Dependently Typed Programming in Agda},
 pages        = {1--2},
 doi          = {10.1007/978-3-642-04652-0\_5},
)
@book(okasaki-1998,
 author       = {Chris Okasaki},
 year         = {1998},
 title        = {Purely Functional Data Structures},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9780511530104},
)
@article(Sozeau20,
 author       = {Matthieu Sozeau and Abhishek Anand and Simon Boulier and Cyril Cohen and Yannick Forster and Fabian Kunze and Gregory Malecha and Nicolas Tabareau and Th{\'{e}}o Winterhalter},
 year         = {2020},
 title        = {The MetaCoq Project},
 journal      = {J. Autom. Reason.},
 volume       = {64},
 number       = {5},
 pages        = {947--999},
 doi          = {10.1007/s10817-019-09540-0},
)
@inproceedings(th-for-free,
 author       = {Philip Wadler},
 year         = {1989},
 title        = {Theorems for Free!},
 booktitle    = {Proceedings of the Fourth International Conference on Functional Programming Languages and Computer Architecture},
 series       = {FPCA '89},
 publisher    = {Association for Computing Machinery},
 address      = {New York, NY, USA},
 pages        = {347\IeC{\textendash}359},
 doi          = {10.1145/99370.99404},
)
@inproceedings(ornaments-in-practice,
 author       = {Thomas Williams and Pierre-\'{E}variste Dagand and Didier R\'{e}my},
 year         = {2014},
 title        = {Ornaments in Practice},
 booktitle    = {Proceedings of the 10th ACM SIGPLAN Workshop on Generic Programming},
 series       = {WGP '14},
 publisher    = {Association for Computing Machinery},
 address      = {New York, NY, USA},
 pages        = {15\IeC{\textendash}24},
 doi          = {10.1145/2633628.2633631},
)
@(ptree,
 author       = {Yuming Zou and Paul E. Black},
 year         = {2019},
 title        = {perfect binary tree},
 url          = {https://www.nist.gov/dads/HTML/perfectBinaryTree.html},
)