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

Roversi:2014-JLC (Article)
Author(s) Luca Roversi
Title« A deep inference system with a self-dual binder which is complete for linear lambda calculus »
JournalJournal of Logic and Computation
Year2014
URLhttp://logcom.oxfordjournals.org/content/early/2014/06/05/logcom.exu033.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 λ-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{Roversi:2014-JLC,
  author = {Roversi, Luca},
  url = {http://logcom.oxfordjournals.org/content/early/2014/06/05/logcom.exu033.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/early/2014/06/05/logcom.exu033.full.pdf+html},
  year = {2014},
  doi = {10.1093/logcom/exu033},
  journal = {Journal of Logic and Computation},
}


 Chronological Overview 
 Type-Hierarchical Overview 
Formal Methods in Computing
(Most of the papers antecedent to 1995
are 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)

Valid HTML 4.01!