Okay so to actually answer the thread title — yes, people are doing this, but it's weirdly siloed. The bisimulation / process calculi crowd has been doing coinduction forever for proving behavioral equivalences, but the program analysis crowd seems to have mostly stuck to inductive lattice-based approaches (hello Cousot & Cousot, we love you).

The interesting thing is that coinduction gives you the greatest fixpoint whereas Tarski-style abstract interpretation usually targets the least fixpoint. For liveness-style properties this is actually what you want — you're asserting something holds forever, not just eventually.

There's a great Springer paper: "Program Verification by Coinduction" that implements exactly this in Coq. No intermediate program logics needed — it takes an operational semantics directly as input.

This is true and I feel like the disconnect is cultural as much as technical. PL theory seminars rarely cover bisimulation in depth unless you're specifically in the concurrency track. And abstract interpretation people sometimes treat coinduction like some exotic category theory thing when really it's just gfp = cofixpoint, same lattice machinery.

Also: coinductive big-step operational semantics (Leroy, 2006) is criminally underrated for this. You can describe diverging evaluations alongside terminating ones without hacks like adding a ⊥ element everywhere. The whole thing falls out naturally from the coinductive structure.

Relevant: coinductive big-step semantics reading list I put together last month.

Has anyone actually tried using coinductive logic programming (co-LP) for a real type analysis? There's a ResearchGate paper on using it for precise static type analysis of OO languages — the idea is you translate source to a logic program and then type-checking becomes a query. The coinductive semantics handles infinite terms from recursive types without exploding.

I tried this for a toy language last semester and the main pain point is the "guardedness condition" — your corecursive functions have to be productive, i.e., always make observable progress. Coq is very strict about this and it can be annoying when you want to write what feels like a natural recursive analysis pass.

The guardedness checker is essentially asking: "does every corecursive call happen under a constructor?" Which makes sense for productivity but is frustrating when you're writing analyses that feel more naturally expressed without that constraint.

I feel this so deeply. Sized types are supposed to help here — instead of a syntactic guardedness check you get an ordinal-indexed type system that can track productivity more flexibly. Agda has sized types, Coq's situation is more complicated.

For program analysis specifically I wonder if the "clocks and comonads" approach from Atkey & McBride would be relevant — temporal type theory basically internalizes the productivity requirement into the types themselves so you can reason about it more compositionally. It's more overhead conceptually but you get the coinductive structure for free.

Also @monad_catgirl do you have your toy language implementation anywhere? I'd genuinely love to look at how you encoded the type analysis coinductively, even if it was just exploratory.

To synthesize a bit before more replies come in:

Things we agree on so far:

1. Coinduction is the right framework for liveness/safety over potentially non-terminating programs — you want νF, not μF.
2. The biggest practical barrier is tooling — most analysis frameworks assume finiteness somewhere.
3. Coinductive big-step semantics is underused and more people should know about it.
4. The guardedness problem is real but sized types / clocked types are promising mitigations.

Open questions:

— Is there a practical coinductive abstract interpreter someone has actually deployed on real code, or is this all still theoretical?
— How does this interact with widening operators? Widening is usually justified for lfp convergence acceleration — does it even make sense in a gfp context?
— Anyone know of work connecting coinductive analysis to separation logic for heap reasoning?

🌸 Good thread everyone. Please keep it going!