{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,14]],"date-time":"2026-03-14T09:03:15Z","timestamp":1773478995355,"version":"3.50.1"},"publisher-location":"Singapore","reference-count":29,"publisher":"Springer Nature Singapore","isbn-type":[{"value":"9789819983100","type":"print"},{"value":"9789819983117","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"DOI":"10.1007\/978-981-99-8311-7_5","type":"book-chapter","created":{"date-parts":[[2023,11,22]],"date-time":"2023-11-22T07:02:17Z","timestamp":1700636537000},"page":"91-111","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Proofs as\u00a0Terms, Terms as\u00a0Graphs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5880-5379","authenticated-orcid":false,"given":"Jui-Hsuan","family":"Wu","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,11,21]]},"reference":[{"issue":"4","key":"5_CR1","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1017\/S0956796800000186","volume":"1","author":"M Abadi","year":"1991","unstructured":"Abadi, M., Cardelli, L., Curien, P.L., L\u00e9vy, J.J.: Explicit substitutions. J. Funct. Program. 1(4), 375\u2013416 (1991)","journal-title":"J. Funct. Program."},{"key":"5_CR2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.08.006","author":"B Accattoli","year":"2015","unstructured":"Accattoli, B.: Proof nets and the call-by-value $$\\lambda $$-calculus. J. Theor. Comput. Sci. (TCS) (2015). https:\/\/doi.org\/10.1016\/j.tcs.2015.08.006","journal-title":"J. Theor. Comput. Sci. (TCS)"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-030-02508-3_3","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2018","author":"B Accattoli","year":"2018","unstructured":"Accattoli, B.: Proof nets and the linear substitution calculus. In: Fischer, B., Uustalu, T. (eds.) ICTAC 2018. LNCS, vol. 11187, pp. 37\u201361. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-02508-3_3"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Accattoli, B., Bonelli, E., Kesner, D., Lombardi, C.: A nonstandard standardization theorem. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 659\u2013670 (2014)","DOI":"10.1145\/2535838.2535886"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Accattoli, B., Condoluci, A., Coen, C.S.: Strong call-by-value is reasonable, implosively. In: 2021 36th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS), pp. 1\u201314. IEEE (2021)","DOI":"10.1109\/LICS52264.2021.9470630"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/978-3-642-29822-6_4","volume-title":"Functional and Logic Programming","author":"B Accattoli","year":"2012","unstructured":"Accattoli, B., Paolini, L.: Call-by-value solvability, revisited. In: Schrijvers, T., Thiemann, P. (eds.) FLOPS 2012. LNCS, vol. 7294, pp. 4\u201316. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-29822-6_4"},{"issue":"3","key":"5_CR7","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1093\/logcom\/2.3.297","volume":"2","author":"JM Andreoli","year":"1992","unstructured":"Andreoli, J.M.: Logic programming with focusing proofs in linear logic. J. Logic Comput. 2(3), 297\u2013347 (1992). https:\/\/doi.org\/10.1093\/logcom\/2.3.297","journal-title":"J. Logic Comput."},{"issue":"1","key":"5_CR8","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1016\/S0168-0072(00)00032-4","volume":"107","author":"JM Andreoli","year":"2001","unstructured":"Andreoli, J.M.: Focussing and proof construction. Ann. Pure Appl. Logic 107(1), 131\u2013163 (2001)","journal-title":"Ann. Pure Appl. Logic"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"Balabonski, T.: A unified approach to fully lazy sharing. In: Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 469\u2013480 (2012)","DOI":"10.1145\/2103656.2103713"},{"key":"5_CR10","doi-asserted-by":"publisher","unstructured":"Brock-Nannestad, T., Guenot, N., Gustafsson, D.: Computation in focused intuitionistic logic. In: Falaschi, M., Albert, E. (eds.) Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, Siena, Italy, 14\u201316 July 2015. pp. 43\u201354. ACM (2015). https:\/\/doi.org\/10.1145\/2790449.2790528","DOI":"10.1145\/2790449.2790528"},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1007\/978-3-540-89439-1_33","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"K Chaudhuri","year":"2008","unstructured":"Chaudhuri, K.: Focusing strategies in the sequent calculus of synthetic connectives. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 467\u2013481. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-89439-1_33"},{"issue":"2","key":"5_CR12","doi-asserted-by":"publisher","first-page":"577","DOI":"10.1093\/logcom\/exu030","volume":"26","author":"K Chaudhuri","year":"2016","unstructured":"Chaudhuri, K., Hetzl, S., Miller, D.: A multi-focused proof system isomorphic to expansion proofs. J. Log. Comput. 26(2), 577\u2013603 (2016)","journal-title":"J. Log. Comput."},{"key":"5_CR13","series-title":"IFIP International Federation for Information Processing","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-0-387-09680-3_26","volume-title":"Fifth IFIP International Conference On Theoretical Computer Science \u2013 Tcs 2008","author":"K Chaudhuri","year":"2008","unstructured":"Chaudhuri, K., Miller, D., Saurin, A.: Canonical sequent proofs via multi-focusing. In: Ausiello, G., Karhum\u00e4ki, J., Mauri, G., Ong, L. (eds.) TCS 2008. IIFIP, vol. 273, pp. 383\u2013396. Springer, Boston, MA (2008). https:\/\/doi.org\/10.1007\/978-0-387-09680-3_26"},{"key":"5_CR14","doi-asserted-by":"publisher","unstructured":"Condoluci, A., Accattoli, B., Coen, C.S.: Sharing equality is linear. In: Proceedings of the 21st International Symposium on Principles and Practice of Declarative Programming, pp. 1\u201314 (2019). https:\/\/doi.org\/10.1145\/3354166.3354174","DOI":"10.1145\/3354166.3354174"},{"key":"5_CR15","doi-asserted-by":"publisher","unstructured":"Danos, V., Joinet, J.B., Schellinx, H.: LKT and LKQ: sequent calculi for second order logic based upon dual linear decompositions of classical implication. In: Girard, J.Y., Lafont, Y., Regnier, L. (eds.) Advances in Linear Logic, pp. 211\u2013224. No. 222 in London Mathematical Society Lecture Note Series, Cambridge University Press (1995). https:\/\/doi.org\/10.1017\/CBO9780511629150","DOI":"10.1017\/CBO9780511629150"},{"key":"5_CR16","doi-asserted-by":"publisher","unstructured":"Delande, O., Miller, D.: A neutral approach to proof and refutation in MALL. In: Pfenning, F. (ed.) 23th Symposium on Logic in Computer Science, pp. 498\u2013508. IEEE Computer Society Press (2008). https:\/\/doi.org\/10.1016\/j.apal.2009.07.017","DOI":"10.1016\/j.apal.2009.07.017"},{"key":"5_CR17","doi-asserted-by":"publisher","unstructured":"Di Cosmo, R., Kesner, D.: Strong normalization of explicit substitutions via cut elimination in proof nets. In: Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science, pp. 35\u201346 (1997). https:\/\/doi.org\/10.1109\/LICS.1997.614927","DOI":"10.1109\/LICS.1997.614927"},{"key":"5_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/11780342_19","volume-title":"Logical Approaches to Computational Barriers","author":"R Dyckhoff","year":"2006","unstructured":"Dyckhoff, R., Lengrand, S.: LJQ: a strongly focused calculus for intuitionistic logic. In: Beckmann, A., Berger, U., L\u00f6we, B., Tucker, J.V. (eds.) CiE 2006. LNCS, vol. 3988, pp. 173\u2013185. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11780342_19"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Sabry, A., Duba, B.F., Felleisen, M.: The essence of compiling with continuations. In: Proceedings of the ACM SIGPLAN 1993 Conference on Programming Language Design and Implementation, pp. 237\u2013247 (1993)","DOI":"10.1145\/155090.155113"},{"issue":"1","key":"5_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"JY Girard","year":"1987","unstructured":"Girard, J.Y.: Linear logic. Theoret. Comput. Sci. 50(1), 1\u2013102 (1987). https:\/\/doi.org\/10.1016\/0304-3975(87)90045-4","journal-title":"Theoret. Comput. Sci."},{"key":"5_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/BFb0022247","volume-title":"Computer Science Logic","author":"H Herbelin","year":"1995","unstructured":"Herbelin, H.: A $$\\lambda $$-calculus structure isomorphic to Gentzen-style sequent calculus structure. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol. 933, pp. 61\u201375. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/BFb0022247"},{"issue":"3","key":"5_CR22","doi-asserted-by":"publisher","first-page":"1065","DOI":"10.4007\/annals.2006.164.1065","volume":"143","author":"DJD Hughes","year":"2006","unstructured":"Hughes, D.J.D.: Proofs without syntax. Ann. Math. 143(3), 1065\u20131076 (2006)","journal-title":"Ann. Math."},{"key":"5_CR23","doi-asserted-by":"publisher","unstructured":"Liang, C., Miller, D.: Focusing and polarization in linear, intuitionistic, and classical logics. Theor. Comput. Sci. 410(46), 4747\u20134768 (2009). https:\/\/doi.org\/10.1016\/j.tcs.2009.07.041, abstract Interpretation and Logic Programming: In honor of professor Giorgio Levi","DOI":"10.1016\/j.tcs.2009.07.041"},{"issue":"5","key":"5_CR24","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.apal.2022.103091","volume":"173","author":"S Marin","year":"2022","unstructured":"Marin, S., Miller, D., Pimentel, E., Volpe, M.: From axioms to synthetic inference rules via focusing. Ann. Pure Appl. Logic 173(5), 1\u201332 (2022). https:\/\/doi.org\/10.1016\/j.apal.2022.103091","journal-title":"Ann. Pure Appl. Logic"},{"issue":"4","key":"5_CR25","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/BF00370646","volume":"46","author":"D Miller","year":"1987","unstructured":"Miller, D.: A compact representation of proofs. Stud. Logica. 46(4), 347\u2013370 (1987). https:\/\/doi.org\/10.1007\/BF00370646","journal-title":"Stud. Logica."},{"key":"5_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/978-3-540-74915-8_31","volume-title":"Computer Science Logic","author":"D Miller","year":"2007","unstructured":"Miller, D., Saurin, A.: From proofs to focused proofs: a modular proof of focalization in linear logic. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 405\u2013419. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74915-8_31"},{"key":"5_CR27","doi-asserted-by":"publisher","unstructured":"Miller, D., Wu, J.H.: A positive perspective on term representations. In: Klin, B., Pimentel, E. (eds.) 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), vol. 252, pp. 3:1\u20133:21. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2023). https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2023.3","DOI":"10.4230\/LIPIcs.CSL.2023.3"},{"key":"5_CR28","doi-asserted-by":"publisher","unstructured":"Pimentel, E., Nigam, V., Neto, J.: Multi-focused proofs with different polarity assignments. In: Benevides, M., Thiemann, R. (eds.) Proceedings of the Tenth Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2015), ENTCS, vol. 323, pp. 163\u2013179, July 2016. https:\/\/doi.org\/10.1016\/j.entcs.2016.06.011","DOI":"10.1016\/j.entcs.2016.06.011"},{"key":"5_CR29","unstructured":"Wadsworth, C.P.: Semantics and Pragmatics of the Lambda Calculus. Ph.D. thesis, University of Oxford (1971)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-99-8311-7_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,22]],"date-time":"2023-11-22T07:03:18Z","timestamp":1700636598000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-99-8311-7_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9789819983100","9789819983117"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-981-99-8311-7_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"21 November 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"APLAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Asian Symposium on Programming Languages and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Taipei","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Taiwan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 November 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 November 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"aplas2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/aplas-2023","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"HotCRP","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"32","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"15","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"47% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}