loading...
Context Semantics, Linear Logic and Computational Complexity
Seattle, Washington August 12-August 15
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2006.2121st Annual IEEE Symposium on Logic i ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Ugo Dal Lago, Universite Paris 13, France
We show that context semantics can be fruitfully applied to the quantitative analysis of proof normalization in linear logic. In particular, context semantics lets us define the weight of a proof-net as a measure of its inherent complexity: it is both an upper bound to normalization time (modulo a polynomial overhead, independently on the reduction strategy) and a lower bound to the number of steps to normal form (for certain reduction strategies). Weights are then exploited in proving strong soundness theorems for various subsystems of linear logic, namely elementary linear logic, soft linear logic and light linear logic.
Citation:
Ugo Dal Lago, "Context Semantics, Linear Logic and Computational Complexity," lics, pp.169-178, 21st Annual IEEE Symposium on Logic in Computer Science (LICS'06), 2006
Usage of this product signifies your acceptance of the Terms of Use.


Suggestions