[isabelle] New entry "Abstract Hoare Logics" in AFP



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






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.