LINK [1] T. Altenkirch and C. McBride, “Generic programming within dependently typed programming,” In IFIP TC2/WG2.1 Working Conference on Generic Programming, pp.1-20. Kluwer, B.V., 2003.

LINK [2] J.-P. Bernardy, A Theory of Parametric Polymorphism and an Application. PhD thesis, Chalmers University of Technology, 2011.

LINK [3] J.-P. Bernardy and M. Lasson, “Realizability and parametricity in pure type systems,” In Martin Hofmann, editor, Foundations of Software Science and Computation Structures, volume 6604 of Lecture Notes in Computer Science, pp.108-122. Springer-Verlag, 2011.

LINK [4] E. Brady, Practical Implementation of a Dependently Typed Functional Programming Language. PhD thesis, University of Durham, 2005.

LINK [5] J. Chapman, P.-É. Dagand, C. McBride, and P. Morris, “The gentle art of levitation,” In International Conference on Functional Programming, ICFP,'10, pp.3-14. ACM, 2010.

LINK [6] P.-É. Dagand and C. McBride, “Transporting functions across ornaments,” In International Conference on Functional Programming, ICFP,'12, pp.103-114. ACM, Sept. 2012.

LINK [7] P. Dybjer, “Inductive families,” Formal Aspects of Computing, vol.6, pp.440-465, 1994.

LINK [8] H.-S. Ko and J. Gibbons, “Modularising inductive families,” In Jaakko Järvi and Shin-Cheng Mu, editors, Workshop on Generic Programming, WGP,'11, pp.13-24. ACM, Sept. 2011.

LINK [9] P. M.-Löf. Intuitionistic Type Theory. Bibliopolis, Napoli, 1984.

LINK [10] C. McBride, “Ornamental algebras, algebraic ornaments,” To appear in Journal of Functional Programming.

LINK [11] S. Monnier and D. Haguenauer, “Singleton types here, singleton types there, singleton types everywhere,” In Programming Languages meets Program Verification, PLPV,'10, pp.1-8. ACM, Jan. 2010.

LINK [12] U. Norell, “Dependently typed programming in Agda,” In P. Koopman, R. Plasmeijer, and D. Swierstra, editors, Advanced Functional Programming, vol.5832 of Lecture Notes in Computer Science, pp.230-266. Springer-Verlag, 2009.

LINK [13] C. Okasaki. Purely functional data structures. Cambridge University Press, 1999.