Additives of linear logic and normalization—Part I: a (restricted) Church–Rosser property

We define a generalized cut-elimination procedure for proof-nets of full linear logic (without constants), for which we prove a (restricted) Church–Rosser property.

Saved in:
Bibliographic Details
Published in:Theoretical computer science 2003-02, Vol.294 (3), p.489-524
Main Author: Tortora de Falco, Lorenzo
Format: Article
Language:English
Subjects:
Additive connectives
Confluence
Cut-elimination
Exact sciences and technology
General logic
Logic and foundations
Mathematical logic, foundations, set theory
Mathematics
Proof-nets with jumps
Sciences and techniques of general use
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
cited_by cdi_FETCH-LOGICAL-c3301-9c16e886e82ca99cfc6b288a8b89f2593230660c2a0b71c386c058ed390e42d73
cites cdi_FETCH-LOGICAL-c3301-9c16e886e82ca99cfc6b288a8b89f2593230660c2a0b71c386c058ed390e42d73
container_end_page 524
container_issue 3
container_start_page 489
container_title Theoretical computer science
container_volume 294
creator Tortora de Falco, Lorenzo
description We define a generalized cut-elimination procedure for proof-nets of full linear logic (without constants), for which we prove a (restricted) Church–Rosser property.
doi_str_mv 10.1016/S0304-3975(01)00176-1
format article
fullrecord <record><control><sourceid>proquest_cross</sourceid><recordid>TN_cdi_proquest_miscellaneous_27828947</recordid><sourceformat>XML</sourceformat><sourcesystem>PC</sourcesystem><els_id>S0304397501001761</els_id><sourcerecordid>27828947</sourcerecordid><originalsourceid>FETCH-LOGICAL-c3301-9c16e886e82ca99cfc6b288a8b89f2593230660c2a0b71c386c058ed390e42d73</originalsourceid><addsrcrecordid>eNqFkMtKA0EQRRtRMD4-QeiNkixG-zEz3e1GQvAFguJjKU2npsa0TGZi90TQlf-gX-iXODGiSwuK2pyqe-sSssPZPmc8P7hhkqWJNCrrMz5gjKs84Sukx7UyiRAmXSW9X2SdbMT4yLrKVN4j98Oi8K1_xkibkla-Rhdo1Tx4oK4uaN2Eqav8q2t9U3--fVy50NLzQ-poP2Bsg4cWiwEdTeYBJp9v79dNjBjoLDQzDO3LFlkrXRVx-2dukruT49vRWXJxeXo-Gl4kICXjiQGeo9ZdC3DGQAn5WGjt9FibUmRGCsnynIFwbKw4SJ0DyzQW0jBMRaHkJtlb3u2En-adMTv1EbCqXI3NPFqhtNAmXYDZEoTQOQ1Y2lnwUxdeLGd2Eab9DtMukrKM2-8wLe_2dn8EXARXlcHV4OPfcpopxbMFd7TksPv22WOwETzWgIUPCK0tGv-P0hen8Iod</addsrcrecordid><sourcetype>Aggregation Database</sourcetype><iscdi>true</iscdi><recordtype>article</recordtype><pqid>27828947</pqid></control><display><type>article</type><title>Additives of linear logic and normalization—Part I: a (restricted) Church–Rosser property</title><source>Elsevier:Jisc Collections:Elsevier Read and Publish Agreement 2022-2024:Freedom Collection (Reading list)</source><creator>Tortora de Falco, Lorenzo</creator><creatorcontrib>Tortora de Falco, Lorenzo</creatorcontrib><description>We define a generalized cut-elimination procedure for proof-nets of full linear logic (without constants), for which we prove a (restricted) Church–Rosser property.</description><identifier>ISSN: 0304-3975</identifier><identifier>EISSN: 1879-2294</identifier><identifier>DOI: 10.1016/S0304-3975(01)00176-1</identifier><identifier>CODEN: TCSCDI</identifier><language>eng</language><publisher>Amsterdam: Elsevier B.V</publisher><subject>Additive connectives ; Confluence ; Cut-elimination ; Exact sciences and technology ; General logic ; Logic and foundations ; Mathematical logic, foundations, set theory ; Mathematics ; Proof-nets with jumps ; Sciences and techniques of general use</subject><ispartof>Theoretical computer science, 2003-02, Vol.294 (3), p.489-524</ispartof><rights>2002 Elsevier Science B.V.</rights><rights>2003 INIST-CNRS</rights><lds50>peer_reviewed</lds50><oa>free_for_read</oa><woscitedreferencessubscribed>false</woscitedreferencessubscribed><citedby>FETCH-LOGICAL-c3301-9c16e886e82ca99cfc6b288a8b89f2593230660c2a0b71c386c058ed390e42d73</citedby><cites>FETCH-LOGICAL-c3301-9c16e886e82ca99cfc6b288a8b89f2593230660c2a0b71c386c058ed390e42d73</cites></display><links><openurl>$$Topenurl_article</openurl><openurlfulltext>$$Topenurlfull_article</openurlfulltext><thumbnail>$$Tsyndetics_thumb_exl</thumbnail><link.rule.ids>309,310,314,776,780,785,786,23910,23911,25119,27903,27904</link.rule.ids><backlink>$$Uhttp://pascal-francis.inist.fr/vibad/index.php?action=getRecordDetail&amp;idt=14577151$$DView record in Pascal Francis$$Hfree_for_read</backlink></links><search><creatorcontrib>Tortora de Falco, Lorenzo</creatorcontrib><title>Additives of linear logic and normalization—Part I: a (restricted) Church–Rosser property</title><title>Theoretical computer science</title><description>We define a generalized cut-elimination procedure for proof-nets of full linear logic (without constants), for which we prove a (restricted) Church–Rosser property.</description><subject>Additive connectives</subject><subject>Confluence</subject><subject>Cut-elimination</subject><subject>Exact sciences and technology</subject><subject>General logic</subject><subject>Logic and foundations</subject><subject>Mathematical logic, foundations, set theory</subject><subject>Mathematics</subject><subject>Proof-nets with jumps</subject><subject>Sciences and techniques of general use</subject><issn>0304-3975</issn><issn>1879-2294</issn><fulltext>true</fulltext><rsrctype>article</rsrctype><creationdate>2003</creationdate><recordtype>article</recordtype><recordid>eNqFkMtKA0EQRRtRMD4-QeiNkixG-zEz3e1GQvAFguJjKU2npsa0TGZi90TQlf-gX-iXODGiSwuK2pyqe-sSssPZPmc8P7hhkqWJNCrrMz5gjKs84Sukx7UyiRAmXSW9X2SdbMT4yLrKVN4j98Oi8K1_xkibkla-Rhdo1Tx4oK4uaN2Eqav8q2t9U3--fVy50NLzQ-poP2Bsg4cWiwEdTeYBJp9v79dNjBjoLDQzDO3LFlkrXRVx-2dukruT49vRWXJxeXo-Gl4kICXjiQGeo9ZdC3DGQAn5WGjt9FibUmRGCsnynIFwbKw4SJ0DyzQW0jBMRaHkJtlb3u2En-adMTv1EbCqXI3NPFqhtNAmXYDZEoTQOQ1Y2lnwUxdeLGd2Eab9DtMukrKM2-8wLe_2dn8EXARXlcHV4OPfcpopxbMFd7TksPv22WOwETzWgIUPCK0tGv-P0hen8Iod</recordid><startdate>20030218</startdate><enddate>20030218</enddate><creator>Tortora de Falco, Lorenzo</creator><general>Elsevier B.V</general><general>Elsevier</general><scope>6I.</scope><scope>AAFTH</scope><scope>IQODW</scope><scope>AAYXX</scope><scope>CITATION</scope><scope>7SC</scope><scope>8FD</scope><scope>JQ2</scope><scope>L7M</scope><scope>L~C</scope><scope>L~D</scope></search><sort><creationdate>20030218</creationdate><title>Additives of linear logic and normalization—Part I: a (restricted) Church–Rosser property</title><author>Tortora de Falco, Lorenzo</author></sort><facets><frbrtype>5</frbrtype><frbrgroupid>cdi_FETCH-LOGICAL-c3301-9c16e886e82ca99cfc6b288a8b89f2593230660c2a0b71c386c058ed390e42d73</frbrgroupid><rsrctype>articles</rsrctype><prefilter>articles</prefilter><language>eng</language><creationdate>2003</creationdate><topic>Additive connectives</topic><topic>Confluence</topic><topic>Cut-elimination</topic><topic>Exact sciences and technology</topic><topic>General logic</topic><topic>Logic and foundations</topic><topic>Mathematical logic, foundations, set theory</topic><topic>Mathematics</topic><topic>Proof-nets with jumps</topic><topic>Sciences and techniques of general use</topic><toplevel>peer_reviewed</toplevel><toplevel>online_resources</toplevel><creatorcontrib>Tortora de Falco, Lorenzo</creatorcontrib><collection>ScienceDirect Open Access Titles</collection><collection>Elsevier:ScienceDirect:Open Access</collection><collection>Pascal-Francis</collection><collection>CrossRef</collection><collection>Computer and Information Systems Abstracts</collection><collection>Technology Research Database</collection><collection>ProQuest Computer Science Collection</collection><collection>Advanced Technologies Database with Aerospace</collection><collection>Computer and Information Systems Abstracts – Academic</collection><collection>Computer and Information Systems Abstracts Professional</collection><jtitle>Theoretical computer science</jtitle></facets><delivery><delcategory>Remote Search Resource</delcategory><fulltext>fulltext</fulltext></delivery><addata><au>Tortora de Falco, Lorenzo</au><format>journal</format><genre>article</genre><ristype>JOUR</ristype><atitle>Additives of linear logic and normalization—Part I: a (restricted) Church–Rosser property</atitle><jtitle>Theoretical computer science</jtitle><date>2003-02-18</date><risdate>2003</risdate><volume>294</volume><issue>3</issue><spage>489</spage><epage>524</epage><pages>489-524</pages><issn>0304-3975</issn><eissn>1879-2294</eissn><coden>TCSCDI</coden><abstract>We define a generalized cut-elimination procedure for proof-nets of full linear logic (without constants), for which we prove a (restricted) Church–Rosser property.</abstract><cop>Amsterdam</cop><pub>Elsevier B.V</pub><doi>10.1016/S0304-3975(01)00176-1</doi><tpages>36</tpages><oa>free_for_read</oa></addata></record>
fulltext fulltext
identifier ISSN: 0304-3975
ispartof Theoretical computer science, 2003-02, Vol.294 (3), p.489-524
issn 0304-3975
1879-2294
language eng
recordid cdi_proquest_miscellaneous_27828947
source Elsevier:Jisc Collections:Elsevier Read and Publish Agreement 2022-2024:Freedom Collection (Reading list)
subjects Additive connectives
Confluence
Cut-elimination
Exact sciences and technology
General logic
Logic and foundations
Mathematical logic, foundations, set theory
Mathematics
Proof-nets with jumps
Sciences and techniques of general use
title Additives of linear logic and normalization—Part I: a (restricted) Church–Rosser property
url http://sfxeu10.hosted.exlibrisgroup.com/loughborough?ctx_ver=Z39.88-2004&ctx_enc=info:ofi/enc:UTF-8&ctx_tim=2025-01-24T07%3A50%3A08IST&url_ver=Z39.88-2004&url_ctx_fmt=infofi/fmt:kev:mtx:ctx&rfr_id=info:sid/primo.exlibrisgroup.com:primo3-Article-proquest_cross&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.genre=article&rft.atitle=Additives%20of%20linear%20logic%20and%20normalization%E2%80%94Part%20I:%20a%20(restricted)%20Church%E2%80%93Rosser%20property&rft.jtitle=Theoretical%20computer%20science&rft.au=Tortora%20de%20Falco,%20Lorenzo&rft.date=2003-02-18&rft.volume=294&rft.issue=3&rft.spage=489&rft.epage=524&rft.pages=489-524&rft.issn=0304-3975&rft.eissn=1879-2294&rft.coden=TCSCDI&rft_id=info:doi/10.1016/S0304-3975(01)00176-1&rft_dat=%3Cproquest_cross%3E27828947%3C/proquest_cross%3E%3Cgrp_id%3Ecdi_FETCH-LOGICAL-c3301-9c16e886e82ca99cfc6b288a8b89f2593230660c2a0b71c386c058ed390e42d73%3C/grp_id%3E%3Coa%3E%3C/oa%3E%3Curl%3E%3C/url%3E&rft_id=info:oai/&rft_pqid=27828947&rft_id=info:pmid/&rfr_iscdi=true