Dynamic Logic of Common Knowledge in a Proof Assistant - Pierre Lescanne; Jérôme Puisségur (CoRR, 2007)