Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, EpiSciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Conference papers

From Bunches to Labels and Back in BI Logic

Didier Galmiche 1 Michel Marti 1 Daniel Méry 1 
1 TYPES - Logic, Proof Theory and Programming
LORIA - FM - Department of Formal Methods
Abstract : In this work we study proof translations in BI logic. In this context we first define a labelled sequent calculus, called GBI, in which labels and constraints reflect the Kripke monoidal resource semantics (KRM) of BI, with total (and not partial) composition of resources and explicit inconsistent resources. After proving the soundness of GBI w.r.t. KRM structures, we show how to translate any LBI-proof (proof of the LBI sequent calculus) into GBI-proof. We also consider the problem of translating GBI-proofs back into LBI-proofs. Noticing that every LBI-translated GBI-proof enjoys a tree-like property on the structure of labels, We show that any GBI-proof that preserves this tree-like property can systematically be translated into an LBI-proof.
Document type :
Conference papers
Complete list of metadata
Contributor : Didier GALMICHE Connect in order to contact the contributor
Submitted on : Tuesday, November 3, 2020 - 11:52:53 AM
Last modification on : Monday, February 7, 2022 - 10:04:06 AM


  • HAL Id : hal-02986801, version 1



Didier Galmiche, Michel Marti, Daniel Méry. From Bunches to Labels and Back in BI Logic. Int. Workshop Syntax meets Semantics, SYSMICS 2019, 2019, Amsterdam, Netherlands. ⟨hal-02986801⟩



Record views