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

A. Abel, Termination checking with types, RAIRO - Theoretical Informatics and Applications, vol.38, issue.4, pp.277-319, 2004.
DOI : 10.1051/ita:2004015

A. Abel, MiniAgda: Integrating Sized and Dependent Types, Electronic Proceedings in Theoretical Computer Science, vol.43, pp.14-28, 2010.
DOI : 10.4204/EPTCS.43.2

A. Abel, Re: [Coq-Club] Propositional extensionality is inconsistent in Coq Archived at https://sympa.inria.fr/sympa, pp.2013-2025, 2013.

A. Abel and B. Pientka, Wellfounded recursion with copatterns: A unified approach to termination and productivity, pp.185-196, 2013.

A. Abel, B. Pientka, D. Thibodeau, and A. Setzer, Copatterns: Programming infinite structures by observations, pp.27-38, 2013.

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

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

F. Bartels, Generalised coinduction, Mathematical Structures in Computer Science, vol.13, issue.2, pp.321-348, 2003.
DOI : 10.1017/S0960129502003900
URL : http://doi.org/10.1016/s1571-0661(04)80903-4

F. Bartels, On Generalised Coinduction and Probabilistic Specification Formats: Distributive Laws in Coalgebraic Modelling, 2004.

N. Benton, The Proof Assistant as an Integrated Development Environment, APLAS 2013, pp.307-314, 2013.
DOI : 10.1007/978-3-319-03542-0_22

J. Bernardy, P. Jansson, and R. Paterson, Proofs for free, Journal of Functional Programming, vol.83, issue.02, pp.107-152, 2012.
DOI : 10.1007/BFb0037116

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development?Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science, 2004.
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
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, Unified Classical Logic Completeness, IJCAR 2014, pp.46-60, 2014.
DOI : 10.1007/978-3-319-08587-6_4

J. C. Blanchette, A. Popescu, and D. Traytel, Formalization associated with this paper. https://github, 2015.

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

A. Cave, F. Ferreira, P. Panangaden, and B. Pientka, Fair reactive programming, Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, pp.361-372, 2014.
DOI : 10.1145/2535838.2535881
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.405.856

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

J. Crow, S. Owre, J. Rushby, N. Shankar, and M. Srivas, A tutorial introduction to PVS, 1995.

M. Dénès, [Coq-Club] Propositional extensionality is inconsistent in Coq Archived at https://sympa.inria.fr/sympa, pp.2013-2025, 2013.

P. , D. Gianantonio, and M. Miculan, A unifying approach to recursive and co-recursive definitions, TYPES 2002, pp.148-161, 2003.

C. Elliott and P. Hudak, Functional reactive animation, ICFP '97, pp.263-273, 1997.
DOI : 10.1145/258948.258973
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.17.7696

J. Endrullis, D. Hendriks, and M. Bodin, Circular Coinduction in Coq Using Bisimulation-Up-To Techniques, ITP 2013, pp.354-369, 2013.
DOI : 10.1007/978-3-642-39634-2_26

U. Hensel and B. Jacobs, Proof principles for datatypes with iterated recursion, CTCS '97, pp.220-241, 1997.
DOI : 10.1007/BFb0026991

J. Heras, E. Komendantskaya, and M. Schmidt, (Co)recursion in logic programming: Lazy vs eager, Theor. Pract. Log. Prog, vol.14, pp.4-5

R. Hinze, Concrete stream calculus: An extended study, Journal of Functional Programming, vol.66, issue.5-6, pp.463-535, 2010.
DOI : 10.1016/S0304-3975(97)00065-0

R. Hinze and D. W. James, Proving the unique fixed-point principle correct?An adventure with category theory, pp.359-371, 2011.

B. Huffman, A Purely Definitional Universal Domain, LNCS, vol.5, issue.3, pp.260-275, 2009.
DOI : 10.1145/1190315.1190324

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. Hur, G. Neis, D. Dreyer, and V. Vafeiadis, The power of parameterization in coinductive proof, POPL '13, pp.193-206, 2013.

B. Jacobs, Distributive laws for the coinductive solution of recursive equations, Information and Computation, vol.204, issue.4, pp.561-587, 2006.
DOI : 10.1016/j.ic.2005.03.006

C. Keller and M. Lasson, Parametricity in an impredicative sort, CSL 2012, pp.381-395, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00730913

