Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
422136 | Electronic Notes in Theoretical Computer Science | 2008 | 13 Pages |
Abstract
We study conditions for a concurrent construction of proof-nets in the framework of linear logic following Andreoli's works. We define specific correctness criteria for that purpose. We first study the multiplicative case and show how the correctness criterion given by Danos and decidable in linear time, may be extended to closed modules (i.e. validity of polarized proof structures). We then study the exponential case and give a correctness criterion by means of a contraction relation that helps to discover frontiers of exponential boxes.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics