### 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.

### License

BSD License

### Topics

- Computer science/Programming languages/Logics

### Session Ribbon_Proofs

- More_Finite_Map
- JHelper
- Proofchain
- Ribbons_Basic
- Ribbons_Interfaces
- Ribbons_Stratified
- Ribbons_Graphical
- Ribbons_Graphical_Soundness

## Cite

×

Ribbon_Proofs-AFP

    @article{Ribbon_Proofs-AFP,
      author  = {John Wickerson},
      title   = {Ribbon Proofs},
      journal = {Archive of Formal Proofs},
      month   = {January},
      year    = {2013},
      note    = {\url{https://isa-afp.org/entries/Ribbon_Proofs.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Mar 2, 2013 : Isabelle2013
- Feb 16, 2013 : Isabelle2013