Formal Methods in Computing(Most of the papers antecedent to 1995are not included in the list) FRAMES  NO FRAME

 Roversi01042016 (Article) Author(s) Luca Roversi Title « A deep inference system with a self-dual binder which is complete for linear lambda calculus » Journal Journal of Logic and Computation Volume 26 Number 2 Page(s) 677-698 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 self-dual non-commutative logical operator Seq. We introduce SBVB that extends SBV by adding the self-dual binder Sdb on names. The system SBVB is consistent because we prove that (the analogous of) cut-elimination holds for it. Moreover, the resulting interplay between Seq and Sdb can model $\beta$-reduction of linear $\lambda$-calculus inside the cut-free subsystem BVB of SBVB. The long-term aim is to keep developing a programme whose goal is to give pure logical accounts of computational primitives under the proof-search-as-computation analogy, by means of minimal and incremental extensions of SBV.

 BibTeX code

@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 self-dual 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
self-dual non-commutative logical operator Seq. We introduce SBVB
that extends SBV by adding the self-dual binder Sdb on names. The
system SBVB is consistent because we prove that (the analogous of)
cut-elimination holds for it. Moreover, the resulting interplay
between Seq and Sdb can model $\beta$-reduction of linear
$\lambda$-calculus inside the cut-free subsystem BVB of SBVB. The
long-term aim is to keep developing a programme whose goal is to
give pure logical accounts of computational primitives under the
proof-search-as-computation analogy, by means of minimal and
incremental extensions of SBV.},
eprint = {http://logcom.oxfordjournals.org/content/26/2/677.full.pdf+html},
pages = {677-698},
journal = {Journal of Logic and Computation},
doi = {10.1093/logcom/exu033},
year = {2016},
}

 Formal Methods in Computing(Most of the papers antecedent to 1995are not included in the list) FRAMES  NO FRAME

This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)