M. Abbott, T. Altenkirch, and N. Ghani, Categories of containers, Proceedings of FOSSACS 2003, number 2620 in Lecture Notes in Computer Science, pp.23-38, 2003.

A. Abel, S. Adelsberger, and A. Setzer, , 2016.

A. Abel, S. Adelsberger, and A. Setzer, Interactive programming in Agda-Objects and graphical user interfaces, Journal of Functional Programming, vol.27, 2017.

T. Altenkirch, N. Danielsson, A. Löh, and N. Oury, ??: Dependent types without the sugar, Functional and Logic Programming, vol.6009, pp.40-55, 2010.

A. Wiki, Coinductive data types, 2011.

. Agda, The Agda Wiki, 2014.

T. A. Codata, Talk given at the TYPES Workshop in Jouy-en-Josas, 2004.

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

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development, Texts in Theoretical Computer Science. An EATCS Series, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

Y. Bertot, CoInduction in Coq, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00001174

H. Basold and H. Geuvers, Type theory based on dependent inductive and coinductive types, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, pp.327-336, 2016.

R. Cockett and T. Fukushima, About charity, Yellow Series Report, 1992.

T. Coquand, Infinite objects in type theory, Types for Proofs and Programs, vol.806, pp.62-78, 1994.

N. Anders-danielsson and T. Altenkirch, Subtyping, declaratively, Mathematics of Program Construction, vol.10, pp.100-118, 2010.

N. Anders-danielsson, , 2009.

W. Gasarch, A survey of recursive combinatorics, Handbook of Recursive Mathematics, vol.16, pp.80049-80058, 1998.

H. Geuvers, Inductive and coinductive types with iteration and recursion, formal proceedings of the 1992 workshop on Types for Proofs and Programs, pp.183-207, 1992.

E. Giménez, Codifying guarded definitions with recursive schemes, Types for Proofs and Programs, vol.996, pp.39-59, 1995.

C. E. Giménez, English: A calculus of infinite constructions and its application to the verification of communicating systems), 1996.

J. G. Granström, Reference and Computation in Intuitionistic Type Theory, 2008.

J. Greiner, Programming with inductive and co-inductive types, vol.37, 1992.

T. Hagino, A Categorical Programming Language, 1987.

T. Hagino, Codatatypes in ML. J. Symb. Comput, vol.8, issue.6, pp.80065-80068, 1989.

B. T. Howard, Inductive, coinductive, and pointed types, Proceedings of the first ACM SIGPLAN international conference on Functional programming, ICFP '96, pp.102-109, 1996.

P. Hancock and A. Setzer, Interactive programs in dependent type theory, CSL 2000, vol.1862, pp.317-331, 2000.

P. Hancock and A. Setzer, Interactive programs and weakly final coalgebras (extended version), Dependently typed programming, number 04381 in Dagstuhl Seminar Proceedings. Internationales Begegnungs-und Forschungszentrum (IBFI), 2004.

P. Hancock and A. Setzer, Interactive programs and weakly final coalgebras in dependent type theory, From Sets and Types to Topology and Analysis. Towards Practicable Foundations for Constructive Mathematics, pp.115-134, 2005.

. Inria, The Coq Proof Assistant Reference Manual. INRIA, version 8

B. Igried and A. Setzer, Programming with monadic CSP-style processes in dependent type theory, Proceedings of the 1st International Workshop on Type-Driven Development, pp.28-38, 2016.

B. Igried and A. Setzer, Trace and stable failures semantics for CSP-Agda, Proceedings of the First Workshop on Coalgebra, Horn Clause Logic Programming and Types, vol.258, pp.36-51, 2016.

B. Igried and A. Setzer, Accepted for publication in Postproceedings TYPES, vol.23, 2016.

B. Jacobs and J. Rutten, A tutorial on (co)algebras and (co)induction, EATCS Bulletin, vol.62, pp.62-222, 1997.

. Stephen-cole-kleene, A symmetric form of Gödel's theorem, Ind. Math, vol.12, pp.244-246, 1950.

C. Mcbride, Let's see how things unfold: Reconciling the infinite with the intensional, Proceedings of the 3rd international Conference on Algebra and Coalgebra in Computer Science, CALCO'09, pp.113-126, 2009.

P. Nax and . Mendler, Recursive types and type constraints in second-order lambda calculus, Proceedings of the Second Annual IEEE Symp. on Logic in Computer Science, LICS 1987, pp.30-36, 1987.

P. Nax and . Mendler, Inductive types and type constraints in the second-order lambda calculus, Annals of Pure and Applied Logic, vol.51, issue.1-2, pp.159-172, 1991.

U. Norell, Towards a practical programming language based on dependent type theory, 2007.

P. Odifreddi, Classical Recursion Theory, vol.125, pp.70011-70020, 1992.

N. Oury, Coinductive types and type preservation, 2008.

B. Rosser, Extensions of some theorems of Gödel and Church, The Journal of Symbolic Logic, vol.1, issue.3, pp.87-91, 1936.

J. Rutten, Universal coalgebra: a theory of systems, Theoretical Computer Science, vol.249, issue.1, pp.56-62, 2000.

A. Setzer, Coalgebras as types determined by their elimination rules, of Logic, Epistemology, and the Unity of Science, vol.27, pp.351-369, 2012.

A. Setzer, How to reason coinductively informally, Advances in Proof Theory, pp.377-408, 2016.

B. A. Trakhtenbrot, On recursive separability, Dokl. Acad. Nauk, vol.88, pp.953-956, 1953.

D. A. Turner, Elementary strong functional programming, Funtional Programming Languages in Education, vol.1022, pp.1-13, 1995.

D. A. Turner, Total functional programming, Journal of Universal Computer Science, vol.10, issue.7, pp.751-768, 2004.

V. Vene and T. Uustalu, Functional programming with apomorphisms (corecursion), Proceedings of the Estonian Academy of Sciences, vol.47, pp.147-161, 1998.