{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:43:37Z","timestamp":1750308217077,"version":"3.41.0"},"reference-count":19,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2006,7,1]],"date-time":"2006-07-01T00:00:00Z","timestamp":1151712000000},"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":[[2006,7]]},"abstract":"<jats:p>\n            We consider the following decision problems:ProofNet: Is a given multiplicative linear logic (MLL) proof structure a proof net?EssNet: Is a given essential net (of an intuitionistic MLL sequent) correct?In this article we show how to obtain linear-time algorithms for EssNet. As a corollary, by showing that ProofNet is linear-time reducible to EssNet (by the Trip Translation), we obtain a linear-time algorithm for ProofNet.We show further that it is possible to optimize the verification so that each node of the input structure is visited at most once. Finally, we present linear-time algorithms for\n            <jats:italic>sequentializing<\/jats:italic>\n            proof nets and essential nets, that is, for finding derivations of the underlying sequents.\n          <\/jats:p>","DOI":"10.1145\/1149114.1149116","type":"journal-article","created":{"date-parts":[[2006,10,18]],"date-time":"2006-10-18T18:11:32Z","timestamp":1161195092000},"page":"473-498","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Fast verification of MLL proof nets via IMLL"],"prefix":"10.1145","volume":"7","author":[{"given":"Andrzej S.","family":"Murawski","sequence":"first","affiliation":[{"name":"Oxford University Computing Laboratory, Oxford, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C.-H. Luke","family":"Ong","sequence":"additional","affiliation":[{"name":"Oxford University Computing Laboratory, Oxford, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2006,7]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539797317263"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00104-9"},{"key":"e_1_2_1_3_1","unstructured":"Bellin G. and van de Wiele J. 1992. Proof nets for classical MLL and linear lambda terms. Available online at http:\/\/www.seas.upenn.edu\/~sweirich\/types\/archive\/1992\/msg00057.html.  Bellin G. and van de Wiele J. 1992. Proof nets for classical MLL and linear lambda terms. Available online at http:\/\/www.seas.upenn.edu\/~sweirich\/types\/archive\/1992\/msg00057.html."},{"key":"e_1_2_1_4_1","unstructured":"Buchsbaum A. 2000. Private email communication.  Buchsbaum A. 2000. Private email communication."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/295656.295663"},{"key":"e_1_2_1_6_1","unstructured":"Cormen T. H. Leiserson C. E. and Rivest R. L. 1990. Introduction to Algorithms. MIT Press Cambridge MA.   Cormen T. H. Leiserson C. E. and Rivest R. L. 1990. Introduction to Algorithms. MIT Press Cambridge MA."},{"key":"e_1_2_1_7_1","unstructured":"Danos V. 1990. La logique lin\u00e9aire appliqu\u00e9e \u00e0 l'\u00e9tude de divers processus de normalisation et principalement du \u03bb-calcul. Ph.D. dissertation. Universit\u00e9 de Paris Paris France.  Danos V. 1990. La logique lin\u00e9aire appliqu\u00e9e \u00e0 l'\u00e9tude de divers processus de normalisation et principalement du \u03bb-calcul. Ph.D. dissertation. Universit\u00e9 de Paris Paris France."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01622878"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(05)80064-9"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/320176.320229"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90014-5"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/788021.788963"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/22145.22166"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80409-8"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/357062.357071"},{"key":"e_1_2_1_17_1","unstructured":"Murawski A. S. and Ong C.-H. L. 2000a. A linear-time algorithm for verifying MLL proof nets via essential nets. In Millennial Perspectives in Computer Science: Proceedings of the 1999 Oxford-Microsoft Symposium in Honour of Sir Tony Hoare J. Davies B. Roscoe and J. Woodcock Eds. Cornerstones in Computing Series. Palgrave Macmillan Houndsmills Basingstoke Hamps. U.K. 289--302.  Murawski A. S. and Ong C.-H. L. 2000a. A linear-time algorithm for verifying MLL proof nets via essential nets. In Millennial Perspectives in Computer Science: Proceedings of the 1999 Oxford-Microsoft Symposium in Honour of Sir Tony Hoare J. Davies B. Roscoe and J. Woodcock Eds. Cornerstones in Computing Series. Palgrave Macmillan Houndsmills Basingstoke Hamps. U.K. 289--302."},{"volume-title":"Proceedings of the 15th IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press","author":"Murawski A. S.","key":"e_1_2_1_18_1"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00244-4"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1149114.1149116","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1149114.1149116","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:31:13Z","timestamp":1750264273000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1149114.1149116"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,7]]},"references-count":19,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2006,7]]}},"alternative-id":["10.1145\/1149114.1149116"],"URL":"https:\/\/doi.org\/10.1145\/1149114.1149116","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2006,7]]},"assertion":[{"value":"2006-07-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}