Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
|
 |
Proofnets and Context Semantics for the Additives
| |
|
Proofnets and Context Semantics for the Additives
Harry G. Mairson5 and Xavier Rival6 
| (5) |
Computer Science Department, Brandeis University Waltham, Massachusetts, 02454 |
| (6) |
École Normale Superieure, 45 rue d’Ulm, 75005 Paris |
Abstract
We provide a context semantics for Multiplicative-Additive Linear Logic (MALL), together with proofnets whose reduction preserves semantics, where proofnet reduction is equated with cut-elimination on MALL sequents. The results
extend the program of Gonthier, Abadi, and Lévy, who provided a “geometry of optimal λ-reduction” (context semantics) for
λ-calculus and Multiplicative-Exponential Linear Logic (MELL). We integrate three features: a semantics that uses buses to implement slicing; a proofnet technology that allows multidimensional boxes and generalized garbage, preserving the linearity of additive reduction; and finally, a read-back procedure that computes a cut-free proof from the semantics, a constructive companion to full abstraction theorems.
Fulltext Preview (Small, Large)
 References secured to subscribers.
|
|
|
|
|
|