@inproceedings(containers1,
 author       = {Michael Abbott and Thorsten Altenkirch and Neil Ghani},
 year         = {2003},
 title        = {Categories of Containers},
 editor       = {Andrew D. Gordon},
 booktitle    = {Foundations of Software Science and Computation Structures},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {23--38},
 doi          = {10.1007/3-540-36576-1_2},
)
@inproceedings(containers3,
 author       = {Michael Abbott and Thorsten Altenkirch and Neil Ghani},
 year         = {2004},
 title        = {Representing Nested Inductive Types Using W-Types},
 editor       = {Josep D{\'i}az and Juhani Karhum{\"a}ki and Arto Lepist{\"o} and Donald Sannella},
 booktitle    = {Automata, Languages and Programming},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {59--71},
 doi          = {10.1007/978-3-540-27836-8_8},
)
@article(containers,
 author       = {Michael Abbott and Thorsten Altenkirch and Neil Ghani},
 year         = {2005},
 title        = {Containers: Constructing Strictly Positive Types},
 journal      = {Theor. Comput. Sci.},
 volume       = {342},
 number       = {1},
 pages        = {3\IeC{\textendash}27},
 doi          = {10.1016/j.tcs.2005.06.002},
)
@inproceedings(containers2,
 author       = {Michael Abbott and Thorsten Altenkirch and Neil Ghani and Conor McBride},
 year         = {2003},
 title        = {Derivatives of Containers},
 editor       = {Martin Hofmann},
 booktitle    = {Typed Lambda Calculi and Applications},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {16--30},
 doi          = {10.1007/3-540-44904-3_2},
)
@article(ranked,
 author       = {R. Bernecky},
 year         = {1987},
 title        = {An Introduction to Function Rank},
 journal      = {SIGAPL APL Quote Quad},
 volume       = {18},
 number       = {2},
 pages        = {39\IeC{\textendash}43},
 doi          = {10.1145/377719.55632},
)
@inproceedings(pooling,
 author       = {Y-Lan Boureau and Jean Ponce and Yann LeCun},
 year         = {2010},
 title        = {A Theoretical Analysis of Feature Pooling in Visual Recognition},
 booktitle    = {Proceedings of the 27th International Conference on International Conference on Machine Learning},
 series       = {ICML\IeC{\textquoteright}10},
 publisher    = {Omnipress},
 address      = {Madison, WI, USA},
 pages        = {111\IeC{\textendash}118},
)
@article(refinement-ml,
 author       = {Tim Freeman and Frank Pfenning},
 year         = {1991},
 title        = {Refinement Types for ML},
 journal      = {SIGPLAN Not.},
 volume       = {26},
 number       = {6},
 pages        = {268\IeC{\textendash}277},
 doi          = {10.1145/113446.113468},
)
@inproceedings(refinement-logic,
 author       = {Susumu Hayashi},
 year         = {1994},
 title        = {Logic of refinement types},
 editor       = {Henk Barendregt and Tobias Nipkow},
 booktitle    = {Types for Proofs and Programs},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {108--126},
 doi          = {10.1007/3-540-58085-9_74},
)
@book(Iverson:1962:APL,
 author       = {Kenneth E. Iverson},
 year         = {1962},
 title        = {A Programming Language},
 publisher    = {John Wiley \& Sons, Inc.},
 address      = {New York, NY, USA},
 doi          = {10.1145/1460833.1460872},
)
@inproceedings(fish,
 author       = {C Barry Jay and Paul A Steckler},
 year         = {1998},
 title        = {The functional imperative: shape!},
 booktitle    = {European Symposium on Programming},
 organization = {Springer},
 pages        = {139--153},
 doi          = {10.1007/BFb0053568},
)
@article(sac,
 author       = {Sven-Bodo Scholz},
 year         = {2003},
 title        = {Single Assignment C: Efficient Support for High-level Array Operations in a Functional Setting},
 journal      = {J. Funct. Program.},
 volume       = {13},
 number       = {6},
 pages        = {1005--1059},
 doi          = {10.1017/S0956796802004458},
)
@misc(github,
 author       = {{\v{S}}inkarovs, Artjoms},
 year         = {2020},
 title        = {Arrays with Levels in Agda},
 howpublished = {\url{https://github.com/ashinkarov/agda-arrays-with-levels}},
 note         = {[Accessed: March 2020]},
)
@inproceedings(remora,
 author       = {Justin Slepak and Olin Shivers and Panagiotis Manolios},
 year         = {2014},
 title        = {An Array-Oriented Language with Static Rank Polymorphism},
 editor       = {Zhong Shao},
 booktitle    = {Programming Languages and Systems},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {27--46},
 doi          = {10.1007/978-3-642-54833-8_3},
)
@misc(jlang,
 author       = {Roger Stokes},
 year         = {15 June 2015},
 title        = {Learning J. An Introduction to the J Programming Language},
 howpublished = {\url{http://www.jsoftware.com/help/learning/contents.htm}},
 note         = {[Accessed: March 2020]},
)
@article(qube,
 author       = {Kai Trojahner and Clemens Grelck},
 year         = {2009},
 title        = {Dependently typed array programs don't go wrong},
 journal      = {The Journal of Logic and Algebraic Programming},
 volume       = {78},
 number       = {7},
 pages        = {643 -- 664},
 doi          = {10.1016/j.jlap.2009.03.002},
 note         = {The 19th Nordic Workshop on Programming Theory (NWPT 2007)},
)
@misc(klang,
 author       = {Arthur Whitney},
 year         = {2001},
 title        = {K},
 howpublished = {\url{http://archive.vector.org.uk/art10010830}},
 note         = {[Accessed: March 2020]},
)