Typechecking liveness properties of coprograms
To expand on pedagand's answer: productivity is the term used for the computational dual (in some precise sense) of termination. Formally, a program f : CoData is productive if running the computation f eventually produces a constructor of CoData, and every (recursive) sub-term of that constructor is also productive.

For example

primes = filterBy prime [0..]


in haskell is productive, since there is an infinite number of prime numbers and so computing primes will always eventually produce a cons constructor.

There has been a number of works on using types to check for productivity of a given definition. One nice overview is Abel, Iteration and Coiteration Schemes for Higher-Order and Nested Datatypes from 2005.