A. Abel, Mixed Inductive/Coinductive Types and Strong Normalization, Programming Languages and Systems, 5th Asian Symposium, APLAS 2007 Proceedings. Lecture Notes in Computer Science, p.pp, 2007.
DOI : 10.1007/978-3-540-76637-7_19

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

A. Abel, Semi-continuous sized types and termination, Logical Methods in Computer Science, vol.42, issue.3, pp.1-33, 2008.
DOI : 10.2168/lmcs-4(2:3)2008

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

A. Abel, A. Abel, and T. Altenkirch, Type-based termination, inflationary fixed-points, and mixed inductive-coinductive types A predicative analysis of structural recursion, Proceedings of the 8th Workshop on Fixed Points in Computer Science Electronic Proceedings in Theoretical Computer Science, pp.1-11, 2002.

A. Abel and J. Chapman, Normalization by Evaluation in the Delay Monad: A Case Study for Coinduction via Copatterns and Sized Types, Proceedings 5th Workshop on Mathematically Structured Functional Programming, MSFP 2014 Electronic Proceedings in Theoretical Computer Science, pp.51-67, 2014.
DOI : 10.4204/EPTCS.153.4

A. Abel and B. Pientka, Wellfounded recursion with copatterns: A unified approach to termination and productivity, Proceedings of the Eighteenth ACM SIG- PLAN International Conference on Functional Programming, ICFP'13, pp.185-196, 2013.

R. M. Amadio, S. B. Coupet-grimal, and J. L. Sacchini, Analysis of a guard condition in type theory, First International Conference, FoSSaCS'98, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'98 Talk at the Journée " ´ egalité et terminaison " du 2 février 2010 in conjunction with JFLA 2010, pp.48-62, 1998.
DOI : 10.1007/BFb0053541

URL : https://hal.archives-ouvertes.fr/inria-00073388

G. Barthe, M. J. Frade, E. Giménez, L. Pinto, and T. Uustalu, Type-based termination of recursive definitions, Mathematical Structures in Computer Science, vol.14, issue.1, pp.97-141, 2004.
DOI : 10.1017/S0960129503004122

A. M. Ben-amram, Size-change termination with difference constraints, ACM Transactions on Programming Languages and Systems, vol.30, issue.3, 2008.
DOI : 10.1145/1353445.1353450

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

J. C. Blanchette, A. Popescu, and D. Traytel, Foundational extensible corecursion: a proof assistant perspective, Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, pp.192-204, 2015.
DOI : 10.1145/2858949.2784732

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

T. Coquand, Infinite objects in type theory, Lecture Notes in Computer Science, vol.806, pp.62-78, 1994.
DOI : 10.1007/3-540-58085-9_72

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

N. A. Danielsson and T. Altenkirch, Subtyping, Declaratively, 10th International Conference, pp.100-118, 2010.
DOI : 10.1007/978-3-642-13321-3_8

E. Giménez, Codifying guarded definitions with recursive schemes, Lecture Notes in Computer Science, vol.996, pp.39-59, 1994.
DOI : 10.1007/3-540-60579-7_3

J. Hughes, L. Pareto, A. Sabry, H. J. Boehm, and G. L. Jr, Proving the correctness of reactive systems using sized types, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '96, pp.410-423, 1996.
DOI : 10.1145/237721.240882

C. Hur, G. Neis, D. Dreyer, V. Vafeiadis, R. Giacobazzi et al., The power of parameterization in coinductive proof, The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'13, pp.193-206, 2013.

P. Hyvernat, The size-change termination principle for constructor based languages, Logical Methods in Computer Science, vol.10, issue.11, pp.11-2014, 2014.
URL : https://hal.archives-ouvertes.fr/hal-00547440

N. P. Mendler, P. Panangaden, and R. L. Constable, Infinite objects in type theory, Proceedings , Symposium on Logic in Computer Science, pp.16-18, 1986.

N. P. 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.
DOI : 10.1016/0168-0072(91)90069-X

URL : http://doi.org/10.1016/0168-0072(91)90069-x

K. Nakata and T. Uustalu, Resumptions, Weak Bisimilarity and Big-Step Semantics for While with Interactive I/O: An Exercise in Mixed Induction-Coinduction, Proceedings Seventh Workshop on Structural Operational Semantics Electronic Proceedings in Theoretical Computer Science, pp.57-75, 2010.
DOI : 10.4204/EPTCS.32.5

B. Nordström, K. Petersson, and J. M. Smith, Programming in Martin Löf's Type Theory: An Introduction, 1990.

C. Paulin-mohring, Inductive definitions in the system Coq rules and properties, Typed Lambda Calculi and Applications, International Conference on Typed Lambda Calculi and Applications, TLCA '93, pp.328-345, 1993.
DOI : 10.1007/BFb0037116

D. Pous and D. Sangiorgi, Enhancements of the bisimulation proof method Advanced Topics in Bisimulation and Coinduction, 2012.

J. Sacchini, Coq: Type-based termination in the Coq proof assistant (2015), project description

J. L. Sacchini, Type-Based Productivity of Stream Definitions in the Calculus of Constructions, 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science, pp.233-242, 2013.
DOI : 10.1109/LICS.2013.29

C. Sprenger and M. Dam, On the Structure of Inductive Reasoning: Circular and Tree-Shaped Proofs in the ??Calculus, FOSSACS 2003 Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2003, pp.425-4403, 2003.
DOI : 10.1007/3-540-36576-1_27