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

Patrick Cousot

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

2020

Patrick Cousot

We study partial and total correctness proof methods based on generalized fixpoint/iteration/variant induction principles applied to the denotational semantics of first-order functional and iterative programs.

Keywords:

Programming language
Denotational semantics
Correctness
Fixed point
Computer science
Theoretical computer science
correctness proofs

Correction
Source
Cite
Save
Machine Reading By IdeaReader

References

Citations