{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:09:18Z","timestamp":1750219758832,"version":"3.41.0"},"reference-count":29,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T00:00:00Z","timestamp":1697414400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CF-1651225,CF-1836724,CNS-1844807"],"award-info":[{"award-number":["CF-1651225,CF-1836724,CNS-1844807"]}],"id":[{"id":"10.13039\/100000001","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,10,16]]},"abstract":"<jats:p>\n            Pretty printers make trade-offs between the\n            <jats:italic>expressiveness<\/jats:italic>\n            of their pretty printing language, the\n            <jats:italic>optimality<\/jats:italic>\n            objective that they minimize when choosing between different ways to lay out a document, and the\n            <jats:italic>performance<\/jats:italic>\n            of their algorithm. This paper presents a new pretty printer, \u03a0\n            <jats:sub>\n              <jats:italic>e<\/jats:italic>\n            <\/jats:sub>\n            , that is strictly more expressive than all pretty printers in the literature and provably minimizes an optimality objective. Furthermore, the time complexity of \u03a0\n            <jats:sub>\n              <jats:italic>e<\/jats:italic>\n            <\/jats:sub>\n            is better than many existing pretty printers. When choosing among different ways to lay out a document, \u03a0\n            <jats:sub>\n              <jats:italic>e<\/jats:italic>\n            <\/jats:sub>\n            consults a user-supplied\n            <jats:italic>cost factory<\/jats:italic>\n            , which determines the optimality objective, giving \u03a0\n            <jats:sub>\n              <jats:italic>e<\/jats:italic>\n            <\/jats:sub>\n            a unique degree of flexibility. We use the Lean theorem prover to verify the correctness (validity and optimality) of \u03a0\n            <jats:sub>\n              <jats:italic>e<\/jats:italic>\n            <\/jats:sub>\n            , and implement \u03a0\n            <jats:sub>\n              <jats:italic>e<\/jats:italic>\n            <\/jats:sub>\n            concretely as a pretty printer that we call PrettyExpressive. To evaluate our pretty printer against others, we develop a formal framework for reasoning about the expressiveness of pretty printing languages, and survey pretty printers in the literature, comparing their expressiveness, optimality, worst-case time complexity, and practical running time. Our evaluation shows that PrettyExpressive is efficient and effective at producing optimal layouts. PrettyExpressive has also seen real-world adoption: it serves as a foundation of a code formatter for Racket.\n          <\/jats:p>","DOI":"10.1145\/3622837","type":"journal-article","created":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T15:41:29Z","timestamp":1697470889000},"page":"1122-1149","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["A Pretty Expressive Printer"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3900-5602","authenticated-orcid":false,"given":"Sorawee","family":"Porncharoenwase","sequence":"first","affiliation":[{"name":"University of Washington, Seattle, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-0244-6193","authenticated-orcid":false,"given":"Justin","family":"Pombrio","sequence":"additional","affiliation":[{"name":"n.n., Cambridge, United States"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1155-2711","authenticated-orcid":false,"given":"Emina","family":"Torlak","sequence":"additional","affiliation":[{"name":"University of Washington, Seattle, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,10,16]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Pablo R Azero Alcocer and S Doaitse Swierstra. 1998. Optimal pretty-printing combinators. https:\/\/web.archive.org\/web\/20040911044443\/http:\/\/www.cs.uu.nl\/groups\/ST\/Software\/PP\/pabloicfp.ps \t\t\t\t  Pablo R Azero Alcocer and S Doaitse Swierstra. 1998. Optimal pretty-printing combinators. https:\/\/web.archive.org\/web\/20040911044443\/http:\/\/www.cs.uu.nl\/groups\/ST\/Software\/PP\/pabloicfp.ps"},{"key":"e_1_2_1_2_1","unstructured":"Jean-Philippe Bernardy. 2017. Disjunctionless. https:\/\/github.com\/jyp\/prettiest\/pull\/10 \t\t\t\t  Jean-Philippe Bernardy. 2017. Disjunctionless. https:\/\/github.com\/jyp\/prettiest\/pull\/10"},{"key":"e_1_2_1_3_1","unstructured":"Jean-Philippe Bernardy. 2017. prettiest. https:\/\/github.com\/jyp\/prettiest\/blob\/5e7a12cf37bb01467485bbe1e9d8f272fa4f8cd5\/Text\/PrettyPrint\/Compact\/Core.hs \t\t\t\t  Jean-Philippe Bernardy. 2017. prettiest. https:\/\/github.com\/jyp\/prettiest\/blob\/5e7a12cf37bb01467485bbe1e9d8f272fa4f8cd5\/Text\/PrettyPrint\/Compact\/Core.hs"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110250"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1053468.1053473"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1184\/R1\/6610382.v1"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSM.2002.1167816"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_9_1","unstructured":"ESLint. 2014. Change no-comma-dangle to comma-dangle. https:\/\/github.com\/eslint\/eslint\/issues\/1350 \t\t\t\t  ESLint. 2014. Change no-comma-dangle to comma-dangle. https:\/\/github.com\/eslint\/eslint\/issues\/1350"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(91)90036-W"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3127323"},{"volume-title":"The design of a pretty-printing library","author":"Hughes John","key":"e_1_2_1_12_1","unstructured":"John Hughes . 1995. The design of a pretty-printing library . In Advanced Functional Programming, Johan Jeuring and Erik Meijer (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 53\u201396. isbn:978-3-540-49270-2 John Hughes. 1995. The design of a pretty-printing library. In Advanced Functional Programming, Johan Jeuring and Erik Meijer (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 53\u201396. isbn:978-3-540-49270-2"},{"volume-title":"Linear Pretty-Printing","author":"Kiselyov Oleg","key":"e_1_2_1_13_1","unstructured":"Oleg Kiselyov , Simon Peyton-Jones , and Amr Sabry . 2012. Lazy v. Yield: Incremental , Linear Pretty-Printing . In Programming Languages and Systems, Ranjit Jhala and Atsushi Igarashi (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 190\u2013206. isbn:978-3-642-35182-2 Oleg Kiselyov, Simon Peyton-Jones, and Amr Sabry. 2012. Lazy v. Yield: Incremental, Linear Pretty-Printing. In Programming Languages and Systems, Ranjit Jhala and Atsushi Igarashi (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 190\u2013206. isbn:978-3-642-35182-2"},{"key":"e_1_2_1_14_1","unstructured":"Daan Leijen. 2000. wl-pprint: The Wadler\/Leijen Pretty Printer. https:\/\/hackage.haskell.org\/package\/wl-pprint \t\t\t\t  Daan Leijen. 2000. wl-pprint: The Wadler\/Leijen Pretty Printer. https:\/\/hackage.haskell.org\/package\/wl-pprint"},{"volume-title":"Automated Deduction \u2013 CADE 28, Andr\u00e9 Platzer and Geoff Sutcliffe (Eds.)","author":"de Moura Leonardo","key":"e_1_2_1_15_1","unstructured":"Leonardo de Moura and Sebastian Ullrich . 2021. The Lean 4 Theorem Prover and Programming Language . In Automated Deduction \u2013 CADE 28, Andr\u00e9 Platzer and Geoff Sutcliffe (Eds.) . Springer International Publishing , Cham . 625\u2013635. isbn:978-3-030-79876-5 Leonardo de Moura and Sebastian Ullrich. 2021. The Lean 4 Theorem Prover and Programming Language. In Automated Deduction \u2013 CADE 28, Andr\u00e9 Platzer and Geoff Sutcliffe (Eds.). Springer International Publishing, Cham. 625\u2013635. isbn:978-3-030-79876-5"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/357114.357115"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360224"},{"key":"e_1_2_1_18_1","unstructured":"Simon Peyton-Jones. 1997. A pretty printer library in Haskell. https:\/\/web.archive.org\/web\/20080221052958\/http:\/\/research.microsoft.com\/Users\/simonpj\/downloads\/pretty-printer\/pretty.html The identified mistakes are noted at \t\t\t\t  Simon Peyton-Jones. 1997. A pretty printer library in Haskell. https:\/\/web.archive.org\/web\/20080221052958\/http:\/\/research.microsoft.com\/Users\/simonpj\/downloads\/pretty-printer\/pretty.html The identified mistakes are noted at"},{"volume-title":"Perspectives of System Informatics","author":"Podkopaev Anton","key":"e_1_2_1_19_1","unstructured":"Anton Podkopaev and Dmitri Boulytchev . 2015. Polynomial-Time Optimal Pretty-Printing Combinators with Choice . In Perspectives of System Informatics , Andrei Voronkov and Irina Virbitskaite (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 257\u2013265. isbn:978-3-662-46823-4 Anton Podkopaev and Dmitri Boulytchev. 2015. Polynomial-Time Optimal Pretty-Printing Combinators with Choice. In Perspectives of System Informatics, Andrei Voronkov and Irina Virbitskaite (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 257\u2013265. isbn:978-3-662-46823-4"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498709"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.8332960"},{"key":"e_1_2_1_22_1","unstructured":"Sorawee Porncharoenwase Justin Pombrio and Emina Torlak. 2023. A Pretty Expressive Printer (with Appendices). arxiv:2310.01530. \t\t\t\t  Sorawee Porncharoenwase Justin Pombrio and Emina Torlak. 2023. A Pretty Expressive Printer (with Appendices). arxiv:2310.01530."},{"key":"e_1_2_1_23_1","unstructured":"Prettier. 2016. Technical Details. https:\/\/prettier.io\/docs\/en\/technical-details.html \t\t\t\t  Prettier. 2016. Technical Details. https:\/\/prettier.io\/docs\/en\/technical-details.html"},{"key":"e_1_2_1_24_1","series-title":"LNCS","volume-title":"Pablo R Azero Alcocer, and Joao Saraiva","author":"Swierstra S Doaitse","year":"1999","unstructured":"S Doaitse Swierstra , Pablo R Azero Alcocer, and Joao Saraiva . 1999 . Designing and Implementing Combinator Languages. In Third Summer School on Advanced Functional Programming, volume 1608 of LNCS . Springer-Verlag , 150\u2013206. S Doaitse Swierstra, Pablo R Azero Alcocer, and Joao Saraiva. 1999. Designing and Implementing Combinator Languages. In Third Summer School on Advanced Functional Programming, volume 1608 of LNCS. Springer-Verlag, 150\u2013206."},{"key":"e_1_2_1_25_1","unstructured":"The Python Language Reference. 2010. Lexical analysis. https:\/\/docs.python.org\/2.7\/reference\/lexical_analysis.html \t\t\t\t  The Python Language Reference. 2010. Lexical analysis. https:\/\/docs.python.org\/2.7\/reference\/lexical_analysis.html"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2666356.2594340"},{"key":"e_1_2_1_27_1","doi-asserted-by":"crossref","unstructured":"Philip Wadler. 2003. A prettier printer. The Fun of Programming Cornerstones of Computing 223\u2013243. \t\t\t\t  Philip Wadler. 2003. A prettier printer. The Fun of Programming Cornerstones of Computing 223\u2013243.","DOI":"10.1007\/978-1-349-91518-7_11"},{"key":"e_1_2_1_28_1","unstructured":"Phillip Yelland. 2015. rfmt: A code formatter for R. https:\/\/github.com\/google\/rfmt \t\t\t\t  Phillip Yelland. 2015. rfmt: A code formatter for R. https:\/\/github.com\/google\/rfmt"},{"key":"e_1_2_1_29_1","unstructured":"Phillip Yelland. 2016. A New Approach to Optimal Code Formatting. Technical note for open source project rfmt; https:\/\/github.com\/google\/rfmt \t\t\t\t  Phillip Yelland. 2016. A New Approach to Optimal Code Formatting. Technical note for open source project rfmt; https:\/\/github.com\/google\/rfmt"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622837","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3622837","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3622837","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:37:04Z","timestamp":1750178224000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622837"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,16]]},"references-count":29,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2023,10,16]]}},"alternative-id":["10.1145\/3622837"],"URL":"https:\/\/doi.org\/10.1145\/3622837","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2023,10,16]]},"assertion":[{"value":"2023-10-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}