[isabelle] AFP 2013 released
- To: isabelle-users Mailinglist <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] AFP 2013 released
- From: Gerwin Klein <Gerwin.Klein at nicta.com.au>
- Date: Sat, 16 Feb 2013 09:29:36 +0000
- Accept-language: en-AU, en-US
- Thread-index: AQHODCgjBNEXZ3lifEWRqff9+BmhEQ==
- Thread-topic: AFP 2013 released
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:
by Mizuhito Ogawa and Christian Sternagel (submitted 2012-11-02)
A proof of the open induction schema based on J.-C. Raoult, Proving
open properties by induction, Information Processing Letters 29,
by John Wickerson (submitted 2013-01-19)
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.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and