References

1. Ian Bayley (2001): Generic Operations on Nested Datatypes. University of Oxford.
2. Yves Bertot & Pierre Castéran (2004): Interactive theorem proving and program development. Coq'Art: The Calculus of inductive constructions., doi:10.1007/978-3-662-07964-5.
3. Richard Bird & Lambert Meertens (1998): Nested datatypes. In: Johan Jeuring: Mathematics of Program Construction. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 52–67, doi:10.1007/BFb0054285.
4. Richard Bird & Ross Paterson (1999): Generalised Folds for Nested Datatypes. Formal Aspects of Computing 11(2), pp. 200222, doi:10.1007/s001650050047.
5. Pierre-Evariste Dagand & Conor McBride (2014): Transporting functions across ornaments. Journal of Functional Programming 24(2-3), pp. 316383, doi:10.1017/S0956796814000069.
6. Benjamin Delaware, Bruno C. d. S. Oliveira & Tom Schrijvers (2013): Meta-Theory à La Carte. In: Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13. Association for Computing Machinery, New York, NY, USA, pp. 207218, doi:10.1145/2429069.2429094.
7. Peng Fu & Peter Selinger: Dependently Typed Folds for Nested Data Types. ArXiv:1806.05230v1.
8. Ralf Hinze (1998): Numerical Representations as Higher-Order Nested Datatypes. Technical Report.
9. Ralf Hinze (1999): Efficient Generalized Folds. Technical Report.
10. Ralf Hinze & Ross Paterson (2006): Finger trees: a simple general-purpose data structure. Journal of Functional Programming 16(2), pp. 197217, doi:10.1017/S0956796805005769.
11. José Pedro Magalhães, Atze Dijkstra, Johan Jeuring & Andres Löh (2010): A Generic Deriving Mechanism for Haskell. In: Proceedings of the Third ACM Haskell Symposium on Haskell, Haskell '10. Association for Computing Machinery, New York, NY, USA, pp. 3748, doi:10.1145/1863523.1863529.
12. Clare Martin, Jeremy Gibbons & Ian Bayley (2004): Disciplined, efficient, generalised folds for nested datatypes. Formal Asp. Comput. 16, pp. 19–35, doi:10.1007/s00165-003-0013-6.
13. Ulf Norell (2009): Dependently Typed Programming in Agda, pp. 1–2, doi:10.1007/978-3-642-04652-0_5.
14. Chris Okasaki (1998): Purely Functional Data Structures. Cambridge University Press, doi:10.1017/CBO9780511530104.
15. Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau & Théo Winterhalter (2020): The MetaCoq Project. J. Autom. Reason. 64(5), pp. 947–999, doi:10.1007/s10817-019-09540-0.
16. Philip Wadler (1989): Theorems for Free!. In: Proceedings of the Fourth International Conference on Functional Programming Languages and Computer Architecture, FPCA '89. Association for Computing Machinery, New York, NY, USA, pp. 347359, doi:10.1145/99370.99404.
17. Thomas Williams, Pierre-Évariste Dagand & Didier Rémy (2014): Ornaments in Practice. In: Proceedings of the 10th ACM SIGPLAN Workshop on Generic Programming, WGP '14. Association for Computing Machinery, New York, NY, USA, pp. 1524, doi:10.1145/2633628.2633631.
18. Yuming Zou & Paul E. Black (2019): perfect binary tree. Available at https://www.nist.gov/dads/HTML/perfectBinaryTree.html.

Comments and questions to: eptcs@eptcs.org

For website issues: webmaster@eptcs.org