M. G. Abbott, T. Altenkirch, and N. Ghani, Representing Nested Inductive Types Using W-Types, ICALP 2004, pp.59-71, 2004.
DOI : 10.1007/978-3-540-27836-8_8
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.154.6188

A. Abel and R. Matthes, Fixed Points of Type Constructors and Primitive Recursion, CSL 2004, pp.190-204, 2004.
DOI : 10.1007/978-3-540-30124-0_17
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.67.3989

A. Abel, R. Matthes, and T. Uustalu, Iteration and coiteration schemes for higher-order and nested datatypes, Theoretical Computer Science, vol.333, issue.1-2, pp.3-66, 2005.
DOI : 10.1016/j.tcs.2004.10.017
URL : http://doi.org/10.1016/j.tcs.2004.10.017

N. Benton, C. Hur, A. Kennedy, and C. Mcbride, Strongly Typed Term Representations in Coq, Journal of Automated Reasoning, vol.14, issue.1, pp.141-159, 2012.
DOI : 10.1145/604131.604150
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.174.7638

S. Berghofer and M. Wenzel, Inductive Datatypes in HOL ??? Lessons Learned in Formal-Logic Engineering, TPHOLs '99, pp.19-36, 1999.
DOI : 10.1007/3-540-48256-3_3
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.7659

J. Biendarra, Functor-Preserving Type Definitions in Isabelle, 2015.

R. S. Bird and R. Paterson, de Bruijn notation as a nested datatype, Journal of Functional Programming, vol.9, issue.1, pp.77-91, 1999.
DOI : 10.1017/S0956796899003366

R. S. Bird and R. Paterson, Generalised folds for nested datatypes, Formal Aspects of Computing, vol.11, issue.2, pp.200-222, 1999.
DOI : 10.1007/s001650050047
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.42.1517

J. C. Blanchette, J. Hölzl, A. Lochbihler, L. Panny, A. Popescu et al., Truly modular (co)datatypes for Isabelle/HOL Formalization and implementation accompanying this paper, ITP 2014, pp.93-110, 2014.
DOI : 10.1007/978-3-319-08970-6_7

J. C. Blanchette, F. Meier, A. Popescu, and D. Traytel, Foundational nonuniform (co)datatypes for higher-order logic (report), 2017.
DOI : 10.1109/lics.2017.8005071

J. C. Blanchette, A. Popescu, and D. Traytel, Foundational extensible corecursion, ICFP 2015, pp.192-204, 2015.
DOI : 10.1145/2858949.2784732
URL : https://hal.archives-ouvertes.fr/hal-01212589

J. C. Blanchette, A. Popescu, and D. Traytel, Witnessing (Co)datatypes, ESOP 2015, pp.359-382, 2015.
DOI : 10.1007/978-3-662-46669-8_15
URL : https://hal.archives-ouvertes.fr/hal-01212587

A. Church, A formulation of the simple theory of types, The Journal of Symbolic Logic, vol.1, issue.02, pp.56-68, 1940.
DOI : 10.2307/2371199

N. A. Danielsson, Lightweight semiformal time complexity analysis for purely functional data structures, POPL 2008, pp.133-144, 2008.
DOI : 10.1145/1328897.1328457

N. Ghani, M. Hamana, T. Uustalu, and V. Vene, Representing cyclic structures as nested datatypes, TFP 2006 of Trends in Functional Programming, pp.173-188, 2006.

N. Ghani, P. Johann, and C. Fumex, Generic Fibrational Induction, Logical Methods in Computer Science, vol.8, issue.2, p.2012
DOI : 10.2168/LMCS-8(2:12)2012
URL : http://arxiv.org/pdf/1206.0357

M. J. Gordon and T. F. Melham, Introduction to HOL: A Theorem Proving Environment for Higher Order Logic, 1993.

E. L. Gunter, A broader class of trees for recursive type definitions for HOL, HUG '93, pp.141-154, 1994.
DOI : 10.1007/3-540-57826-9_131

