Typechecking liveness properties of coprograms Clarification: in Total Functional Programming terminology, a program terminates with useful input, while a coprogram doesn't necessarily terminates, and repeatedly produces useful input.

I am investigating the relationship between model checking and type theory. It is straightforward to encode safety properties in the type of a program. It seems like typing coprograms would be the best way to check liveness properties, but where is the literature on the subject? I can't find any papers about the general case.
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.