{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:16:56Z","timestamp":1762460216456,"version":"3.41.0"},"reference-count":20,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2011,5,1]],"date-time":"2011-05-01T00:00:00Z","timestamp":1304208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2011,5]]},"abstract":"<jats:p>\n            Multiary sequent terms were originally introduced as a tool for proving termination of permutative conversions in cut-free sequent calculus. This work develops the language of multiary sequent terms into a term calculus for the computational (Curry-Howard) interpretation of a fragment of sequent calculus with cuts and cut-elimination rules. The system, called\n            <jats:italic>generalized multiary \u03bb-calculus<\/jats:italic>\n            , is a rich extension of the \u03bb-calculus where the computational content of the sequent calculus format is explained through an enlarged form of the application constructor. Such constructor exhibits the features of multiarity (the ability to form lists of arguments) and generality (the ability to prescribe a kind of continuation). The system integrates in a modular way the multiary \u03bb-calculus and an isomorphic copy of the \u03bb-calculus with generalized application, \u039b\n            <jats:italic>J<\/jats:italic>\n            (in particular, natural deduction is captured internally up to isomorphism). In addition, the system: (i) comes with permutative conversion rules, whose role is to eliminate the new features of application; (ii) is equipped with reduction rules \u2014 either the \u03bc-rule, typical of the multiary setting, or rules for cut-elimination, which enlarge the ordinary \u03b2-rule. This article establishes the metatheory of the system, with emphasis on the role of the \u03bc-rule, and including a study of the interaction of reduction and permutative conversions.\n          <\/jats:p>","DOI":"10.1145\/1929954.1929959","type":"journal-article","created":{"date-parts":[[2011,5,17]],"date-time":"2011-05-17T12:59:03Z","timestamp":1305637143000},"page":"1-41","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["A calculus of multiary sequent terms"],"prefix":"10.1145","volume":"12","author":[{"given":"Jos\u00e9 Esp\u00edrito","family":"Santo","sequence":"first","affiliation":[{"name":"Universidade do Minho, Braga, Portugal"}]},{"given":"Lu\u00eds","family":"Pinto","sequence":"additional","affiliation":[{"name":"Universidade do Minho, Braga, Portugal"}]}],"member":"320","published-online":{"date-parts":[[2011,5,16]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.03.032"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351262"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00138-8"},{"key":"e_1_2_2_4_1","unstructured":"Esp\u00edrito Santo J. 2002a. Conservative extensions of the \u03bb-calculus for the computational interpretation of sequent calculus. Ph.D. thesis University of Edinburgh.  Esp\u00edrito Santo J. 2002a. Conservative extensions of the \u03bb-calculus for the computational interpretation of sequent calculus. Ph.D. thesis University of Edinburgh."},{"key":"e_1_2_2_5_1","volume-title":"Proceedings of LPAR'02","volume":"2514","author":"Esp\u00edrito Santo J.","year":"2002"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11805618_15"},{"key":"e_1_2_2_7_1","unstructured":"Esp\u00edrito Santo J. Matthes R. and \n      \n      \n      Pinto L\n      \n  \n  . \n  2007\n  . Continuation-passing style and strong normalization for intuitionistic sequent calculi. In Proceedings of TLCA'07. S. Ronchi Della Rocca Ed. Lecture Notes in Computer Science vol. \n  4583 Springer Berlin 286--300.   Esp\u00edrito Santo J. Matthes R. and Pinto L. 2007. Continuation-passing style and strong normalization for intuitionistic sequent calculi. In Proceedings of TLCA'07. S. Ronchi Della Rocca Ed. Lecture Notes in Computer Science vol. 4583 Springer Berlin 286--300."},{"key":"e_1_2_2_8_1","doi-asserted-by":"crossref","unstructured":"Esp\u00edrito Santo J.\n     and \n      \n      \n      Pinto L\n      \n  \n  . \n  2003\n  . Permutative conversions in intuitionistic multiary sequent calculus with cuts. In Proceedings of the TLCA'03. M. Hoffman Ed. Lecture Notes in Computer Science vol. \n  2701 Springer Berlin 286--300.   Esp\u00edrito Santo J. and Pinto L. 2003. Permutative conversions in intuitionistic multiary sequent calculus with cuts. In Proceedings of the TLCA'03. M. Hoffman Ed. Lecture Notes in Computer Science vol. 2701 Springer Berlin 286--300.","DOI":"10.1007\/3-540-44904-3_20"},{"key":"e_1_2_2_9_1","doi-asserted-by":"crossref","unstructured":"Esp\u00edrito Santo J.\n     and \n      \n      \n      Pinto L\n      \n  \n  . \n  2004\n  . Confluence and strong normalization of the generalised multiary \u03bb-calculus. In Revised Selected Papers from the International Workshop TYPES 2003. S. Berardi et al. Eds. Lecture Notes in Computer Science vol. \n  3085 Springer Berlin 194--209.  Esp\u00edrito Santo J. and Pinto L. 2004. Confluence and strong normalization of the generalised multiary \u03bb-calculus. In Revised Selected Papers from the International Workshop TYPES 2003. S. Berardi et al. Eds. Lecture Notes in Computer Science vol. 3085 Springer Berlin 194--209.","DOI":"10.1007\/978-3-540-24849-1_13"},{"volume-title":"The Collected Papers of Gerhard Gentzen","author":"Gentzen G.","key":"e_1_2_2_10_1"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/647844.736588"},{"key":"e_1_2_2_12_1","doi-asserted-by":"crossref","unstructured":"Joachimski F.\n     and \n      \n      \n      Matthes R\n      \n  \n  . \n  2000\n  . Standardization and confluence for a lambda-calculus with generalized applications. In Proceedings of RTA'00. L. Bachmair Ed. Lecture Notes in Computer Science vol. \n  1833 Springer Berlin 141--155.   Joachimski F. and Matthes R. 2000. Standardization and confluence for a lambda-calculus with generalized applications. In Proceedings of RTA'00. L. Bachmair Ed. Lecture Notes in Computer Science vol. 1833 Springer Berlin 141--155.","DOI":"10.1007\/10721975_10"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00153-002-0156-9"},{"key":"e_1_2_2_14_1","doi-asserted-by":"crossref","unstructured":"Kesner D. 2009. A theory of explicit substitutions with safe and full composition. Logical Meth. Comput. Sci 5 3:1 1--29.  Kesner D. 2009. A theory of explicit substitutions with safe and full composition. Logical Meth. Comput. Sci 5 3:1 1--29.","DOI":"10.2168\/LMCS-5(3:1)2009"},{"key":"e_1_2_2_15_1","unstructured":"Mints G. 1996. Normal forms for sequent derivations. In Kreiseliana P. Odifreddi Ed. A. K. Peters Wellesley MA 469--492.  Mints G. 1996. Normal forms for sequent derivations. In Kreiseliana P. Odifreddi Ed. A. K. Peters Wellesley MA 469--492."},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0003-4843(77)80004-1"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/297346.297375"},{"volume":"149","volume-title":"Studies in Logic and the Foundations of Mathematics","author":"S\u00f8rensen M.","key":"e_1_2_2_18_1"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001530100091"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/0003-4843(74)90010-2"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1929954.1929959","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1929954.1929959","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T10:52:38Z","timestamp":1750243958000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1929954.1929959"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,5]]},"references-count":20,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2011,5]]}},"alternative-id":["10.1145\/1929954.1929959"],"URL":"https:\/\/doi.org\/10.1145\/1929954.1929959","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2011,5]]},"assertion":[{"value":"2009-07-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-05-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}