| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
Separata: Isabelle tactics for Separation Algebra
| Title: | Separata: Isabelle tactics for Separation Algebra |
| Authors: | Zhe Hou (zhe /dot/ hou /at/ ntu /dot/ edu /dot/ sg), David Sanan (sanan /at/ ntu /dot/ edu /dot/ sg), Alwen Tiu (ATiu /at/ ntu /dot/ edu /dot/ sg), Rajeev Gore (rajeev /dot/ gore /at/ anu /dot/ edu /dot/ au) and Ranald Clouston (ranald /dot/ clouston /at/ cs /dot/ au /dot/ dk) |
| Submission date: | 2016-11-16 |
| Abstract: | We bring the labelled sequent calculus $LS_{PASL}$ for propositional abstract separation logic to Isabelle. The tactics given here are directly applied on an extension of the Separation Algebra in the AFP. In addition to the cancellative separation algebra, we further consider some useful properties in the heap model of separation logic, such as indivisible unit, disjointness, and cross-split. The tactics are essentially a proof search procedure for the calculus $LS_{PASL}$. We wrap the tactics in an Isabelle method called separata, and give a few examples of separation logic formulae which are provable by separata. |
| BibTeX: |
@article{Separata-AFP,
author = {Zhe Hou and David Sanan and Alwen Tiu and Rajeev Gore and Ranald Clouston},
title = {Separata: Isabelle tactics for Separation Algebra},
journal = {Archive of Formal Proofs},
month = nov,
year = 2016,
note = {\url{http://isa-afp.org/entries/Separata.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Depends on: | Separation_Algebra |
| Status: [ok] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |