Proof nets, garbage, and computations

Authors
Guerrini, S Martini, S Masini, A
Citation
S. Guerrini et al., Proof nets, garbage, and computations, THEOR COMP, 253(2), 2001, pp. 185-237
Citations number
28
Categorie Soggetti
Computer Science & Engineering
Journal title
THEORETICAL COMPUTER SCIENCE
ISSN journal
03043975 → ACNP
Volume
253
Issue
2
Year of publication
2001
Pages
185 - 237
Database
ISI
SICI code
0304-3975(20010228)253:2<185:PNGAC>2.0.ZU;2-9
Abstract
We study the problem of local and asynchronous computation in the context o f multiplicative exponential linear logic (MELL) proof nets. The main novel ty is in a complete set of rewriting rules for cut-elimination in presence of weakening (which requires garbage collection). The proposed reduction sy stem is strongly normalizing and confluent. The proofs are all based on pur e syntactical reasonings. (C) 2001 Elsevier Science B,V. All rights reserve d.