|
|
|
|
|
Bunched LogicBunched logic is a variety of substructural logic that, like linear logic, has classes of multiplicative and additive operators, but differs from usual proof calculi in having a tree-like context of hypotheses instead of a flat list-like structure; it is thus a calculus of deep inference. Sub-trees of the context tree are referred to as bunches; hence the name. The internal nodes in the context tree are labelled with the mode of composition — multiplicative or additive, with the following characteristics: - Multiplicative composition denies the structural rules of weakening and contraction.
- Additive composition admits weakening and contraction of entire bunches.
Bunched logic extended with a semantic model of locations and store is known as separation logic. It has been used to define the logic of pointer-analysis in languages like Algol or C. See also References
|
 |
|
| Copyright 2005-2009 OnPedia.com. All Rights Reserved |
|
|