HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Resource Models and Proofs in Bunched Implications Logic

Didier Galmiche 1
1 TYPES - Logic, proof Theory and Programming
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : In this talk, we present, after an analysis of the BI models, a theory of semantic proof-search for BI, that is based on the use of algebras of labels in order to solve the resource-distribution and sharing problems. Therefore, we deduce methods that generate proofs or countermodels in BI. As consequences, we have two strong results for propositional BI: decidability and finite model property, and we also propose, a new resource semantics, based on partially defined monoids, which generalizes the semantics of BI's pointer logic and for which BI is complete. We analyse the consequences of these proof-theoretic and semantics results about BI in the context of separation and spatial logics (specifications and proofs of programs or distributed concurrent systems).
Document type :
Conference papers
Complete list of metadata

Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 9:38:32 AM
Last modification on : Friday, February 26, 2021 - 3:28:08 PM


  • HAL Id : inria-00099552, version 1



Didier Galmiche. Resource Models and Proofs in Bunched Implications Logic. First APPSEM-II Workshop 2003 - (Applied Semantics II), 2003, Nottingham/UK. ⟨inria-00099552⟩



Record views