{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T20:29:55Z","timestamp":1770236995164,"version":"3.49.0"},"reference-count":99,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2023,1,9]],"date-time":"2023-01-09T00:00:00Z","timestamp":1673222400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["GA 818616"],"award-info":[{"award-number":["GA 818616"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,1,9]]},"abstract":"<jats:p>We introduce a general theory of quantitative and metric rewriting systems, namely systems with a rewriting  \nrelation enriched over quantales modelling abstract quantities. We develop theories of abstract and term-based  \nsystems, refining cornerstone results of rewriting theory (such as Newman\u2019s Lemma, Church-Rosser Theorem,  \nand critical pair-like lemmas) to a metric and quantitative setting. To avoid distance trivialisation and lack of  \nconfluence issues, we introduce non-expansive, linear term rewriting systems, and then generalise the latter  \nto the novel class of graded term rewriting systems. These systems make quantitative rewriting modal and  \ncontext-sensitive, this way endowing rewriting with coeffectful behaviours.<\/jats:p>","DOI":"10.1145\/3571256","type":"journal-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T21:58:14Z","timestamp":1673474294000},"page":"1832-1863","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Elements of Quantitative Rewriting"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2159-0615","authenticated-orcid":false,"given":"Francesco","family":"Gavazzo","sequence":"first","affiliation":[{"name":"University of Pisa, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8927-7414","authenticated-orcid":false,"given":"Cecilia","family":"Di Florio","sequence":"additional","affiliation":[{"name":"University of Bologna, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Abadi Mart\u00edn","year":"1999","unstructured":"Mart\u00edn Abadi , Anindya Banerjee , Nevin Heintze , and Jon G. Riecke . 1999. A Core Calculus of Dependency. In POPL \u201999 , Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages , San Antonio, TX, USA , January 20-22, 1999 . 147\u2013160. Mart\u00edn Abadi, Anindya Banerjee, Nevin Heintze, and Jon G. Riecke. 1999. A Core Calculus of Dependency. In POPL \u201999, Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Antonio, TX, USA, January 20-22, 1999. 147\u2013160."},{"key":"e_1_2_1_2_1","volume-title":"Proc. ACM Program. Lang., 4, ICFP","author":"Abel Andreas","year":"2020","unstructured":"Andreas Abel and Jean-Philippe Bernardy . 2020 . A unified view of modalities in type systems . Proc. ACM Program. Lang., 4, ICFP (2020), 90:1\u201390:28. Andreas Abel and Jean-Philippe Bernardy. 2020. A unified view of modalities in type systems. Proc. ACM Program. Lang., 4, ICFP (2020), 90:1\u201390:28."},{"key":"e_1_2_1_3_1","unstructured":"Samson Abramsky. 2002. Predicative Copying and Polynomial Time. Clifford Lectures Tulane. \t\t\t\t  Samson Abramsky. 2002. Predicative Copying and Polynomial Time. Clifford Lectures Tulane."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129502003730"},{"key":"e_1_2_1_5_1","unstructured":"Peter Aczel. 1978. A general Church-Rosser theorem. Draft Manchester. \t\t\t\t  Peter Aczel. 1978. A general Church-Rosser theorem. Draft Manchester."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(80)90045-6"},{"key":"e_1_2_1_7_1","volume-title":"The optimal implementation of functional programming languages","author":"Asperti Andrea","unstructured":"Andrea Asperti and Stefano Guerrini . 1998. The optimal implementation of functional programming languages ( Cambridge tracts in theoretical computer science, Vol. 45). Cambridge University Press. Andrea Asperti and Stefano Guerrini. 1998. The optimal implementation of functional programming languages (Cambridge tracts in theoretical computer science, Vol. 45). Cambridge University Press."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209189"},{"key":"e_1_2_1_9_1","volume-title":"Ugo Dal Lago, and Akihisa Yamada","author":"Avanzini Martin","year":"2020","unstructured":"Martin Avanzini , Ugo Dal Lago, and Akihisa Yamada . 2020 . On probabilistic term rewriting. Sci. Comput. Program ., 185 (2020). Martin Avanzini, Ugo Dal Lago, and Akihisa Yamada. 2020. On probabilistic term rewriting. Sci. Comput. Program., 185 (2020)."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1017\/9781108770750.011"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209177"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CALCO.2021.7"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-47797-7_4"},{"key":"e_1_2_1_14_1","volume-title":"Proc. of FSTTCS. 403\u2013415","author":"Baldan Paolo","year":"2014","unstructured":"Paolo Baldan , Filippo Bonchi , Henning Kerstan , and Barbara K\u00f6nig . 2014 . Behavioral Metrics via Functor Lifting . In Proc. of FSTTCS. 403\u2013415 . Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara K\u00f6nig. 2014. Behavioral Metrics via Functor Lifting. In Proc. of FSTTCS. 403\u2013415."},{"key":"e_1_2_1_15_1","volume-title":"Proc. of CALCO","author":"Baldan Paolo","year":"2015","unstructured":"Paolo Baldan , Filippo Bonchi , Henning Kerstan , and Barbara K\u00f6nig . 2015 . Towards Trace Metrics via Functor Lifting . In Proc. of CALCO 2015. 35\u201349. Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara K\u00f6nig. 2015. Towards Trace Metrics via Functor Lifting. In Proc. of CALCO 2015. 35\u201349."},{"key":"e_1_2_1_16_1","unstructured":"H.P. Barendregt. 1984. The lambda calculus: its syntax and semantics. North-Holland. \t\t\t\t  H.P. Barendregt. 1984. The lambda calculus: its syntax and semantics. North-Holland."},{"key":"e_1_2_1_17_1","volume-title":"Fuzzy Relational Systems: Foundations and Principles","author":"Belohl\u00e1vek R.","unstructured":"R. Belohl\u00e1vek . 2002. Fuzzy Relational Systems: Foundations and Principles . Springer US. R. Belohl\u00e1vek. 2002. Fuzzy Relational Systems: Foundations and Principles. Springer US."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/FUZZY.2009.5277248"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ins.2010.04.007"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/b105121"},{"key":"e_1_2_1_21_1","volume-title":"Simon Peyton Jones, and Arnaud Spiwack","author":"Bernardy Jean-Philippe","year":"2018","unstructured":"Jean-Philippe Bernardy , Mathieu Boespflug , Ryan R. Newton , Simon Peyton Jones, and Arnaud Spiwack . 2018 . Linear Haskell: practical linearity in a higher-order polymorphic language. PACMPL, 2, POPL ( 2018), 5:1\u20135:29. Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon Peyton Jones, and Arnaud Spiwack. 2018. Linear Haskell: practical linearity in a higher-order polymorphic language. PACMPL, 2, POPL (2018), 5:1\u20135:29."},{"key":"e_1_2_1_22_1","volume-title":"Term Rewriting Systems","author":"Bezem M.","unstructured":"M. Bezem , J.W. Klop , E. Barendsen , R. de Vrijer , and Terese. 2003. Term Rewriting Systems . Cambridge University Press . M. Bezem, J.W. Klop, E. Barendsen, R. de Vrijer, and Terese. 2003. Term Rewriting Systems. Cambridge University Press."},{"key":"e_1_2_1_23_1","volume-title":"Bird and Oege de Moor","author":"Richard","year":"1997","unstructured":"Richard S. Bird and Oege de Moor . 1997 . Algebra of programming. Prentice Hall . Richard S. Bird and Oege de Moor. 1997. Algebra of programming. Prentice Hall."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(97)00042-X"},{"key":"e_1_2_1_25_1","doi-asserted-by":"crossref","unstructured":"R.V. Book and F. Otto. 1993. String-rewriting Systems. Springer-Verlag. \t\t\t\t  R.V. Book and F. Otto. 1993. String-rewriting Systems. Springer-Verlag.","DOI":"10.1007\/978-1-4613-9771-7"},{"key":"e_1_2_1_26_1","volume-title":"Proc. of ESOP","author":"Brunel Alo\u00efs","year":"2014","unstructured":"Alo\u00efs Brunel , Marco Gaboardi , Damiano Mazza , and Steve Zdancewic . 2014 . A Core Quantitative Coeffect Calculus . In Proc. of ESOP 2014. 351\u2013370. Alo\u00efs Brunel, Marco Gaboardi, Damiano Mazza, and Steve Zdancewic. 2014. A Core Quantitative Coeffect Calculus. In Proc. of ESOP 2014. 351\u2013370."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434331"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1936-1501858-0"},{"key":"e_1_2_1_29_1","volume-title":"Proc. of ESOP","author":"Crubill\u00e9 R.","year":"2014","unstructured":"R. Crubill\u00e9 and U. Dal Lago . 2014. On Probabilistic Applicative Bisimulation and Call-by-Value lambda-Calculi . In Proc. of ESOP 2014 . 209\u2013228. R. Crubill\u00e9 and U. Dal Lago. 2014. On Probabilistic Applicative Bisimulation and Call-by-Value lambda-Calculi. In Proc. of ESOP 2014. 209\u2013228."},{"key":"e_1_2_1_30_1","volume-title":"Proc. of LICS","author":"Crubill\u00e9 R.","year":"2015","unstructured":"R. Crubill\u00e9 and U. Dal Lago . 2015. Metric Reasoning about lambda-Terms: The Affine Case . In Proc. of LICS 2015 . 633\u2013644. R. Crubill\u00e9 and U. Dal Lago. 2015. Metric Reasoning about lambda-Terms: The Affine Case. In Proc. of LICS 2015. 633\u2013644."},{"key":"e_1_2_1_31_1","volume-title":"Proc. of ESOP","author":"Crubill\u00e9 R.","year":"2017","unstructured":"R. Crubill\u00e9 and U. Dal Lago . 2017. Metric Reasoning About lambda-Terms: The General Case . In Proc. of ESOP 2017 . 341\u2013367. R. Crubill\u00e9 and U. Dal Lago. 2017. Metric Reasoning About lambda-Terms: The General Case. In Proc. of ESOP 2017. 341\u2013367."},{"key":"e_1_2_1_32_1","unstructured":"H.B. Curry and R. Feys. 1958. Combinatory Logic (Combinatory Logic). North-Holland Publishing Company. \t\t\t\t  H.B. Curry and R. Feys. 1958. Combinatory Logic (Combinatory Logic). North-Holland Publishing Company."},{"key":"e_1_2_1_33_1","unstructured":"H.B. Curry and R. Feys. 1958. Combinatory Logic (Combinatory Logic). North-Holland Publishing Company. \t\t\t\t  H.B. Curry and R. Feys. 1958. Combinatory Logic (Combinatory Logic). North-Holland Publishing Company."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3531130.3533337"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2022.16"},{"key":"e_1_2_1_36_1","volume-title":"Proc. of ESOP","author":"Lago Ugo Dal","year":"2019","unstructured":"Ugo Dal Lago and Francesco Gavazzo . 2019 . Effectful Normal Form Bisimulation . In Proc. of ESOP 2019. 263\u2013292. Ugo Dal Lago and Francesco Gavazzo. 2019. Effectful Normal Form Bisimulation. In Proc. of ESOP 2019. 263\u2013292."},{"key":"e_1_2_1_37_1","volume-title":"Proc. of ICTCS","author":"Lago Ugo Dal","year":"2020","unstructured":"Ugo Dal Lago and Francesco Gavazzo . 2020 . Differential Logical Relations Part II: Increments and Derivatives . In Proc. of ICTCS 2020. 101\u2013114. Ugo Dal Lago and Francesco Gavazzo. 2020. Differential Logical Relations Part II: Increments and Derivatives. In Proc. of ICTCS 2020. 101\u2013114."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2021.09.027"},{"key":"e_1_2_1_39_1","volume-title":"via Lawvere. CoRR, abs\/2103.03871","author":"Lago Ugo Dal","year":"2021","unstructured":"Ugo Dal Lago and Francesco Gavazzo . 2021. Modal Reasoning = Metric Reasoning , via Lawvere. CoRR, abs\/2103.03871 ( 2021 ), arXiv:2103.03871. arxiv:2103.03871 Ugo Dal Lago and Francesco Gavazzo. 2021. Modal Reasoning = Metric Reasoning, via Lawvere. CoRR, abs\/2103.03871 (2021), arXiv:2103.03871. arxiv:2103.03871"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498680"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498692"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICALP.2019.111"},{"key":"e_1_2_1_43_1","volume-title":"Proc. of POPL","author":"de Amorim A.A.","year":"2017","unstructured":"A.A. de Amorim , M. Gaboardi , J. Hsu , S. Katsumata , and I. Cherigui . 2017. A semantic account of metric preservation . In Proc. of POPL 2017 . 545\u2013556. A.A. de Amorim, M. Gaboardi, J. Hsu, S. Katsumata, and I. Cherigui. 2017. A semantic account of metric preservation. In Proc. of POPL 2017. 545\u2013556."},{"key":"e_1_2_1_44_1","doi-asserted-by":"crossref","unstructured":"J.W. de Bakker and J.I. Zucker. 1982. Denotational Semantics of Concurrency. In STOC. 153\u2013158. \t\t\t\t  J.W. de Bakker and J.I. Zucker. 1982. Denotational Semantics of Concurrency. In STOC. 153\u2013158.","DOI":"10.1145\/800070.802188"},{"key":"e_1_2_1_45_1","doi-asserted-by":"crossref","unstructured":"M.M. Deza and E. Deza. 2009. Encyclopedia of Distances. Springer Berlin Heidelberg. \t\t\t\t  M.M. Deza and E. Deza. 2009. Encyclopedia of Distances. Springer Berlin Heidelberg.","DOI":"10.1007\/978-3-642-00234-2"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(96)00154-5"},{"key":"e_1_2_1_47_1","volume-title":"Proc. of SETTA","author":"Du W.","year":"2016","unstructured":"W. Du , Y. Deng , and D. Gebler . 2016. Behavioural Pseudometrics for Nondeterministic Probabilistic Systems . In Proc. of SETTA 2016 . 67\u201384. W. Du, Y. Deng, and D. Gebler. 2016. Behavioural Pseudometrics for Nondeterministic Probabilistic Systems. In Proc. of SETTA 2016. 67\u201384."},{"key":"e_1_2_1_48_1","volume-title":"Workshop on Realizability Semantics and Applications.","author":"Escardo M.H.","year":"1999","unstructured":"M.H. Escardo . 1999 . A metric model of PCF . In Workshop on Realizability Semantics and Applications. M.H. Escardo. 1999. A metric model of PCF. In Workshop on Realizability Semantics and Applications."},{"key":"e_1_2_1_49_1","volume-title":"Metrics for Finite Markov Decision Processes. In Prof. of UAI","author":"Ferns N.","year":"2004","unstructured":"N. Ferns , P Panangaden , and D. Precup . 2004 . Metrics for Finite Markov Decision Processes. In Prof. of UAI 2004 . 162\u2013169. N. Ferns, P Panangaden, and D. Precup. 2004. Metrics for Finite Markov Decision Processes. In Prof. of UAI 2004. 162\u2013169."},{"key":"e_1_2_1_50_1","volume-title":"Metrics for Markov Decision Processes with Infinite State Spaces. In Prof. of UAI","author":"Ferns N.","year":"2005","unstructured":"N. Ferns , P Panangaden , and D. Precup . 2005 . Metrics for Markov Decision Processes with Infinite State Spaces. In Prof. of UAI 2005 . 201\u2013208. N. Ferns, P Panangaden, and D. Precup. 2005. Metrics for Markov Decision Processes with Infinite State Spaces. In Prof. of UAI 2005. 201\u2013208."},{"key":"e_1_2_1_51_1","volume-title":"AMS Conference proceedings. 13","author":"Flagg Robert C","year":"1992","unstructured":"Robert C Flagg . 1992 . Completeness in continuity spaces . In AMS Conference proceedings. 13 , 183\u2013199. Robert C Flagg. 1992. Completeness in continuity spaces. In AMS Conference proceedings. 13, 183\u2013199."},{"key":"e_1_2_1_52_1","volume-title":"Freyd and Andre Scedrov","author":"Peter","year":"1990","unstructured":"Peter J. Freyd and Andre Scedrov . 1990 . Categories, allegories (North-Holland mathematical library, Vol. 39). North-Holland. Peter J. Freyd and Andre Scedrov. 1990. Categories, allegories (North-Holland mathematical library, Vol. 39). North-Holland."},{"key":"e_1_2_1_53_1","volume-title":"Proc. of ICFP","author":"Gaboardi Marco","year":"2016","unstructured":"Marco Gaboardi , Shin-ya Katsumata, Dominic A. Orchard , Flavien Breuvart , and Tarmo Uustalu . 2016 . Combining effects and coeffects via grading . In Proc. of ICFP 2016. 476\u2013489. Marco Gaboardi, Shin-ya Katsumata, Dominic A. Orchard, Flavien Breuvart, and Tarmo Uustalu. 2016. Combining effects and coeffects via grading. In Proc. of ICFP 2016. 476\u2013489."},{"key":"e_1_2_1_54_1","volume-title":"Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2018","author":"Gavazzo Francesco","year":"2018","unstructured":"Francesco Gavazzo . 2018 . Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances . In Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2018 , Oxford, UK , July 09-12, 2018. 452\u2013461. Francesco Gavazzo. 2018. Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances. In Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018. 452\u2013461."},{"key":"e_1_2_1_55_1","volume-title":"Coinductive Equivalences and Metrics for Higher-order Languages with Algebraic Effects. Ph. D. Dissertation","author":"Gavazzo Francesco","unstructured":"Francesco Gavazzo . 2019. Coinductive Equivalences and Metrics for Higher-order Languages with Algebraic Effects. Ph. D. Dissertation . University of Bologna , Italy. http:\/\/amsdottorato.unibo.it\/9075\/ Francesco Gavazzo. 2019. Coinductive Equivalences and Metrics for Higher-order Languages with Algebraic Effects. Ph. D. Dissertation. University of Bologna, Italy. http:\/\/amsdottorato.unibo.it\/9075\/"},{"key":"e_1_2_1_56_1","volume-title":"Non-Expansive, and Graded Systems. CoRR, abs\/2206.13610","author":"Gavazzo Francesco","year":"2022","unstructured":"Francesco Gavazzo and Cecilia Di Florio . 2022. Quantitative and Metric Rewriting: Abstract , Non-Expansive, and Graded Systems. CoRR, abs\/2206.13610 ( 2022 ), https:\/\/doi.org\/10.48550\/arXiv.2206.13610 10.48550\/arXiv.2206.13610 Francesco Gavazzo and Cecilia Di Florio. 2022. Quantitative and Metric Rewriting: Abstract, Non-Expansive, and Graded Systems. CoRR, abs\/2206.13610 (2022), https:\/\/doi.org\/10.48550\/arXiv.2206.13610"},{"key":"e_1_2_1_57_1","doi-asserted-by":"crossref","unstructured":"D. Gebler Larsen. K.G. and S. Tini. 2016. Compositional bisimulation metric reasoning with Probabilistic Process Calculi. Logical Methods in Computer Science 12 4 (2016). \t\t\t\t  D. Gebler Larsen. K.G. and S. Tini. 2016. Compositional bisimulation metric reasoning with Probabilistic Process Calculi. Logical Methods in Computer Science 12 4 (2016).","DOI":"10.2168\/LMCS-12(4:12)2016"},{"key":"e_1_2_1_58_1","volume-title":"ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings. 331\u2013350","author":"Dan","unstructured":"Dan R. Ghica and Alex I. Smith. 2014. Bounded Linear Types in a Resource Semiring. In Programming Languages and Systems - 23rd European Symposium on Programming , ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings. 331\u2013350 . Dan R. Ghica and Alex I. Smith. 2014. Bounded Linear Types in a Resource Semiring. In Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings. 331\u2013350."},{"key":"e_1_2_1_59_1","volume-title":"Algorithms on Strings, Trees, and Sequences: Computer Science and Computational Biology","author":"Gusfield D.","unstructured":"D. Gusfield . 1997. Algorithms on Strings, Trees, and Sequences: Computer Science and Computational Biology . Cambridge University Press . D. Gusfield. 1997. Algorithms on Strings, Trees, and Sequences: Computer Science and Computational Biology. Cambridge University Press."},{"key":"e_1_2_1_60_1","volume-title":"Metamathematics of Fuzzy Logic","author":"H\u00e1jek P.","unstructured":"P. H\u00e1jek . 1998. Metamathematics of Fuzzy Logic . Springer Netherlands . P. H\u00e1jek. 1998. Metamathematics of Fuzzy Logic. Springer Netherlands."},{"key":"e_1_2_1_61_1","volume-title":"The Church-Rosser Property and a Result in Combinatory Logic. Ph. D. Dissertation","author":"Hindley J.R.","unstructured":"J.R. Hindley . 1964. The Church-Rosser Property and a Result in Combinatory Logic. Ph. D. Dissertation . University of Newcastle-upon-Tyne . J.R. Hindley. 1964. The Church-Rosser Property and a Result in Combinatory Logic. Ph. D. Dissertation. University of Newcastle-upon-Tyne."},{"key":"e_1_2_1_62_1","volume-title":"Basic Simple Type Theory","author":"Hindley J.R.","unstructured":"J.R. Hindley . 2008. Basic Simple Type Theory . Cambridge University Press . J.R. Hindley. 2008. Basic Simple Type Theory. Cambridge University Press."},{"key":"e_1_2_1_63_1","doi-asserted-by":"crossref","unstructured":"J.R. Hindley and J.P. Seldin. 2008. Lambda-Calculus and Combinators: An Introduction. Cambridge University Press. \t\t\t\t  J.R. Hindley and J.P. Seldin. 2008. Lambda-Calculus and Combinators: An Introduction. Cambridge University Press.","DOI":"10.1017\/CBO9780511809835"},{"key":"e_1_2_1_64_1","volume-title":"A Categorical Approach to Order, Metric, and Topology","author":"Topology Monoidal","unstructured":"2014. Monoidal Topology . A Categorical Approach to Order, Metric, and Topology , D. Hofmann, G.J. Seal, and W. Tholen (Eds.) (Encyclopedia of Mathematics and its Applications). Cambridge University Press . 2014. Monoidal Topology. A Categorical Approach to Order, Metric, and Topology, D. Hofmann, G.J. Seal, and W. Tholen (Eds.) (Encyclopedia of Mathematics and its Applications). Cambridge University Press."},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/322217.322230"},{"key":"e_1_2_1_66_1","volume-title":"The Implementation of Functional Programming Languages","author":"Peyton Jones Simon L.","unstructured":"Simon L. Peyton Jones . 1987. The Implementation of Functional Programming Languages . Prentice-Hall . Simon L. Peyton Jones. 1987. The Implementation of Functional Programming Languages. Prentice-Hall."},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02924844"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934518"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005102"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-14(3:19)2018"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470662"},{"key":"e_1_2_1_72_1","volume-title":"Linearity and Uniqueness: An Entente Cordiale","author":"Marshall Daniel","unstructured":"Daniel Marshall , Michael Vollmer , and Dominic Orchard . 2022. Linearity and Uniqueness: An Entente Cordiale . In Programming Languages and Systems, Ilya Sergey (Ed.). Springer International Publishing , Cham . 346\u2013375. Daniel Marshall, Michael Vollmer, and Dominic Orchard. 2022. Linearity and Uniqueness: An Entente Cordiale. In Programming Languages and Systems, Ilya Sergey (Ed.). Springer International Publishing, Cham. 346\u2013375."},{"key":"e_1_2_1_73_1","volume-title":"The Stanford Encyclopedia of Philosophy (Summer 2011 ed.), Edward N","author":"Meier-Oeser Stephan","unstructured":"Stephan Meier-Oeser . 2011. Medieval Semiotics . In The Stanford Encyclopedia of Philosophy (Summer 2011 ed.), Edward N . Zalta (Ed.). Metaphysics Research Lab, Stanford University . Stephan Meier-Oeser. 2011. Medieval Semiotics. In The Stanford Encyclopedia of Philosophy (Summer 2011 ed.), Edward N. Zalta (Ed.). Metaphysics Research Lab, Stanford University."},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470717"},{"key":"e_1_2_1_75_1","volume-title":"Beyond Nonexpansive Operations in Quantitative Algebraic Reasoning. CoRR, abs\/2201.09087","author":"Mio Matteo","year":"2022","unstructured":"Matteo Mio , Ralph Sarkis , and Valeria Vignudelli . 2022. Beyond Nonexpansive Operations in Quantitative Algebraic Reasoning. CoRR, abs\/2201.09087 ( 2022 ), arxiv:2201.09087 Matteo Mio, Ralph Sarkis, and Valeria Vignudelli. 2022. Beyond Nonexpansive Operations in Quantitative Algebraic Reasoning. CoRR, abs\/2201.09087 (2022), arxiv:2201.09087"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2019.102306"},{"key":"e_1_2_1_77_1","unstructured":"J.R. Munkres. 2000. Topology. Prentice Hall Incorporated. \t\t\t\t  J.R. Munkres. 2000. Topology. Prentice Hall Incorporated."},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66167-4_8"},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.2307\/1968867"},{"key":"e_1_2_1_80_1","volume-title":"Proc. ACM Program. Lang., 3, ICFP","author":"Orchard Dominic","year":"2019","unstructured":"Dominic Orchard , Vilem-Benjamin Liepelt , and Harley Eades III. 2019 . Quantitative Program Reasoning with Graded Modal Types . Proc. ACM Program. Lang., 3, ICFP (2019), Article 110, 110:1\u2013110:30 pages. Dominic Orchard, Vilem-Benjamin Liepelt, and Harley Eades III. 2019. Quantitative Program Reasoning with Graded Modal Types. Proc. ACM Program. Lang., 3, ICFP (2019), Article 110, 110:1\u2013110:30 pages."},{"key":"e_1_2_1_81_1","volume-title":"Proc. of ICFP","author":"Petricek Tomas","year":"2014","unstructured":"Tomas Petricek , Dominic A. Orchard , and Alan Mycroft . 2014 . Coeffects: a calculus of context-dependent computation . In Proc. of ICFP 2014. 123\u2013135. Tomas Petricek, Dominic A. Orchard, and Alan Mycroft. 2014. Coeffects: a calculus of context-dependent computation. In Proc. of ICFP 2014. 123\u2013135."},{"key":"e_1_2_1_82_1","volume-title":"Proc. of ICFP","author":"Reed J.","year":"2010","unstructured":"J. Reed and B.C. Pierce . 2010. Distance makes the types grow stronger: a calculus for differential privacy . In Proc. of ICFP 2010 . 157\u2013168. J. Reed and B.C. Pierce. 2010. Distance makes the types grow stronger: a calculus for differential privacy. In Proc. of ICFP 2010. 157\u2013168."},{"key":"e_1_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.1017\/9781108936880"},{"key":"e_1_2_1_84_1","doi-asserted-by":"publisher","DOI":"10.1145\/800161.805157"},{"key":"e_1_2_1_85_1","unstructured":"K.I. Rosenthal. 1990. Quantales and their applications. Longman Scientific & Technical. \t\t\t\t  K.I. Rosenthal. 1990. Quantales and their applications. Longman Scientific & Technical."},{"key":"e_1_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00649991"},{"key":"e_1_2_1_87_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00650498"},{"key":"e_1_2_1_88_1","volume-title":"Meyer","author":"Routley Richard","year":"1973","unstructured":"Richard Routley and Robert K . Meyer . 1973 . The Semantics of Entailment. In Truth, Syntax and Modality, Hugues Leblanc (Ed.) (Studies in Logic and the Foundations of Mathematics , Vol. 68). Elsevier, 199 \u2013 243. Richard Routley and Robert K. Meyer. 1973. The Semantics of Entailment. In Truth, Syntax and Modality, Hugues Leblanc (Ed.) (Studies in Logic and the Foundations of Mathematics, Vol. 68). Elsevier, 199 \u2013 243."},{"key":"e_1_2_1_89_1","volume-title":"Higher Order Operational Techniques in Semantics","author":"Sands D.","unstructured":"D. Sands . 1998. Improvement Theory and Its Applications . In Higher Order Operational Techniques in Semantics , A. D. Gordon and A. M. Pitts (Eds.). Cambridge University Press , 275\u2013306. D. Sands. 1998. Improvement Theory and Its Applications. In Higher Order Operational Techniques in Semantics, A. D. Gordon and A. M. Pitts (Eds.). Cambridge University Press, 275\u2013306."},{"key":"e_1_2_1_90_1","volume-title":"Relational Mathematics (Encyclopedia of Mathematics and its Applications","author":"Schmidt Gunther","unstructured":"Gunther Schmidt . 2011. Relational Mathematics (Encyclopedia of Mathematics and its Applications , Vol. 132). Cambridge University Press. Gunther Schmidt. 2011. Relational Mathematics (Encyclopedia of Mathematics and its Applications, Vol. 132). Cambridge University Press."},{"key":"e_1_2_1_91_1","unstructured":"M\u00edche\u00e1l \u00d3 Searc\u00f3id. 2006. Metric Spaces. Springer London. \t\t\t\t  M\u00edche\u00e1l \u00d3 Searc\u00f3id. 2006. Metric Spaces. Springer London."},{"key":"e_1_2_1_92_1","unstructured":"L.A. Steen and J.A. Seebach. 1995. Counterexamples in Topology. Dover Publications. \t\t\t\t  L.A. Steen and J.A. Seebach. 1995. Counterexamples in Topology. Dover Publications."},{"key":"e_1_2_1_93_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02413910"},{"key":"e_1_2_1_94_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.fss.2013.08.009"},{"key":"e_1_2_1_95_1","doi-asserted-by":"publisher","DOI":"10.2307\/2268577"},{"key":"e_1_2_1_96_1","unstructured":"A. Thue. 1914. Probleme \u00fcber Ver\u00e4nderungen von Zeichenreihen nach gegebenen Regeln. J. Dybwad. \t\t\t\t  A. Thue. 1914. Probleme \u00fcber Ver\u00e4nderungen von Zeichenreihen nach gegebenen Regeln. J. Dybwad."},{"key":"e_1_2_1_97_1","doi-asserted-by":"publisher","DOI":"10.2307\/2272559"},{"key":"e_1_2_1_98_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2016.32"},{"key":"e_1_2_1_99_1","volume-title":"Optimal Transport: Old and New","author":"Villani C.","unstructured":"C. Villani . 2008. Optimal Transport: Old and New . Springer Berlin Heidelberg . C. Villani. 2008. Optimal Transport: Old and New. Springer Berlin Heidelberg."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571256","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3571256","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:08:22Z","timestamp":1750183702000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571256"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,9]]},"references-count":99,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2023,1,9]]}},"alternative-id":["10.1145\/3571256"],"URL":"https:\/\/doi.org\/10.1145\/3571256","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,1,9]]},"assertion":[{"value":"2023-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}