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.