Email Gateway (Aug 19 2022 at 10:12): Email Gateway (Aug 19 2022 at 10:12):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
The entries in the Archive of Formal proofs are now available for Isabelle2013 at [http://afp.sf.net].
The following new entries are available from the front page:
Open Induction
by Mizuhito Ogawa and Christian Sternagel (submitted 2012-11-02)
[http://afp.sourceforge.net/entries/Open_Induction.shtml]
Abstract:
A proof of the open induction schema based on J.-C. Raoult, Proving
open properties by induction, Information Processing Letters 29,
1988, pp.19-23.
Ribbon Proofs
by John Wickerson (submitted 2013-01-19)
[http://afp.sourceforge.net/entries/Ribbon_Proofs.shtml]
Abstract:
This document concerns the theory of ribbon proofs: a diagrammatic
proof system, based on separation logic, for verifying program
correctness. We include the syntax, proof rules, and soundness
results for two alternative formalisations of ribbon proofs.
Compared to traditional proof outlines, ribbon proofs emphasise the
structure of a proof, so are intelligible and pedagogical. Because
they contain less redundancy than proof outlines, and allow each
proof step to be checked locally, they may be more scalable. Where
proof outlines are cumbersome to modify, ribbon proofs can be visually
manoeuvred to yield proofs of variant programs.
Cheers,
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Last updated: Apr 25 2024 at 16:19 UTC