Skip to Main content Skip to Navigation
Conference papers

An adequate compositional encoding of bigraph structure in linear logic with subexponentials

Kaustuv Chaudhuri 1 Giselle Reis 1
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : In linear logic, formulas can be split into two sets: classical (those that can be used as many times as necessary) or linear (those that are consumed and no longer available after being used). Subexponentials generalize this notion by allowing the formulas to be split into many sets, each of which can then be specified to be classical or linear. This flexibility increases its expressiveness: we already have adequate encodings of a number of other proof systems, and for computational models such as concurrent constraint programming, in linear logic with subexponentials (SEL). Bigraphs were proposed by Milner in 2001 as a model for ubiquitous computing, subsuming models of computation such as CCS and the π-calculus and capable of modeling connectivity and locality at the same time. In this work we present an encoding of the bigraph structure in SEL, thus giving an indication of the expressive power of this logic, and at the same time providing a framework for reasoning and operating on bigraphs. Our encoding is adequate and therefore the operations of composition and juxtaposition can be performed on the logical level. Moreover, all the proof-theoretical tools of SEL become available for querying and proving properties of bigraph structures.
Complete list of metadata

Cited literature [14 references]  Display  Hide  Download
Contributor : Giselle Reis <>
Submitted on : Friday, October 2, 2015 - 2:38:20 PM
Last modification on : Friday, April 30, 2021 - 10:02:41 AM
Long-term archiving on: : Sunday, January 3, 2016 - 10:45:31 AM


Files produced by the author(s)




Kaustuv Chaudhuri, Giselle Reis. An adequate compositional encoding of bigraph structure in linear logic with subexponentials. 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Nov 2015, Suva, Fiji. pp.146--161, ⟨10.1007/978-3-662-48899-7_11⟩. ⟨hal-01208362⟩



Record views


Files downloads