M. Abbott, T. Altenkirch, and N. Ghani, Containers: Constructing strictly positive types, Theoretical Computer Science, vol.342, issue.1, pp.3-27, 2005.
DOI : 10.1016/j.tcs.2005.06.002

URL : http://doi.org/10.1016/j.tcs.2005.06.002

A. Asperti, W. Ricciotti, C. S. Coen, and E. Tassi, The Matita Interactive Theorem Prover, CADE-23, pp.64-69, 2011.
DOI : 10.1007/3-540-48256-3_12

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

R. Atkey and C. Mcbride, Productive coprogramming with guarded recursion, pp.197-208, 2013.
DOI : 10.1145/2544174.2500597

Y. Bertot and P. Casteran, Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions, 2004.
DOI : 10.1007/978-3-662-07964-5

URL : https://hal.archives-ouvertes.fr/hal-00344237

J. C. Blanchette, J. Hölzl, A. Lochbihler, L. Panny, A. Popescu et al., Truly Modular (Co)datatypes for Isabelle/HOL, ITP 2014, pp.93-110, 2014.
DOI : 10.1007/978-3-319-08970-6_7

URL : http://eprints.mdx.ac.uk/15165/1/codat-impl.pdf

J. C. Blanchette, A. Popescu, and D. Traytel, Foundational extensible corecursion: a proof assistant perspective, pp.192-204, 2015.
DOI : 10.1145/2858949.2784732

URL : https://hal.archives-ouvertes.fr/hal-01212589

A. Bove, P. Dybjer, and U. Norell, A Brief Overview of Agda ??? A Functional Language with Dependent Types, TPHOLs 2009, pp.73-78, 2009.
DOI : 10.1007/978-3-540-87827-8_28

R. Clouston, A. Bizjak, H. B. Grathwohl, and L. Birkedal, Programming and Reasoning with Guarded Recursion for Coinductive Types, FoSSaCS 2015, pp.407-421, 2015.
DOI : 10.1007/978-3-662-46678-0_26

URL : http://arxiv.org/abs/1501.02925

E. Giménez, An application of co-inductive types in Coq: Verification of the alternating bit protocol, TYPES '95, pp.135-152, 1996.
DOI : 10.1007/3-540-61780-9_67

J. Harrison, HOL Light: A tutorial introduction, FMCAD '96, pp.265-269, 1996.
DOI : 10.1007/BFb0031814

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

A. Krauss, Partial Recursive Functions in Higher-Order Logic, IJCAR 2006, pp.589-603, 2006.
DOI : 10.1007/11814771_48

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

T. Nipkow and G. Klein, Concrete Semantics, 2014.
DOI : 10.1007/978-3-319-10542-0

T. Nipkow, L. C. Paulson, and M. Wenzel, Isabelle/HOL: A Proof Assistant for Higher-Order Logic, 2002.
DOI : 10.1007/3-540-45949-9

J. J. Rutten, Universal coalgebra: a theory of systems, Theoretical Computer Science, vol.249, issue.1, pp.3-80, 2000.
DOI : 10.1016/S0304-3975(00)00056-6

K. Slind and M. Norrish, A Brief Overview of HOL4, TPHOLs 2008, pp.28-32, 2008.
DOI : 10.1007/s00165-007-0028-5

D. Traytel, [Agda] Agda's copatterns incompatible with initial algebras (2014), archived at https

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=

D. A. Turner, Elementary strong functional programming, FPLE '95, pp.1-13, 1995.
DOI : 10.1007/3-540-60675-0_35

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=