Completeness and decidability of converse PDL in the constructive type theory of Coq.

Christian Doczkal, Joachim Bard

Browse the full CPP paper archive.