bibliography.bib

@article{hinze_memo_2000,
	title = {Memo functions, polytypically!},
	volume = {2},
	pages = {17--32},
	journaltitle = {Workshop on Generic Programming},
	author = {Hinze, Ralf},
	date = {2000},
	file = {WGP2000.ps:/home/sandy/Zotero/storage/R3TFGBZW/WGP2000.ps:application/postscript},
}

@article{elliott_generic_2017,
	title = {Generic functional parallel algorithms: scan and {FFT}},
	volume = {1},
	issn = {2475-1421},
	url = {https://dl.acm.org/doi/10.1145/3110251},
	doi = {10.1145/3110251},
	shorttitle = {Generic functional parallel algorithms},
	abstract = {Parallel programming, whether imperative or functional, has long focused on arrays as the central data type. Meanwhile, typed functional programming has explored a variety of data types, including lists and various forms of trees.
              Generic
              functional programming decomposes these data types into a small set of fundamental building blocks: sum, product, composition, and their associated identities. Definitions over these few fundamental type constructions then automatically assemble into algorithms for an infinite variety of data types—some familiar and some new. This paper presents generic functional formulations for two important and well-known classes of parallel algorithms: parallel scan (generalized prefix sum) and fast Fourier transform ({FFT}). Notably, arrays play no role in these formulations. Consequent benefits include a simpler and more compositional style, much use of common algebraic patterns and freedom from possibility of run-time indexing errors. The functional generic style also clearly reveals deep commonality among what otherwise appear to be quite different algorithms. Instantiating the generic formulations, two well-known algorithms for each of parallel scan and {FFT} naturally emerge, as well as two possibly new algorithms.},
	pages = {1--25},
	issue = {{ICFP}},
	journaltitle = {Proceedings of the {ACM} on Programming Languages},
	shortjournal = {Proc. {ACM} Program. Lang.},
	author = {Elliott, Conal},
	urldate = {2023-10-23},
	date = {2017-08-29},
	langid = {english},
	file = {Full Text:/home/sandy/Zotero/storage/8ITVCU74/Elliott - 2017 - Generic functional parallel algorithms scan and F.pdf:application/pdf},
}

@audio{abreu_mechanizing_2023,
	title = {Mechanizing Modern Mathematics},
	url = {https://www.typetheoryforall.com/2023/01/16/26-Kevin-Buzzard.html},
	number = {26},
	author = {Abreu, Pedro and Buzzard, Kevin},
	urldate = {2023-04-01},
	date = {2023-01-16},
	note = {Date: 2023-01-16
Issued: 2023-01-16},
}

@report{kidney_automatically_2019,
	title = {Automatically and efficiently illustrating polynomial equalities in Agda},
	institution = {University College Cork},
	type = {Technical Report},
	author = {Kidney, Donnacha Oisín},
	date = {2019},
}

@software{the_agda_community_agda_2023,
	title = {Agda Standard Library},
	url = {https://github.com/agda/agda-stdlib},
	version = {1.7.2},
	author = {The Agda Community,},
	date = {2023-02-01},
}

@movie{hedges_about_2002,
	title = {About a Boy},
	publisher = {Universal Pictures},
	author = {Hedges, Peter},
	editora = {Hornby, Nick},
	editoratype = {collaborator},
	date = {2002},
}

@report{the_agda_community_agda_2023-1,
	title = {Agda User Manual},
	url = {https://agda.readthedocs.io/en/v2.6.3/},
	number = {2.6.3},
	type = {User Manual},
	author = {The Agda Community,},
	date = {2023},
}

@inproceedings{mcbride_how_2014,
	location = {Gothenburg Sweden},
	title = {How to keep your neighbours in order},
	isbn = {978-1-4503-2873-9},
	url = {https://dl.acm.org/doi/10.1145/2628136.2628163},
	doi = {10.1145/2628136.2628163},
	eventtitle = {{ICFP}'14: {ACM} {SIGPLAN} International Conference on Functional Programming},
	pages = {297--309},
	booktitle = {Proceedings of the 19th {ACM} {SIGPLAN} international conference on Functional programming},
	publisher = {{ACM}},
	author = {{McBride}, Conor Thomas},
	urldate = {2023-10-23},
	date = {2014-08-19},
	langid = {english},
	file = {Full Text:/home/sandy/Zotero/storage/T9LK7GJY/McBride - 2014 - How to keep your neighbours in order.pdf:application/pdf},
}

@online{graham_beating_2001,
	title = {Beating the Averages},
	url = {http://www.paulgraham.com/avg.html},
	titleaddon = {Paul Graham},
	author = {Graham, Paul},
	date = {2001-04},
}

@incollection{scholz_parsing_2011,
	location = {Berlin, Heidelberg},
	title = {Parsing Mixfix Operators},
	volume = {5836},
	isbn = {978-3-642-24451-3 978-3-642-24452-0},
	url = {http://link.springer.com/10.1007/978-3-642-24452-0_5},
	pages = {80--99},
	booktitle = {Implementation and Application of Functional Languages},
	publisher = {Springer Berlin Heidelberg},
	author = {Danielsson, Nils Anders and Norell, Ulf},
	editor = {Scholz, Sven-Bodo and Chitil, Olaf},
	urldate = {2023-10-23},
	date = {2011},
	doi = {10.1007/978-3-642-24452-0_5},
	note = {Series Title: Lecture Notes in Computer Science},
}

@article{hughes_novel_1986,
	title = {A novel representation of lists and its application to the function “reverse”},
	volume = {22},
	issn = {00200190},
	url = {https://linkinghub.elsevier.com/retrieve/pii/0020019086900591},
	doi = {10.1016/0020-0190(86)90059-1},
	pages = {141--144},
	number = {3},
	journaltitle = {Information Processing Letters},
	shortjournal = {Information Processing Letters},
	author = {Hughes, R.John Muir},
	urldate = {2023-10-26},
	date = {1986-03},
	langid = {english},
}