{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,27]],"date-time":"2026-09-27T01:08:10Z","timestamp":1790471290797,"version":"4.1.0"},"reference-count":68,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T00:00:00Z","timestamp":1641945600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,1,16]]},"abstract":"<jats:p>This paper introduces a functional term calculus, called pn, that captures the essence of the operational semantics of Intuitionistic Linear Logic Proof-Nets with a faithful degree of granularity, both statically and dynamically. On the static side, we identify an equivalence relation on pn-terms which is sound and complete with respect to the classical notion of structural equivalence for proof-nets. On the dynamic side, we show that every single (exponential) step in the term calculus translates to a different single (exponential) step in the graphical formalism, thus capturing the original Girard\u2019s granularity of proof-nets but on the level of terms. We also show some fundamental properties of the calculus such as confluence, strong normalization, preservation of \u03b2-strong normalization and the existence of a strong bisimulation that captures pairs of pn-terms having the same graph reduction.<\/jats:p>","DOI":"10.1145\/3498669","type":"journal-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T17:03:12Z","timestamp":1642006992000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["A fine-grained computational interpretation of Girard\u2019s intuitionistic proof-nets"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4254-3129","authenticated-orcid":false,"given":"Delia","family":"Kesner","sequence":"first","affiliation":[{"name":"Universit\u00e9 de Paris, France \/ CNRS, France \/ IRIF, France \/ Institut Universitaire de France, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,1,12]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000186"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90181-R"},{"key":"e_1_2_2_3_1","unstructured":"Beniamino Accattoli. 2011. Jumping around the box: graphical and operational studies on Lambda Calculus and Linear Logic.. Universit\u00e0 di Roma La Sapienza.  Beniamino Accattoli. 2011. Jumping around the box: graphical and operational studies on Lambda Calculus and Linear Logic.. Universit\u00e0 di Roma La Sapienza."},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-02508-3_3"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628154"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535886"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04027-6_7"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15205-4_30"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(1:28)2012"},{"key":"e_1_2_2_10_1","unstructured":"1990. ACM Press. isbn:0-89791-343-4  1990. ACM Press. isbn:0-89791-343-4"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800001994"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2017.9"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0037099"},{"key":"e_1_2_2_14_1","volume-title":"Computing Science in the Netherlands","author":"Bloo Roel","unstructured":"Roel Bloo and Kristoffer Rose . 1995. Preservation of Strong Normalization in Named Lambda Calculi with Explicit Substitution and Garbage Collection . In Computing Science in the Netherlands . Netherlands Computer Science Research Foundation , 62\u201372. Roel Bloo and Kristoffer Rose. 1995. Preservation of Strong Normalization in Named Lambda Calculi with Explicit Substitution and Garbage Collection. In Computing Science in the Netherlands. Netherlands Computer Science Research Foundation, 62\u201372."},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.2307\/1968337"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90230-Y"},{"key":"e_1_2_2_17_1","unstructured":"Vincent Danos. 1990. La Logique Lin\u00e9aire appliqu\u00e9e \u00e0 l\u2019\u00e9tude de divers processus de normalisation (principalement du lambda-calcul). Universit\u00e9 Paris 7.  Vincent Danos. 1990. La Logique Lin\u00e9aire appliqu\u00e9e \u00e0 l\u2019\u00e9tude de divers processus de normalisation (principalement du lambda-calcul). Universit\u00e9 Paris 7."},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561456"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00049-3"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2505879.2505898"},{"key":"e_1_2_2_21_1","volume-title":"A namefree lambda calculus with facilities for internal definition of expressions and segments","author":"de Bruijn Nicolaas Govert","unstructured":"Nicolaas Govert de Bruijn . 1978. A namefree lambda calculus with facilities for internal definition of expressions and segments . Eindhoven University of Technology , Eindhoven . Nicolaas Govert de Bruijn. 1978. A namefree lambda calculus with facilities for internal definition of expressions and segments. Eindhoven University of Technology, Eindhoven."},{"key":"e_1_2_2_22_1","volume-title":"Notes in Pure and Applied Mathematics, 106)","author":"de Bruijn Nicolaas Govert","unstructured":"Nicolaas Govert de Bruijn . 1987. Generalizing Automath by Means of a Lambda-Typed Lambda Calculus . In Mathematical Logic and Theoretical Computer Science, Edgar G.K. Lopez-Escobar David W. Kueker and Carl H. Smith (Eds.) (Lecture Notes in Pure and Applied Mathematics, 106) . Marcel Dekker , 71\u201392. Nicolaas Govert de Bruijn. 1987. Generalizing Automath by Means of a Lambda-Typed Lambda Calculus. In Mathematical Logic and Theoretical Computer Science, Edgar G.K. Lopez-Escobar David W. Kueker and Carl H. Smith (Eds.) (Lecture Notes in Pure and Applied Mathematics, 106). Marcel Dekker, 71\u201392."},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014040"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500000505"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1997.614927"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129502003791"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014050"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.08.003"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exs021"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49019-1"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/8.1.7"},{"key":"e_1_2_2_32_1","doi-asserted-by":"crossref","unstructured":"Jean-Yves Girard. 1988. Geometry of interaction 1: Interpretation of System F. In Logic Colloquium 88. North Holland.  Jean-Yves Girard. 1988. Geometry of interaction 1: Interpretation of System F. In Logic Colloquium 88. North Holland.","DOI":"10.1016\/S0049-237X(08)70271-4"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52335-9_49"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_2_2_35_1","volume-title":"Proof-nets: The parallel syntax for proof-theory (Lecture Notes in Pure Applied Mathematics","author":"Girard Jean-Yves","year":"1996","unstructured":"Jean-Yves Girard . 1996 . Proof-nets: The parallel syntax for proof-theory (Lecture Notes in Pure Applied Mathematics , Vol. 180). CRC Press, Boca Raton, FL, USA. 97\u2013 124 . Jean-Yves Girard. 1996. Proof-nets: The parallel syntax for proof-theory (Lecture Notes in Pure Applied Mathematics, Vol. 180). CRC Press, Boca Raton, FL, USA. 97\u2013124."},{"key":"e_1_2_2_36_1","volume-title":"Proof-nets: The parallel syntax for proof-theory. In Logic and Algebra","author":"Girard Jean-Yves","year":"1996","unstructured":"Jean-Yves Girard . 1996 . Proof-nets: The parallel syntax for proof-theory. In Logic and Algebra . Marcel Dekker , 97\u2013124. Jean-Yves Girard. 1996. Proof-nets: The parallel syntax for proof-theory. In Logic and Algebra. Marcel Dekker, 97\u2013124."},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96714"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.37"},{"key":"e_1_2_2_39_1","volume-title":"France-Japan Artificial Intelligence and Computer Science Symposium. 1\u201325","author":"Hardin Th\u00e9r\u00e8se","year":"1989","unstructured":"Th\u00e9r\u00e8se Hardin and Jean-Jacques L\u00e9vy . 1989 . A Confluent Calculus of Substitutions . In France-Japan Artificial Intelligence and Computer Science Symposium. 1\u201325 . Th\u00e9r\u00e8se Hardin and Jean-Jacques L\u00e9vy. 1989. A Confluent Calculus of Substitutions. In France-Japan Artificial Intelligence and Computer Science Symposium. 1\u201325."},{"key":"e_1_2_2_40_1","volume-title":"Morris","author":"Henderson Peter","year":"1976","unstructured":"Peter Henderson and James H . Morris . 1976 . A Lazy Evaluator. In 3rd ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages (POPL), Susan L. Graham, Robert M. Graham, Michael A. Harrison, William I. Grosky, and Jeffrey D. Ullman (Eds.). ACM Press , 95\u2013103. Peter Henderson and James H. Morris. 1976. A Lazy Evaluator. In 3rd ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages (POPL), Susan L. Graham, Robert M. Graham, Michael A. Harrison, William I. Grosky, and Jeffrey D. Ullman (Eds.). ACM Press, 95\u2013103."},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0022247"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1094622.1094629"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0026813"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74915-8_20"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2020.4"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_30"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-007-9018-9"},{"key":"e_1_2_2_48_1","unstructured":"Ambroise Lafont. 2019. Signatures and models for syntax and operational semantics in the presence of variable binding. L\u2019\u00c9cole Nationale Superieure Mines-Telecom Atlantique Bretagne Pays de la Loire - IMT Atlantique.  Ambroise Lafont. 2019. Signatures and models for syntax and operational semantics in the presence of variable binding. L\u2019\u00c9cole Nationale Superieure Mines-Telecom Atlantique Bretagne Pays de la Loire - IMT Atlantique."},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96711"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/6.4.308"},{"key":"e_1_2_2_51_1","unstructured":"Olivier Laurent. 2002. Etude de la polarisation en logique. Universit\u00e9 Aix-Marseille II.  Olivier Laurent. 2002. Etude de la polarisation en logique. Universit\u00e9 Aix-Marseille II."},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00297-3"},{"key":"e_1_2_2_53_1","unstructured":"Xavier Leroy. 1990. The ZINC Experiment: an economical implementation of the ML language. INRIA Rocquencourt.  Xavier Leroy. 1990. The ZINC Experiment: an economical implementation of the ML language. INRIA Rocquencourt."},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289434"},{"key":"e_1_2_2_55_1","unstructured":"Per Martin-L\u00f6f. 1972. An intuitionistic theory of types. Unpublished.  Per Martin-L\u00f6f. 1972. An intuitionistic theory of types. Unpublished."},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014062"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.07.035"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2017.32"},{"key":"e_1_2_2_59_1","volume-title":"The fine-structure of lambda calculus","author":"Nederpelt P.","unstructured":"Robert. P. Nederpelt . 1992. The fine-structure of lambda calculus . Eindhoven University of Technology , Department of Mathematics and Computer Science. Robert. P. Nederpelt. 1992. The fine-structure of lambda calculus. Eindhoven University of Technology, Department of Mathematics and Computer Science."},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0013061"},{"key":"e_1_2_2_61_1","unstructured":"Laurent Regnier. 1992. Lambda-calcul et r\u00e9seaux. Universit\u00e9 Paris 7.  Laurent Regnier. 1992. Lambda-calcul et r\u00e9seaux. Universit\u00e9 Paris 7."},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90012-4"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48959-2_23"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56393-8_3"},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796897002712"},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58140-5_30"},{"key":"e_1_2_2_67_1","volume-title":"Term Rewriting Systems","unstructured":"Terese. 2003. Term Rewriting Systems (Cambridge Tracts in Theoretical Computer Science , Vol. 55). Cambridge University Press. Terese. 2003. Term Rewriting Systems (Cambridge Tracts in Theoretical Computer Science, Vol. 55). Cambridge University Press."},{"key":"e_1_2_2_68_1","volume-title":"Semantics and Pragmatics of the Lambda Calculus","author":"Wadsworth Christopher","unstructured":"Christopher Wadsworth . 1971. Semantics and Pragmatics of the Lambda Calculus . Oxford University . Christopher Wadsworth. 1971. Semantics and Pragmatics of the Lambda Calculus. Oxford University."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498669","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498669","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:27Z","timestamp":1750188627000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498669"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,12]]},"references-count":68,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2022,1,16]]}},"alternative-id":["10.1145\/3498669"],"URL":"https:\/\/doi.org\/10.1145\/3498669","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,1,12]]},"assertion":[{"value":"2022-01-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}