Aarhus University Seal / Aarhus Universitets segl

Charge! A framework for higher-order separation logic in Coq

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

  • Jesper Bengtson, IT University of Copenhagen, Unknown
  • Jonas Braband Jensen, IT University of Copenhagen, Denmark
  • Lars Birkedal
We present a comprehensive set of tactics for working with a shallow embedding of a higher-order separation logic for a subset of Java in Coq. The tactics make it possible to reason at a level of abstraction similar to pen-and-paper separation-logic proof outlines. In particular, the tactics allow the user to reason in the embedded logic rather than in the concrete model, where the stacks and heaps are exposed. The development is generic in the choice of heap model, and most of the development is also independent of the choice of programming language.
Original languageEnglish
Title of host publicationInteractive Theorem Proving : Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings
EditorsLennart Beringer, Amy Felty
Number of pages17
PublisherSpringer VS
Publication year5 Sep 2012
ISBN (print)9783642323461
ISBN (Electronic)978-3-642-32347-8
Publication statusPublished - 5 Sep 2012
Externally publishedYes
EventInternational Conference onInteractive Theorem Proving - Princeton, United States
Duration: 13 Aug 201215 Aug 2012
Conference number: 3


ConferenceInternational Conference onInteractive Theorem Proving
LandUnited States
SeriesLecture Notes in Computer Science

See relations at Aarhus University Citationformats

ID: 81387626