Projects per year
Abstract
Proof nets for MLL (unitfree multiplicative linear logic) and (unitfree additive linear logic) are graphical abstractions of proofs which are efficient (proofs translate in linear time) and canoni cal (invariant under rule commutation). This paper solves a three decade open problem: are there efficient canonical proof nets for MALL (unitfree multiplicativeadditive linear logic)?
Honouring MLL and ALL canonicity, in which all commutations are strictly local prooftree rewrites, we define local canonicity for MALL: invariance under local rule commutation. We present new proof nets for MALL, called conflict nets, which are both efficient and locally canonical.
Honouring MLL and ALL canonicity, in which all commutations are strictly local prooftree rewrites, we define local canonicity for MALL: invariance under local rule commutation. We present new proof nets for MALL, called conflict nets, which are both efficient and locally canonical.
Original language  English 

Title of host publication  Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2016 
Place of Publication  New York, U. S. A. 
Publisher  Association for Computing Machinery 
Pages  437446 
Number of pages  10 
ISBN (Print)  9781450343916 
DOIs  
Publication status  Published  2 Jul 2016 
Event  31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2016  New York, USA United States Duration: 5 Jul 2016 → 8 Jul 2016 
Publication series
Name  Proceedings  Symposium on Logic in Computer Science 

Publisher  IEEE 
ISSN (Electronic)  25755528 
Conference
Conference  31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2016 

Country/Territory  USA United States 
City  New York 
Period  5/07/16 → 8/07/16 
Fingerprint
Dive into the research topics of 'Conflict nets: efficient locally canonical MALL proof nets'. Together they form a unique fingerprint.Projects
 2 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

COMPLEXITY AND NONDETERMINISM IN DEEP INFERENCE
Engineering and Physical Sciences Research Council
1/02/07 → 30/06/08
Project: Research council