{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:13:32Z","timestamp":1750306412460,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":30,"publisher":"ACM","license":[{"start":{"date-parts":[[2015,7,14]],"date-time":"2015-07-14T00:00:00Z","timestamp":1436832000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Danish Council for Strategic Research","award":["10-092309"],"award-info":[{"award-number":["10-092309"]}]},{"name":"ERC"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2015,7,14]]},"DOI":"10.1145\/2790449.2790528","type":"proceedings-article","created":{"date-parts":[[2015,6,29]],"date-time":"2015-06-29T18:10:47Z","timestamp":1435601447000},"page":"43-54","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Computation in focused intuitionistic logic"],"prefix":"10.1145","author":[{"given":"Taus","family":"Brock-Nannestad","sequence":"first","affiliation":[{"name":"INRIA, Saclay, Palaiseau"}]},{"given":"Nicolas","family":"Guenot","sequence":"additional","affiliation":[{"name":"IT University of Copenhagen"}]},{"given":"Daniel","family":"Gustafsson","sequence":"additional","affiliation":[{"name":"IT University of Copenhagen"}]}],"member":"320","published-online":{"date-parts":[[2015,7,14]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628154"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.3.297"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1516507.1516508"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"D.\n      Baelde\n     and \n      D.\n      Miller\n  . \n  Least and greatest fixed points in linear logic\n  . In N. Dershowitz and A. Voronkov editors LPAR\n  '07 volume \n  4790\n   of \n  LNCS pages \n  92\n  --\n  106 2007\n  .   D. Baelde and D. Miller. Least and greatest fixed points in linear logic. In N. Dershowitz and A. Voronkov editors LPAR'07 volume 4790 of LNCS pages 92--106 2007.","DOI":"10.1007\/978-3-540-75560-9_9"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796899003524"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"crossref","unstructured":"T.\n      Brock-Nannestad\n     and \n      C.\n      Sch\u00fcrmann\n  . \n  Focused natural deduction\n  . In C. Ferm\u00fcller and A. Voronkov editors LPAR-\n  17 volume \n  6397\n   of \n  LNCS pages \n  157\n  --\n  171 2010\n  .   T. Brock-Nannestad and C. Sch\u00fcrmann. Focused natural deduction. In C. Ferm\u00fcller and A. Voronkov editors LPAR-17 volume 6397 of LNCS pages 157--171 2010.","DOI":"10.1007\/978-3-642-16242-8_12"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"crossref","unstructured":"K.\n      Chaudhuri\n    .\n  Classical and intuitionistic subexponential logics are equally expressive\n  . In A. Dawar and H. Veith editors CSL\n  '10 volume \n  6247\n   of \n  LNCS pages \n  185\n  --\n  199 2010\n  .   K. Chaudhuri. Classical and intuitionistic subexponential logics are equally expressive. In A. Dawar and H. Veith editors CSL'10 volume 6247 of LNCS pages 185--199 2010.","DOI":"10.1007\/978-3-642-15205-4_17"},{"key":"e_1_3_2_1_8_1","unstructured":"K.\n      Chaudhuri N.\n      Guenot and \n      L.\n      Stra\u00dfburger\n  . \n  The focused calculus of structures\n  . In M. Bezem editor CSL\n  '11 volume \n  12\n   of \n  LIPIcs pages \n  159\n  --\n  173 2011\n  .  K. Chaudhuri N. Guenot and L. Stra\u00dfburger. The focused calculus of structures. In M. Bezem editor CSL'11 volume 12 of LIPIcs pages 159--173 2011."},{"volume-title":"Mechanizing Mathematical Reasoning","year":"2005","author":"Cittadini S.","key":"e_1_3_2_1_9_1"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351262"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"crossref","unstructured":"P.-L.\n      Curien\n     and \n      G.\n      Munch-Maccagnoni\n  . \n  The duality of computation under focus\n  . In C. S. Calude and V. Sassone editors IFIP TCS\n  '10 volume \n  323\n   of \n  AICT pages \n  165\n  --\n  181 2010\n  .  P.-L. Curien and G. Munch-Maccagnoni. The duality of computation under focus. In C. S. Calude and V. Sassone editors IFIP TCS'10 volume 323 of AICT pages 165--181 2010.","DOI":"10.1007\/978-3-642-15240-5_13"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/212876.212894"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.2307\/2275572"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/11780342_19"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"crossref","unstructured":"J.\n      Esp\u00edrito Santo\n    .\n  Completing Herbelin's programme\n  . In S. Ronchi editor TLCA\n  '07 volume \n  4583\n   of \n  LNCS pages \n  118\n  --\n  132 2007\n  .   J. Esp\u00edrito Santo. Completing Herbelin's programme. In S. Ronchi editor TLCA'07 volume 4583 of LNCS pages 118--132 2007.","DOI":"10.1007\/978-3-540-73228-0_10"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"crossref","unstructured":"J.\n      Esp\u00edrito Santo\n    .\n  Delayed substitutions\n  . In F. Baader editor RTA\n  '07 volume \n  4533\n   of \n  LNCS pages \n  169\n  --\n  183 2007\n  .   J. Esp\u00edrito Santo. Delayed substitutions. In F. Baader editor RTA'07 volume 4533 of LNCS pages 169--183 2007.","DOI":"10.1007\/978-3-540-73449-9_14"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00224-009-9183-9"},{"volume-title":"Control operators, the SECD-machine and the \u039b-calculus","year":"1986","author":"Felleisen M.","key":"e_1_3_2_1_18_1"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001328"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"crossref","unstructured":"H.\n      Herbelin\n    .\n  A \u039b-calculus structure isomorphic to Gentzen-style sequent calculus structure\n  . In L. Pacholski and J. Tiuryn editors CSL\n  '94 volume \n  933\n   of \n  LNCS pages \n  61\n  --\n  75 1994\n  .   H. Herbelin. A \u039b-calculus structure isomorphic to Gentzen-style sequent calculus structure. In L. Pacholski and J. Tiuryn editors CSL'94 volume 933 of LNCS pages 61--75 1994.","DOI":"10.1007\/BFb0022247"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"crossref","unstructured":"F.\n      Joachimski\n     and \n      R.\n      Matthes\n  . \n  Standardization and confluence for a lambda calculus with generalized applications\n  . In L. Bachmair editor RTA\n  '00 volume \n  1833\n   of \n  LNCS pages \n  141\n  --\n  155 2000\n  .   F. Joachimski and R. Matthes. Standardization and confluence for a lambda calculus with generalized applications. In L. Bachmair editor RTA'00 volume 1833 of LNCS pages 141--155 2000.","DOI":"10.1007\/10721975_10"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-007-9018-9"},{"volume-title":"Universit\u00e9 Aix-Marseille II","year":"2002","author":"Laurent O.","key":"e_1_3_2_1_24_1"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-0480-6"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.07.041"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/77350.77353"},{"volume-title":"LFMTP'13","year":"2013","author":"Nigam V.","key":"e_1_3_2_1_28_1"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2629678"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2008.01.001"}],"event":{"name":"PPDP '15: 17th International Symposium on Principles and Practice of Declarative Programming","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Siena Italy","acronym":"PPDP '15"},"container-title":["Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2790449.2790528","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2790449.2790528","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T05:07:46Z","timestamp":1750223266000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2790449.2790528"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,7,14]]},"references-count":30,"alternative-id":["10.1145\/2790449.2790528","10.1145\/2790449"],"URL":"https:\/\/doi.org\/10.1145\/2790449.2790528","relation":{},"subject":[],"published":{"date-parts":[[2015,7,14]]},"assertion":[{"value":"2015-07-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}