{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:03:12Z","timestamp":1762459392746,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":43,"publisher":"ACM","license":[{"start":{"date-parts":[[2016,9,5]],"date-time":"2016-09-05T00:00:00Z","timestamp":1473033600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["NSFC 61161130530"],"award-info":[{"award-number":["NSFC 61161130530"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-11-IS02-0002"],"award-info":[{"award-number":["ANR-11-IS02-0002"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,9,5]]},"DOI":"10.1145\/2967973.2968608","type":"proceedings-article","created":{"date-parts":[[2016,9,1]],"date-time":"2016-09-01T18:25:14Z","timestamp":1472754314000},"page":"174-187","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":21,"title":["The Bang Calculus"],"prefix":"10.1145","author":[{"given":"Thomas","family":"Ehrhard","sequence":"first","affiliation":[{"name":"Univ Paris Diderot, Sorbonne Paris Cit\u00e9, Paris, France"}]},{"given":"Giulio","family":"Guerrieri","sequence":"additional","affiliation":[{"name":"Aix Marseille Universit\u00e9, Marseille, France"}]}],"member":"320","published-online":{"date-parts":[[2016,9,5]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90181-R"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.08.006"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628154"},{"key":"e_1_3_2_1_4_1","volume-title":"Preservation of Strong Normalisation modulo permutations for the structural lambda-calculus. Logical Methods in Computer Science, 8(1)","author":"Accattoli B.","year":"2012","unstructured":"B. Accattoli and D. Kesner . Preservation of Strong Normalisation modulo permutations for the structural lambda-calculus. Logical Methods in Computer Science, 8(1) , 2012 . B. Accattoli and D. Kesner. Preservation of Strong Normalisation modulo permutations for the structural lambda-calculus. Logical Methods in Computer Science, 8(1), 2012."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29822-6_4"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199507"},{"key":"e_1_3_2_1_7_1","series-title":"Studies in Logic and the Foundation of Mathematics","volume-title":"Its Syntax and Semantics","author":"Barendregt H. P.","year":"1984","unstructured":"H. P. Barendregt . The Lambda Calculus : Its Syntax and Semantics , volume 103 of Studies in Logic and the Foundation of Mathematics . North-Holland , Amsterdam , 1984 . H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundation of Mathematics. North-Holland, Amsterdam, 1984."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/788018.788785"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(00)00056-7"},{"key":"e_1_3_2_1_10_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/978-3-642-54830-7_7","volume-title":"Foundations of Software Science and Computation Structures - FOSSACS","author":"Carraro A.","year":"2014","unstructured":"A. Carraro and G. Guerrieri . A semantical and operational account of call-by-value solvability . In A. Muscholl, editor, Foundations of Software Science and Computation Structures - FOSSACS 2014 , volume 8412 of Lecture Notes in Computer Science , pages 103 -- 118 . Springer , 2014. A. Carraro and G. Guerrieri. A semantical and operational account of call-by-value solvability. In A. Muscholl, editor, Foundations of Software Science and Computation Structures - FOSSACS 2014, volume 8412 of Lecture Notes in Computer Science, pages 103--118. Springer, 2014."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351262"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2011.02.001"},{"key":"e_1_3_2_1_14_1","volume-title":"Mathematical Structures in Computer Science","author":"de Carvalho D.","year":"2009","unstructured":"D. de Carvalho . Execution Time of lambda-Terms via Denotational Semantics and Intersection Types . Mathematical Structures in Computer Science , 2009 . To appear. D. de Carvalho. Execution Time of lambda-Terms via Denotational Semantics and Intersection Types. Mathematical Structures in Computer Science, 2009. To appear."},{"key":"e_1_3_2_1_15_1","volume-title":"The relational model is injective for Multiplicative Exponential Linear Logic. CoRR, abs\/1502.02404","author":"de Carvalho D.","year":"2015","unstructured":"D. de Carvalho . The relational model is injective for Multiplicative Exponential Linear Logic. CoRR, abs\/1502.02404 , 2015 . D. de Carvalho. The relational model is injective for Multiplicative Exponential Linear Logic. CoRR, abs\/1502.02404, 2015."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2012.01.004"},{"key":"e_1_3_2_1_17_1","first-page":"259","volume-title":"CSL","author":"Ehrhard T.","year":"2012","unstructured":"T. Ehrhard . Collapsing non-idempotent intersection types . In CSL , pages 259 -- 273 , 2012 . T. Ehrhard. Collapsing non-idempotent intersection types. In CSL, pages 259--273, 2012."},{"key":"e_1_3_2_1_18_1","volume-title":"Mathematical Structures in Computer Science","author":"Ehrhard T.","year":"2015","unstructured":"T. Ehrhard . An introduction to Differential Linear Logic: proof-nets, models and antiderivatives . Mathematical Structures in Computer Science , 2015 . To appear. T. Ehrhard. An introduction to Differential Linear Logic: proof-nets, models and antiderivatives. Mathematical Structures in Computer Science, 2015. To appear."},{"key":"e_1_3_2_1_19_1","volume-title":"ESOP 2016, Proceedings","volume":"9632","author":"Ehrhard T.","year":"2016","unstructured":"T. Ehrhard . Call-By-Push-Value from a Linear Logic point of view. In Programming Languages and Systems - 25th European Symposium on Programming , ESOP 2016, Proceedings , volume 9632 of Lecture Notes in Computer Science, pages 202--228. Springer , 2016 . T. Ehrhard. Call-By-Push-Value from a Linear Logic point of view. In Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016, Proceedings, volume 9632 of Lecture Notes in Computer Science, pages 202--228. Springer, 2016."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/11780342_20"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.08.003"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.06.001"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_3_2_1_24_1","first-page":"3","volume-title":"Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE 2015","volume":"46","author":"Guerrieri G.","year":"2015","unstructured":"G. Guerrieri . Head reduction and normalization in a call-by-value lambda-calculus. In N. Nishida et al., editors , Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE 2015 , volume 46 of OASICS, pages 3 -- 17 . Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik , 2015 . G. Guerrieri. Head reduction and normalization in a call-by-value lambda-calculus. In N. Nishida et al., editors, Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE 2015, volume 46 of OASICS, pages 3--17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015."},{"key":"e_1_3_2_1_25_1","first-page":"211","volume-title":"TLCA 2015","volume":"38","author":"Guerrieri G.","year":"2015","unstructured":"G. Guerrieri , L. Paolini , and S. Ronchi Della Rocca. Standardization of a Call-By-Value Lambda-Calculus. In T. Altenkirch, editor, Typed Lambda Calculi and Applications , TLCA 2015 , volume 38 of LIPIcs, pages 211 -- 225 . Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik , 2015 . G. Guerrieri, L. Paolini, and S. Ronchi Della Rocca. Standardization of a Call-By-Value Lambda-Calculus. In T. Altenkirch, editor, Typed Lambda Calculi and Applications, TLCA 2015, volume 38 of LIPIcs, pages 211--225. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015."},{"key":"e_1_3_2_1_26_1","first-page":"1","volume-title":"1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016","volume":"52","author":"Guerrieri G.","year":"2016","unstructured":"G. Guerrieri , L. Pellissier , and L. Tortora de Falco. Computing Connected Proof(-Structure)s From Their Taylor Expansion. In D. Kesner and B. Pientka, editors , 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016 , volume 52 of LIPIcs, pages 20: 1 -- 20 :18. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik , 2016 . G. Guerrieri, L. Pellissier, and L. Tortora de Falco. Computing Connected Proof(-Structure)s From Their Taylor Expansion. In D. Kesner and B. Pientka, editors, 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, volume 52 of LIPIcs, pages 20:1--20:18. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016."},{"key":"e_1_3_2_1_27_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"424","DOI":"10.1007\/978-3-662-49630-5_25","volume-title":"Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS","author":"Kesner D.","year":"2016","unstructured":"D. Kesner . Reasoning About Call-by-need by Means of Types . In B. Jacobs and C. L\u00f6ding, editors, Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS 2016 , Proceedings, volume 9634 of Lecture Notes in Computer Science , pages 424 -- 441 . Springer , 2016. D. Kesner. Reasoning About Call-by-need by Means of Types. In B. Jacobs and C. L\u00f6ding, editors, Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS 2016, Proceedings, volume 9634 of Lecture Notes in Computer Science, pages 424--441. Springer, 2016."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00297-3"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/788023.789038"},{"key":"e_1_3_2_1_30_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"228","DOI":"10.1007\/3-540-48959-2_17","volume-title":"J.-Y","author":"Levy P. B.","year":"1999","unstructured":"P. B. Levy . Call-by-Push-Value: A Subsuming Paradigm . In J.-Y . Girard, editor, Typed Lambda Calculi and Applications, TLCA'99, Proceedings , volume 1581 of Lecture Notes in Computer Science , pages 228 -- 242 . Springer , 1999 . P. B. Levy. Call-by-Push-Value: A Subsuming Paradigm. In J.-Y. Girard, editor, Typed Lambda Calculi and Applications, TLCA'99, Proceedings, volume 1581 of Lecture Notes in Computer Science, pages 228--242. Springer, 1999."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-0480-6"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1992.185536"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/2021953.2021969"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00358-2"},{"key":"e_1_3_2_1_35_1","series-title":"Panoramas et Synth\u00e8ses","volume-title":"Interactive models of computation and program behaviour","author":"Melli\u00e8s P.-A.","year":"2009","unstructured":"P.-A. Melli\u00e8s . Categorical semantics of linear logic . In Interactive models of computation and program behaviour , volume 27 of Panoramas et Synth\u00e8ses . Soci\u00e9t\u00e9 Math\u00e9matique de France , 2009 . P.-A. Melli\u00e8s. Categorical semantics of linear logic. In Interactive models of computation and program behaviour, volume 27 of Panoramas et Synth\u00e8ses. Soci\u00e9t\u00e9 Math\u00e9matique de France, 2009."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/77350.77353"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_3_2_1_38_1","volume-title":"FirstView:1--25","author":"Paolini L.","year":"2015","unstructured":"L. Paolini , M. Piccolo , and S. Ronchi Della Rocca. Essential and relational models. Mathematical Structures in Computer Science , FirstView:1--25 , 2015 . L. Paolini, M. Piccolo, and S. Ronchi Della Rocca. Essential and relational models. Mathematical Structures in Computer Science, FirstView:1--25, 2015."},{"issue":"6","key":"e_1_3_2_1_39_1","first-page":"507","volume":"33","author":"Paolini L.","year":"1999","unstructured":"L. Paolini and S . Ronchi Della Rocca. Call-by-value Solvability. ITA , 33 ( 6 ): 507 -- 534 , 1999 . L. Paolini and S. Ronchi Della Rocca. Call-by-value Solvability. ITA, 33(6):507--534, 1999.","journal-title":"Ronchi Della Rocca. Call-by-value Solvability. ITA"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"e_1_3_2_1_41_1","first-page":"7","article-title":"Lambda calcul et r\u00e9seaux. PhD thesis","author":"Regnier L.","year":"1992","unstructured":"L. Regnier . Lambda calcul et r\u00e9seaux. PhD thesis , Universit\u00e9 Paris 7 , 1992 . L. Regnier. Lambda calcul et r\u00e9seaux. PhD thesis, Universit\u00e9 Paris 7, 1992.","journal-title":"Universit\u00e9 Paris"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90012-4"},{"key":"e_1_3_2_1_43_1","volume-title":"The Parametric \u03bb-calculus: a Metamodel for Computation. Texts in Theoretical Computer Science","author":"della Rocca S. Ronchi","year":"2004","unstructured":"S. Ronchi della Rocca and L. Paolini . The Parametric \u03bb-calculus: a Metamodel for Computation. Texts in Theoretical Computer Science . Springer , Berlin , 2004 . S. Ronchi della Rocca and L. Paolini. The Parametric \u03bb-calculus: a Metamodel for Computation. Texts in Theoretical Computer Science. Springer, Berlin, 2004."},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1057"}],"event":{"name":"PPDP '16: 18th International Symposium on Principles and Practice of Declarative Programming","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Edinburgh United Kingdom","acronym":"PPDP '16"},"container-title":["Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2967973.2968608","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2967973.2968608","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T05:07:03Z","timestamp":1750223223000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2967973.2968608"}},"subtitle":["an untyped lambda-calculus generalizing call-by-name and call-by-value"],"short-title":[],"issued":{"date-parts":[[2016,9,5]]},"references-count":43,"alternative-id":["10.1145\/2967973.2968608","10.1145\/2967973"],"URL":"https:\/\/doi.org\/10.1145\/2967973.2968608","relation":{},"subject":[],"published":{"date-parts":[[2016,9,5]]},"assertion":[{"value":"2016-09-05","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}