loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
2008 23rd Annual IEEE Symposium on Logic in Computer Science
Cut Elimination for Monomial MALL Proof Nets
June 24-June 27
ISBN: 978-0-7695-3183-0
We present a syntax for MALL (multiplicative additive linear logic without units) proof nets which refines Girard's one. It is also based on the use of monomial weights for identifying additive components (slices). Our generalization gives the possibility of representing a kind of sharing of nodes which does not exist in Girard's nets. This sharing leads to the definition of a strong cut elimination procedure for MALL. We give a correctness criterion which is proved to be stable by reduction and to give a sequentialization theorem with respect to the sequent calculus. Sequentialization is proved by showing that an expansion procedure allows us to unfold any of our proof nets into a Girard proof net.
Index Terms:
Linear Logic, Proof Net, Cut Elimination
Citation:
Olivier Laurent, Roberto Maieli, "Cut Elimination for Monomial MALL Proof Nets," lics, pp.486-497, 2008 23rd Annual IEEE Symposium on Logic in Computer Science, 2008
Usage of this product signifies your acceptance of the Terms of Use.