J. Harrison, Inductive definitions: Automation and application, TPHOLs '95, pp.200-213, 1995.
DOI : 10.1007/3-540-60275-5_66

F. Henglein, Type inference with polymorphic recursion, ACM Transactions on Programming Languages and Systems, vol.15, issue.2, pp.253-289, 1993.
DOI : 10.1145/169701.169692
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.388.430

C. Hermida and B. Jacobs, Structural Induction and Coinduction in a Fibrational Setting, Information and Computation, vol.145, issue.2, pp.107-152, 1998.
DOI : 10.1006/inco.1998.2725
URL : http://doi.org/10.1006/inco.1998.2725

R. Hinze, Efficient generalized folds The proceedings appeared as a technical report of, Workshop on Generic Programming, pp.1-16, 2000.

R. Hinze and R. Paterson, Finger trees: a simple general-purpose data structure, Journal of Functional Programming, vol.16, issue.02, pp.197-217, 2006.
DOI : 10.1017/S0956796805005769

A. Hirschowitz and M. Maggesi, Nested Abstract Syntax in Coq, Journal of Automated Reasoning, vol.19, issue.3&4, pp.409-426, 2012.
DOI : 10.1145/1190216.1190245
URL : https://hal.archives-ouvertes.fr/hal-01294214

B. Huffman and O. Kun?ar, Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL, CPP 2013, pp.131-146, 2013.
DOI : 10.1007/978-3-319-03545-1_9

C. E. Martin, J. Gibbons, and I. Bayley, Disciplined, efficient, generalised folds for nested datatypes, Formal Aspects of Computing, vol.16, issue.1, pp.19-35, 2004.
DOI : 10.1007/s00165-003-0013-6
URL : http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.159.1577&rep=rep1&type=pdf

R. Matthes, Recursion on Nested Datatypes in Dependent Type Theory, LNCS, vol.5028, pp.431-446, 2008.
DOI : 10.1007/978-3-540-69407-6_47
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.598.8368

R. Matthes, An induction principle for nested datatypes in intensional type theory, Journal of Functional Programming, vol.19, issue.3-4, pp.439-468, 2009.
DOI : 10.2307/2586554

T. F. Melham, Automating Recursive Type Definitions in Higher Order Logic, Current Trends in Hardware Verification and Automated Theorem Proving, pp.341-386, 1989.
DOI : 10.1007/978-1-4612-3658-0_9
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.302.392

A. Mycroft, Polymorphic type schemes and recursive definitions, Symposium on Programming, pp.217-228, 1984.
DOI : 10.1007/3-540-12925-1_41

G. Naves and A. Spiwack, Balancing Lists: A Proof Pearl, ITP 2014, pp.437-449, 2014.
DOI : 10.1007/978-3-319-08970-6_28
URL : https://hal.archives-ouvertes.fr/hal-01097937

B. Nordhoff, S. Körner, and P. Lammich, Finger trees, Archive of Formal Proofs, 2010.

C. Okasaki, Purely functional data structures, 1999.
DOI : 10.1017/CBO9780511530104

L. C. Paulson, A formulation of the simple theory of types

J. C. Reynolds, Types, abstraction and parametric polymorphism, IFIP '83, pp.513-523, 1983.

J. J. Rutten, Relators and Metric Bisimulations, Electronic Notes in Theoretical Computer Science, vol.11, pp.252-258, 1998.
DOI : 10.1016/S1571-0661(04)00063-5
URL : http://doi.org/10.1016/s1571-0661(04)00063-5

M. Sozeau, PROGRAM-ing finger trees in Coq, ICFP '07, pp.13-24, 2007.

D. Traytel, A. Popescu, and J. C. Blanchette, Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving, 2012 27th Annual IEEE Symposium on Logic in Computer Science, pp.596-605, 2012.
DOI : 10.1109/LICS.2012.75
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.221.844

P. Wadler, Theorems for free! In FPCA '89, pp.347-359, 1989.