B. Klin, Bialgebras for structural operational semantics: An introduction, Theoretical Computer Science, vol.412, issue.38, pp.5043-5069, 2011.
DOI : 10.1016/j.tcs.2011.03.023
URL : http://doi.org/10.1016/j.tcs.2011.03.023

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

N. R. Krishnaswami and N. Benton, Ultrametric Semantics of Reactive Programs, 2011 IEEE 26th Annual Symposium on Logic in Computer Science, pp.257-266, 2011.
DOI : 10.1109/LICS.2011.38

O. Kun?ar-for-isabelle and /. Hol, Correctness of Isabelle's cyclicity checker?Implementability of overloading in proof assistants, ITP 2015, pp.85-94, 2015.

K. R. Leino and M. Moskal, Co-induction simply?Automatic co-inductive proofs in a program verifier, LNCS, vol.8442, pp.382-398, 2014.

X. Leroy, A Formally Verified Compiler Back-end, Journal of Automated Reasoning, vol.27, issue.1, pp.363-446, 2009.
DOI : 10.1007/s10817-009-9155-4
URL : https://hal.archives-ouvertes.fr/inria-00360768

A. Lochbihler, Verifying a Compiler for Java Threads, LNCS, vol.6012, pp.427-447, 2010.
DOI : 10.1007/978-3-642-11957-6_23
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.496.8823

A. Lochbihler, Making the java memory model safe, ACM Transactions on Programming Languages and Systems, vol.35, issue.4, pp.1-65, 2014.
DOI : 10.1145/2518191

A. Lochbihler and J. Hölzl, Recursive Functions on Lazy Lists via Domains and Topologies, ITP 2014, pp.341-357, 2014.
DOI : 10.1007/978-3-319-08970-6_22

J. Matthews, Recursive Function Definition over Coinductive Types, TPHOLs '99, pp.73-90, 1999.
DOI : 10.1007/3-540-48256-3_6
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.23.2683

S. Milius, L. S. Moss, and D. Schwencke, Abstract GSOS Rules and a Modular Treatment of Recursive Definitions, Logical Methods in Computer Science, vol.9, issue.3, p.2013
DOI : 10.2168/LMCS-9(3:28)2013

L. S. Moss, Parametric corecursion, Theoretical Computer Science, vol.260, issue.1-2, pp.139-163, 2001.
DOI : 10.1016/S0304-3975(00)00126-2
URL : http://doi.org/10.1016/s0304-3975(00)00126-2

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

L. C. Paulson, Set theory for verification: I. From foundations to functions, Journal of Automated Reasoning, vol.8, issue.1, pp.353-389, 1993.
DOI : 10.1007/BF00881873

L. C. Paulson, Set theory for verification. II: Induction and recursion, Journal of Automated Reasoning, vol.11, issue.3, pp.167-215, 1995.
DOI : 10.1007/BF00881916

A. Popescu and E. L. Gunter, Incremental Pattern-Based Coinduction for Process Algebra and Its Isabelle Formalization, FoSSaCS 2010, pp.109-127, 2010.
DOI : 10.1007/978-3-642-12032-9_9

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

G. Ro¸suro¸su and D. Lucanu, Circular coinduction?A proof theoretical foundation, LNCS, vol.5728, pp.127-144, 2009.

J. Rot, M. M. Bonsangue, and J. J. Rutten, Coalgebraic Bisimulation-Up-To, SOFSEM 2013, pp.369-381, 2013.
DOI : 10.1007/978-3-642-35843-2_32

J. J. Rutten, Processes as terms: non-well-founded models for bisimulation, Mathematical Structures in Computer Science, vol.X, issue.03, pp.257-275, 1992.
DOI : 10.1016/S0019-9958(82)91250-5

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

J. J. Rutten, A coinductive calculus of streams, Mathematical Structures in Computer Science, vol.15, issue.1, pp.93-147, 2005.
DOI : 10.1017/S0960129504004517

D. Sangiorgi, On the bisimulation proof method, Mathematical Structures in Computer Science, vol.8, issue.5, pp.447-479, 1998.
DOI : 10.1017/S0960129598002527

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

D. Turi and G. Plotkin, Towards a mathematical operational semantics, Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science, pp.280-291, 1997.
DOI : 10.1109/LICS.1997.614955

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=10.1.1.106.8766

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