## Abstract

We formalize higher-order separation logic for a first-order imperative language with procedures and local variables in Isabelle/HOLCF. The assertion language is modeled in such a way that one may use any theory defined in Isabelle/HOLCF to construct assertions, e.g., primitive recursion, least or greatest fixed points etc. The higher-order logic ensures that we can show non-trivial algorithms correct without having to extend the semantics of the language as was done previously in verifications based on first-order separation logic [2,20]. We provide non-trivial examples to support this claim and to show how the higher-order logic enables natural assertions in specifications. To support abstract reasoning we have implemented rules for representation hiding and data abstraction as seen in [1].

The logic is represented as lemmas for reasoning about the denotational semantics of the programming language. This follows the definitional approach common in HOL theorem provers, i.e., the soundness of our model only relies on the soundness of Isabelle/HOL [6]. We use our formalization to give a formally verified proof of Cheney's copying garbage collector [4] using a tagged representation of objects. The proof generalizes the results in [2]. The proof uses an encoding of the separation logic formula this(h) to capture the heap from before the garbage collection and thus shows

another novel use of higher-order separation logic.

The logic is represented as lemmas for reasoning about the denotational semantics of the programming language. This follows the definitional approach common in HOL theorem provers, i.e., the soundness of our model only relies on the soundness of Isabelle/HOL [6]. We use our formalization to give a formally verified proof of Cheney's copying garbage collector [4] using a tagged representation of objects. The proof generalizes the results in [2]. The proof uses an encoding of the separation logic formula this(h) to capture the heap from before the garbage collection and thus shows

another novel use of higher-order separation logic.

Originalsprog | Engelsk |
---|---|

Tidsskrift | Electronical Notes in Theoretical Computer Science |

Sider (fra-til) | 371-389 |

Antal sider | 18 |

ISSN | 1571-0661 |

DOI | |

Status | Udgivet - 2008 |

Begivenhed | Mathematical Foundations of Programming Semantics - University of Pennsylvania, USA Varighed: 22 maj 2008 → 25 maj 2008 Konferencens nummer: 24 |

### Konference

Konference | Mathematical Foundations of Programming Semantics |
---|---|

Nummer | 24 |

Land/Område | USA |

By | University of Pennsylvania |

Periode | 22/05/2008 → 25/05/2008 |

## Emneord

- Higher-Order Separation Logic
- First-Order Imperative Language
- Denotational Semantics
- Isabelle/HOLCF
- Cheney's Copying Garbage Collector