{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T12:15:43Z","timestamp":1770293743880,"version":"3.49.0"},"reference-count":29,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2018,7,30]],"date-time":"2018-07-30T00:00:00Z","timestamp":1532908800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/P00587X\/1"],"award-info":[{"award-number":["EP\/P00587X\/1"]}],"id":[{"id":"10.13039\/501100000266","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":[[2018,7,30]]},"abstract":"<jats:p>\n            Parametricity, in both operational and denotational forms, has long been a useful tool for reasoning about program correctness. However, there is as yet no comparable technique for reasoning about program\n            <jats:italic>improvement<\/jats:italic>\n            , that is, when one program uses fewer resources than another. Existing theories of parametricity cannot be used to address this problem as they are agnostic with regard to resource usage. This article addresses this problem by presenting a new operational theory of parametricity that is sensitive to time costs, which can be used to reason about time improvement properties. We demonstrate the applicability of our theory by showing how it can be used to prove that a number of well-known program fusion techniques are time improvements, including fixed point fusion, map fusion and short cut fusion.\n          <\/jats:p>","DOI":"10.1145\/3236763","type":"journal-article","created":{"date-parts":[[2018,7,31]],"date-time":"2018-07-31T19:41:18Z","timestamp":1533066078000},"page":"1-24","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Parametric polymorphism and operational improvement"],"prefix":"10.1145","volume":"2","author":[{"given":"Jennifer","family":"Hackett","sequence":"first","affiliation":[{"name":"University of Nottingham, UK"}]},{"given":"Graham","family":"Hutton","sequence":"additional","affiliation":[{"name":"University of Nottingham, UK"}]}],"member":"320","published-online":{"date-parts":[[2018,7,30]]},"reference":[{"key":"e_1_2_2_1_1","unstructured":"Sascha B\u00f6hme. 2007. Free Theorems for Sublanguages of Haskell. Master\u2019s thesis. Technische Universit\u00e4t Dresden.  Sascha B\u00f6hme. 2007. Free Theorems for Sublanguages of Haskell. Master\u2019s thesis. Technische Universit\u00e4t Dresden."},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2804302.2804312"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2014.10.007"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.03.005"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/165180.165214"},{"key":"e_1_2_2_6_1","volume-title":"A Foundation for Space-Safe Transformations of Call-by-Need Programs. Electronic Notes on Theoretical Computer Science 26","author":"Gustavsson J\u00f6rgen","year":"1999","unstructured":"J\u00f6rgen Gustavsson and David Sands . 1999. A Foundation for Space-Safe Transformations of Call-by-Need Programs. Electronic Notes on Theoretical Computer Science 26 ( 1999 ). J\u00f6rgen Gustavsson and David Sands. 1999. A Foundation for Space-Safe Transformations of Call-by-Need Programs. Electronic Notes on Theoretical Computer Science 26 (1999)."},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/507635.507667"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628142"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2015.21"},{"key":"e_1_2_2_10_1","unstructured":"Jennifer Hackett and Graham Hutton. 2018. A Generic Foundation for Program Improvement. (2018). In preparation.  Jennifer Hackett and Graham Hutton. 2018. A Generic Foundation for Program Improvement. (2018). In preparation."},{"key":"e_1_2_2_11_1","doi-asserted-by":"crossref","unstructured":"Martin Handley and Graham Hutton. 2018. Improving Haskell. In Trends in Functional Programming.  Martin Handley and Graham Hutton. 2018. Improving Haskell. In Trends in Functional Programming.","DOI":"10.1007\/978-3-030-18506-0_6"},{"key":"e_1_2_2_12_1","volume-title":"Mind the Gap: Unified Reasoning About Program Correctness and Efficiency. (2016)","author":"Hutton Graham","unstructured":"Graham Hutton and Jennifer Hackett . 2016. Mind the Gap: Unified Reasoning About Program Correctness and Efficiency. (2016) . Engineering and Physical Sciences Research Council grant EP\/P00587X\/1. Graham Hutton and Jennifer Hackett. 2016. Mind the Gap: Unified Reasoning About Program Correctness and Efficiency. (2016). Engineering and Physical Sciences Research Council grant EP\/P00587X\/1."},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964010"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158618"},{"key":"e_1_2_2_15_1","volume-title":"Lenses, Envelopes and Barbed Wire. In Functional Programming Languages and Computer Architecture \u201991 (Lecture Notes in Computer Science)","author":"Meijer Erik","unstructured":"Erik Meijer , Maarten M. Fokkinga , and Ross Paterson . 1991. Functional Programming with Bananas , Lenses, Envelopes and Barbed Wire. In Functional Programming Languages and Computer Architecture \u201991 (Lecture Notes in Computer Science) , Vol. 523 . Springer . Erik Meijer, Maarten M. Fokkinga, and Ross Paterson. 1991. Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire. In Functional Programming Languages and Computer Architecture \u201991 (Lecture Notes in Computer Science), Vol. 523. Springer."},{"key":"e_1_2_2_16_1","unstructured":"Andrew Moran and David Sands. 1999a. Improvement in a Lazy Context: An Operational Theory for Call-by-Need. (1999). Extended version of { Moran and Sands 1999b } available at http:\/\/tinyurl.com\/ohuv8ox .  Andrew Moran and David Sands. 1999a. Improvement in a Lazy Context: An Operational Theory for Call-by-Need. (1999). Extended version of { Moran and Sands 1999b } available at http:\/\/tinyurl.com\/ohuv8ox ."},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292547"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500003066"},{"key":"e_1_2_2_19_1","volume-title":"LCF Considered as a Programming Language. Theoretical Computer Science 5, 3","author":"Plotkin Gordon D.","year":"1977","unstructured":"Gordon D. Plotkin . 1977. LCF Considered as a Programming Language. Theoretical Computer Science 5, 3 ( 1977 ). Gordon D. Plotkin. 1977. LCF Considered as a Programming Language. Theoretical Computer Science 5, 3 (1977)."},{"key":"e_1_2_2_20_1","volume-title":"Proceedings of the IFIP 9th World Computer Congress","author":"Reynolds John C.","year":"1983","unstructured":"John C. Reynolds . 1983 . Types, Abstraction and Parametric Polymorphism . Proceedings of the IFIP 9th World Computer Congress (1983). John C. Reynolds. 1983. Types, Abstraction and Parametric Polymorphism. Proceedings of the IFIP 9th World Computer Congress (1983)."},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263760"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2790449.2790512"},{"key":"e_1_2_2_23_1","doi-asserted-by":"crossref","unstructured":"Daniel Seidel and Janis Voigtl\u00e4nder. 2011. Improvements for Free. In Quantitative Aspects of Programming Languages.  Daniel Seidel and Janis Voigtl\u00e4nder. 2011. Improvements for Free. In Quantitative Aspects of Programming Languages.","DOI":"10.4204\/EPTCS.57.7"},{"key":"e_1_2_2_24_1","volume-title":"Simon L Peyton Jones, and Joachim Breitner","author":"Sergey Ilya","year":"2017","unstructured":"Ilya Sergey , Dimitrios Vytiniotis , Simon L Peyton Jones, and Joachim Breitner . 2017 . Modular, Higher Order Cardinality Analysis in Theory and Practice. Journal of Functional Programming 27 (2017). Ilya Sergey, Dimitrios Vytiniotis, Simon L Peyton Jones, and Joachim Breitner. 2017. Modular, Higher Order Cardinality Analysis in Theory and Practice. Journal of Functional Programming 27 (2017)."},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796897002712"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364575"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010000313106"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.09.014"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99404"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3236763","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3236763","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T21:41:28Z","timestamp":1750282888000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3236763"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,7,30]]},"references-count":29,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2018,7,30]]}},"alternative-id":["10.1145\/3236763"],"URL":"https:\/\/doi.org\/10.1145\/3236763","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,7,30]]},"assertion":[{"value":"2018-07-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}