Projects per year
Abstract
We investigate efficient algorithms for the additive fragment of linear logic. This logic is an internal language for categories with finite sums and products, and describes concurrent twoplayer games of finite choice. In the context of session types, typing disciplines for communication along channels, the logic describes the communication of finite choice along a single channel. We give a simple linear time correctness criterion for unitfree propositional additive proof nets via a natural construction on Petri nets. This is an essential ingredient to linear time complexity of the second author's combinatorial proofs for classical logic. For full propositional additive linear logic, including the units, we give a proof search algorithm that is lineartime in the product of the source and target formula, and an algorithm for proof net correctness that is of the same time complexity. We prove that proof search in firstorder additive linear logic is NPcomplete.
Original language  English 

Title of host publication  Proceedings of the 30th ACM/IEEE Symposium on Logic in Computer Science (LICS), 2015 
Publisher  IEEE 
Pages  8091 
Number of pages  12 
ISBN (Print)  9781479988754 
DOIs  
Publication status  Published  10 Jul 2015 
Event  30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2015  Kyoto, Japan Duration: 6 Jul 2015 → 10 Jul 2015 
Publication series
Name  2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science 

Publisher  IEEE 
ISSN (Electronic)  10436871 
Conference
Conference  30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2015 

Country  Japan 
City  Kyoto 
Period  6/07/15 → 10/07/15 
Fingerprint Dive into the research topics of 'Complexity bounds for sumproduct logic via additive proof nets and Petri nets'. Together they form a unique fingerprint.
Projects
 1 Finished

Efficient and Natural Proof Systems
Guglielmi, A., Bruscoli, P. & McCusker, G.
Engineering and Physical Sciences Research Council
1/02/13 → 12/05/16
Project: Research council