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.
My Menu
Saved Items

Proofnets and Context Semantics for the Additives

Harry G. MairsonContact Information and Xavier RivalContact Information

(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.

Contact Information Harry G. Mairson
Email: mairson@cs.brandeis.edu

Contact Information Xavier Rival
Email: rival@di.ens.fr
Fulltext Preview (Small, Large)
Image of the first page of the fulltext

References secured to subscribers.



Export this chapter
Export this chapter as RIS | Text
 
Remote Address: 38.107.191.108 • Server: mpweb03
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)