On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics.

Patrick Cousot

Browse the full LOPSTR paper archive.