## Abstract

When using a proof assistant to reason in an embedded logic -- like separation logic -- one cannot benefit from the proof contexts and basic tactics of the proof assistant. This results in proofs that are at a too low level of abstraction because they are cluttered with bookkeeping code related to manipulating the object logic.

In this paper, we introduce a so-called proof mode that extends the Coq proof assistant with (spatial and non-spatial) named proof contexts for the object logic. We show that thanks to these contexts we can implement high-level tactics for introduction and elimination of the connectives of the object logic, and thereby make reasoning in the embedded logic as seamless as reasoning in the meta logic of the proof assistant. We apply our method to Iris: a state of the art higher-order impredicative concurrent separation logic.

We show that our method is very general, and is not just limited to program verification. We demonstrate its generality by formalizing correctness proofs of fine-grained concurrent algorithms, derived constructs of the Iris logic, and a unary and binary logical relation for a language with concurrency, higher-order store, polymorphism, and recursive types. This is the first formalization of a binary logical relation for such an expressive language. We also show how to use the logical relation to prove contextual refinement of fine-grained concurrent algorithms.

In this paper, we introduce a so-called proof mode that extends the Coq proof assistant with (spatial and non-spatial) named proof contexts for the object logic. We show that thanks to these contexts we can implement high-level tactics for introduction and elimination of the connectives of the object logic, and thereby make reasoning in the embedded logic as seamless as reasoning in the meta logic of the proof assistant. We apply our method to Iris: a state of the art higher-order impredicative concurrent separation logic.

We show that our method is very general, and is not just limited to program verification. We demonstrate its generality by formalizing correctness proofs of fine-grained concurrent algorithms, derived constructs of the Iris logic, and a unary and binary logical relation for a language with concurrency, higher-order store, polymorphism, and recursive types. This is the first formalization of a binary logical relation for such an expressive language. We also show how to use the logical relation to prove contextual refinement of fine-grained concurrent algorithms.

Original language | English |
---|---|

Title of host publication | POPL 2017 Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages |

Place of Publication | New York |

Publisher | Association for Computing Machinery (ACM) |

Pages | 205-217 |

Number of pages | 13 |

ISBN (Electronic) | 978-1-4503-4660-3 |

DOIs | |

Publication status | Published - 2017 |

Event | POPL 2017: The 44th ACM SIGPLAN Symposium on Principles of Programming Languages - Paris, France Duration: 15 Jan 2017 → 21 Jan 2017 |

### Publication series

Name | ACM SIGPLAN Notices |
---|---|

Publisher | ACM |

Number | 1 |

Volume | 52 |

ISSN (Print) | 0362-1340 |

ISSN (Electronic) | 1558-1160 |

### Conference

Conference | POPL 2017 |
---|---|

Country | France |

City | Paris |

Period | 15/01/17 → 21/01/17 |

## Keywords

- Separation logic
- Interactive theorem Proving
- Coq
- Fine-grained concurrency
- Logical Relations