Roversi01042016 (Article)

Author(s)  Luca Roversi 
Title  « A deep inference system with a selfdual binder which is complete for linear lambda calculus » 
Journal  Journal of Logic and Computation 
Volume  26 
Number  2 
Page(s)  677698 
Year  2016 
URL  http://logcom.oxfordjournals.org/content/26/2/677.abstract 
Abstract 
We recall that SBV, a proof system developed under the methodology of deep inference, extends multiplicative linear logic with the selfdual noncommutative logical operator Seq. We introduce SBVB that extends SBV by adding the selfdual binder Sdb on names. The system SBVB is consistent because we prove that (the analogous of) cutelimination holds for it. Moreover, the resulting interplay between Seq and Sdb can model $\beta $reduction of linear $\lambda $calculus inside the cutfree subsystem BVB of SBVB. The longterm aim is to keep developing a programme whose goal is to give pure logical accounts of computational primitives under the proofsearchascomputation analogy, by means of minimal and incremental extensions of SBV. 
@article{Roversi01042016,
number = {2},
volume = {26},
author = {Roversi, Luca},
url = {http://logcom.oxfordjournals.org/content/26/2/677.abstract},
title = {A deep inference system with a selfdual binder which is complete for
linear lambda calculus},
abstract = {We recall that SBV, a proof system developed under the methodology
of deep inference, extends multiplicative linear logic with the
selfdual noncommutative logical operator Seq. We introduce SBVB
that extends SBV by adding the selfdual binder Sdb on names. The
system SBVB is consistent because we prove that (the analogous of)
cutelimination holds for it. Moreover, the resulting interplay
between Seq and Sdb can model $\beta$reduction of linear
$\lambda$calculus inside the cutfree subsystem BVB of SBVB. The
longterm aim is to keep developing a programme whose goal is to
give pure logical accounts of computational primitives under the
proofsearchascomputation analogy, by means of minimal and
incremental extensions of SBV.},
eprint = {http://logcom.oxfordjournals.org/content/26/2/677.full.pdf+html},
pages = {677698},
journal = {Journal of Logic and Computation},
doi = {10.1093/logcom/exu033},
year = {2016},
}
This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)