Propositional dynamic logic (PDL) is at the core of reasoning about dynamic systems. We present a syntax directed formalism for PDL, built on coproofs.

Contrary to proofs, which are generated inductively top-down, coproofs are generated coinductively bottom-up, and may have infinite branches. However, our inference rules allow this only via state-changes, and as a result are sound.

We also prove the semantic completeness of our formalism, and apply it to obtain new interpolation theorems for PDL.