Programming with Bunched Implications

Abstract

We give an operational semantics for the logic programming language BLP, based on the hereditary Harrop fragment of the logic of bunched implications, BI. We introduce BI, explaining the account of the sharing of resources built into its semantics, and indicate how it may be used to give a logic programming language. We explain that the basic input/output model of operational semantics, used in linear logic programming, will not work for bunched logic. We show how to obtain a complete, goal-directed proof theory for hereditary Harrop BI and how to reformulate the operational model to account for the interaction between multiplicative and additive structure. We give examples of how the resulting programming language handles sharing and non-sharing use of resources purely logically and contrast them with Prolog. We describe the use of modules and their applications and discuss the possibilities offered in this context by multiplicative quanti ers. We provide a denotational semantics based on the construction of a least xed point of Herbrand interpretations. Finally we provide an annotated implementation of the operational semantics using the continuation-passing style (CPS).