Email Gateway (Aug 18 2022 at 09:32): Email Gateway (Aug 18 2022 at 09:32):From: Tobias Nipkow <nipkow@in.tum.de>
The development branch of the Archive of Formal Proofs contains a new
entry:
Abstract Hoare Logics
Tobias Nipkow
These therories describe Hoare logics for a number of imperative
language constructs, from while-loops to mutually
recursive procedures. Both partial and total correctness are
treated. In particular a proof system for total correctness of
recursive procedures in the presence of unbounded nondeterminism is
presented.
These theories accompany earlier publications of mine:
@inproceedings{Nipkow-CSL02,author={Tobias Nipkow},
title={Hoare Logics for Recursive Procedures and Unbounded Nondeterminism},
booktitle={Computer Science Logic (CSL 2002)},editor={J. Bradfield},
publisher=Springer,series=LNCS,volume=2471,pages={103-119},year=2002}
@inproceedings{Nipkow-MOD2001,author={Tobias Nipkow},
title={Hoare Logics in {Isabelle/HOL}},
booktitle={Proof and System-Reliability},
editor={H. Schwichtenberg and R. Steinbr?ggen},
publisher={Kluwer},year=2002,pages={341-367}}
Enjoy,
Tobias
Last updated: May 03 2024 at 12:27 UTC