LINK  Y. Bertot and P. Castéran. Interactive theorem proving and program development. Coq'Art: The calculus of inductive constructions, Springer, 2004.
LINK  A. Bove and V. Capretta, “Nested general recursion and partiality in type theory,” In R. J. Boulton and P. B. Jackson, editors, Theorem Proving in Higher Order Logics: 14th International Conference, TPHOLs 2001, vol.2152 of Lecture Notes in Computer Science, pp.121-135, Springer-Verlag, 2001.
LINK  A. Bove, P. Dybjer, and U. Norell, “A brief overview of Agda-a functional language with dependent types,” In S. Berghofer, T. Nipkow, C. Urban, and M. Wenzel, editors, TPHOLs 2009, vol.5674 of Lecture Notes in Computer Science, pp.73-78, Springer, 2009.
LINK  T. Coquand, “Infinite objects in type theory,” In H. Barendregt and T. Nipkow, editors, Types for Proofs and Programs. International Workshop TYPES'93, vol.806 of Lecture Notes in Computer Science, pp.62-78, Springer-Verlag, 1993.
LINK  N. Danielsson and T. Altenkirch, “Subtyping, declaratively,” In C. Bolduc, J. Desharnais, and B. Ktari, editors, Mathematics of Program Construction (MPC 2010), vol.6120 of Lecture Notes in Computer Science, pp.100-118. Springer Berlin/Heidelberg, 2010.
LINK  P. Dybjer, “A general formulation of simultaneous inductive-recursive definitions in type theory,” Journal of Symbolic Logic, vol.65, no.2, 2000.
LINK  P. Dybjer and A. Setzer, “A finite axiomatization of inductive-recursive definitions,” In Proceedings of TLCA 1999, vol.1581 of LNCS, pp.129-146, Springer-Verlag, 1999.
LINK  N. Ghani and P. Hancock, “An algebraic foundation and implementation of induction recursion and indexed induction recursion,” Draft paper, 2011.
LINK  N. Ghani, P. Hancock, L. Malatesta, and A. Setzer, “Fibred data types,” Draft paper, 2012.
LINK  N. Ghani, P. Hancock, and D. Pattinson, “Continuous functions on final coalgebras,” Electr. Notes Theor. Comput. Sci., vol.164, no.1, pp.141-155, 2006. Proceedings of the Eighth Workshop on Coalgebraic Methods in Computer Science (CMCS 2006).
LINK  N. Ghani, P. Hancock, and D. Pattinson, “Continuous functions on final coalgebras,” Electr. Notes Theor. Comput. Sci., vol.249, pp.3-18, 2009. Proceedings of the 25th Conference on Mathematical Foundations of Programming Semantics (MFPS 2009).
LINK  N. Ghani, P. Hancock, and D. Pattinson, “Representations of stream processors using nested fixed points,” Logical Methods in Computer Science, vol.5, no.3, 2009.
LINK  D. E. Knuth. The Art of Computer Programming, Volume III: Sorting and Searching. Addison-Wesley, 1973.
LINK  L. Malatesta, T. Altenkirch, N. Ghani, P. Hancock, and C. McBride, “Small induction recursion, indexed containers and dependent polynomials are equivalent,” Submitted for publication, 2012.
LINK  P. Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1984. Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980.
LINK  P. Martin-Löf, “Mathematics of infinity,” In P. Martin-Löf and G. Mints, editors, Conference on Computer Logic, vol.417 of Lecture Notes in Computer Science, pp.146-197, Springer, 1988.
LINK  C. Okasaki. Purely functional data structures. Cambridge University Press, 1999.
LINK  E. Palmgren, “On universes in type theory,” In Giovanni Sambin and Jan Smith, editors, Twenty-Five Years of Constructive Type Theory, vol.36 of Oxford Logic Guides, pp.191-204, Oxford Science Publications, 1998. Proceedings of a Congress Held in Venice, Oct. 1995.
LINK  M. Rathjen, “The strength of Martin-Löf type theory with a superuniverse. Part I,” Arch. Math. Log., vol.39, no.1, pp.1-39, 2000.
LINK  M. Rathjen, “The strength of Martin-Löf type theory with a superuniverse. Part II,” Arch. Math. Log., vol.40, no.3, pp.207-233, 2001.
LINK  M. Rathjen, E. R. Griffor, and E. Palmgren, “Inaccessibility in constructive set theory and type theory,” Annals of Pure and Applied Logic, vol.94, no.1-3, pp.181-200, 1998.
LINK  The Coq Development Team. The Coq Proof Assistant. Reference Manual. Version 8. INRIA, 2011: http://coq.inria.fr/refman/index.html