{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T15:47:43Z","timestamp":1787068063961,"version":"build-2736575974"},"reference-count":65,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2022,8,29]],"date-time":"2022-08-29T00:00:00Z","timestamp":1661731200000},"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":["1521539,1703835,2006535"],"award-info":[{"award-number":["1521539,1703835,2006535"]}],"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":[[2022,8,29]]},"abstract":"<jats:p>Free monads (and their variants) have become a popular general-purpose tool for representing the semantics of effectful programs in proof assistants. These data structures support the compositional definition of semantics parameterized by uninterpreted events, while admitting a rich equational theory of equivalence. But monads are not the only way to structure effectful computation, why should we limit ourselves?<\/jats:p>\n                  <jats:p>In this paper, inspired by applicative functors, selective functors, and other structures, we define a collection of data structures and theories, which we call program adverbs, that capture a variety of computational patterns. Program adverbs are themselves composable, allowing them to be used to specify the semantics of languages with multiple computation patterns. We use program adverbs as the basis for a new class of semantic embeddings called Tl\u00f6n embeddings. Compared with embeddings based on free monads, Tl\u00f6n embeddings allow more flexibility in computational modeling of effects, while retaining more information about the program's syntactic structure.<\/jats:p>","DOI":"10.1145\/3547632","type":"journal-article","created":{"date-parts":[[2022,8,31]],"date-time":"2022-08-31T15:39:26Z","timestamp":1661960366000},"page":"312-342","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Program adverbs and Tl\u00f6n embeddings"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8720-883X","authenticated-orcid":false,"given":"Yao","family":"Li","sequence":"first","affiliation":[{"name":"Portland State University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6756-9168","authenticated-orcid":false,"given":"Stephanie","family":"Weirich","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,8,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36576-1_2"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES.2013.1"},{"key":"e_1_2_1_3_1","volume-title":"Program Logics for Certified Compilers","author":"Appel Andrew W.","unstructured":"Andrew W. Appel , Robert Dockins , Aquinas Hobor , Lennart Beringer , Josiah Dodds , Gordon Stewart , Sandrine Blazy , and Xavier Leroy . 2014. Program Logics for Certified Compilers . Cambridge University Press . isbn:978-1-10-704801-0 Andrew W. Appel, Robert Dockins, Aquinas Hobor, Lennart Beringer, Josiah Dodds, Gordon Stewart, Sandrine Blazy, and Xavier Leroy. 2014. Program Logics for Certified Compilers. Cambridge University Press. isbn:978-1-10-704801-0"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_4"},{"key":"e_1_2_1_5_1","volume-title":"Labyrinths: Selected Stories & Other Writings, Donald A","author":"Borges Jorge Luis","year":"1961","unstructured":"Jorge Luis Borges . 1940. Tl\u00f6n, Uqbar , Orbis Tertius . In Labyrinths: Selected Stories & Other Writings, Donald A . Yates and James E. Irby (Eds.). The story was translated by James E. Irby. It first appeared in New World Writing No. 18, 1961 . The book was first published in 1962 Jorge Luis Borges. 1940. Tl\u00f6n, Uqbar, Orbis Tertius. In Labyrinths: Selected Stories & Other Writings, Donald A. Yates and James E. Irby (Eds.). The story was translated by James E. Irby. It first appeared in New World Writing No. 18, 1961. The book was first published in 1962"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/645902.672777"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796820000283"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-1(2:1)2005"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.153.2"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473599"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3331545.3342592"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03013-0_13"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429094"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.22152\/programming-journal.org\/2019\/3\/8"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45337-7_17"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373817"},{"key":"e_1_2_1_17_1","volume-title":"Formally Verified Simulations of State-Rich Processes using Interaction Trees in Isabelle\/HOL. CoRR, abs\/2105.05133","author":"Foster Simon","year":"2021","unstructured":"Simon Foster , Chung-Kil Hur , and Jim Woodcock . 2021. Formally Verified Simulations of State-Rich Processes using Interaction Trees in Isabelle\/HOL. CoRR, abs\/2105.05133 ( 2021 ), arxiv:2105.05133. arxiv:2105.05133 Simon Foster, Chung-Kil Hur, and Jim Woodcock. 2021. Formally Verified Simulations of State-Rich Processes using Interaction Trees in Isabelle\/HOL. CoRR, abs\/2105.05133 (2021), arxiv:2105.05133. arxiv:2105.05133"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3356903"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192381"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(99)00023-4"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-59451-5_4"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2804302.2804319"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294106"},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the 27th International Conference on Types for Proofs and Programs, TYPES 2021, June 14\u201318","author":"Kravchuk-Kirilyuk Anastasiya","year":"2021","unstructured":"Anastasiya Kravchuk-Kirilyuk , Yizhou Zhang , and Nada Amin . 2021 . Family Polymorphism for Proof Extensibility . In Proceedings of the 27th International Conference on Types for Proofs and Programs, TYPES 2021, June 14\u201318 , 2021. https:\/\/types21.liacs.nl\/download\/family-polymorphism-for-proof-extensibility\/ Anastasiya Kravchuk-Kirilyuk, Yizhou Zhang, and Nada Amin. 2021. Family Polymorphism for Proof Extensibility. In Proceedings of the 27th International Conference on Types for Proofs and Programs, TYPES 2021, June 14\u201318, 2021. https:\/\/types21.liacs.nl\/download\/family-polymorphism-for-proof-extensibility\/"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158133"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527324"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-020-00523-2"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.6678339"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.02.018"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385971"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341708"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_16"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628144"},{"key":"e_1_2_1_34_1","unstructured":"Coq development team. 2022. The Coq proof assistant. http:\/\/coq.inria.fr Version 8.15.1 \t\t\t\t  Coq development team. 2022. The Coq proof assistant. http:\/\/coq.inria.fr Version 8.15.1"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-19797-5_13"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006326"},{"key":"e_1_2_1_37_1","unstructured":"Bartosz Milewski. 2018. Free Monoidal Functors Categorically!. https:\/\/bartoszmilewski.com\/2018\/05\/16\/free-monoidal-functors-categorically\/ Blog post \t\t\t\t  Bartosz Milewski. 2018. Free Monoidal Functors Categorically!. https:\/\/bartoszmilewski.com\/2018\/05\/16\/free-monoidal-functors-categorically\/ Blog post"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_2_1_39_1","doi-asserted-by":"crossref","unstructured":"Andrey Mokhov. 2019. Implementation of selective applicative functors in Haskell. https:\/\/hackage.haskell.org\/package\/selective \t\t\t\t  Andrey Mokhov. 2019. Implementation of selective applicative functors in Haskell. https:\/\/hackage.haskell.org\/package\/selective","DOI":"10.1145\/3341694"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341694"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796820000088"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2021.29"},{"key":"e_1_2_1_43_1","volume-title":"Proceedings of the 1999 USENIX Annual Technical Conference","author":"Pai Vivek S.","year":"1999","unstructured":"Vivek S. Pai , Peter Druschel , and Willy Zwaenepoel . 1999 . Flash: An efficient and portable Web server . In Proceedings of the 1999 USENIX Annual Technical Conference , June 6-11, 1999, Monterey, California, USA. USENIX, 199\u2013212. http:\/\/www.usenix.org\/events\/usenix99\/full_papers\/pai\/pai.pdf Vivek S. Pai, Peter Druschel, and Willy Zwaenepoel. 1999. Flash: An efficient and portable Web server. In Proceedings of the 1999 USENIX Annual Technical Conference, June 6-11, 1999, Monterey, California, USA. USENIX, 199\u2013212. http:\/\/www.usenix.org\/events\/usenix99\/full_papers\/pai\/pai.pdf"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523707"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2014.10.015"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2022.19"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434307"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341690"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167092"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40447-4_2"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3409003"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2491978"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61628-4_7"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341707"},{"key":"e_1_2_1_55_1","unstructured":"Philip Wadler. 1990. Recursive types for free!. http:\/\/homepages.inf.ed.ac.uk\/wadler\/papers\/free-rectypes\/free-rectypes.txt Draft \t\t\t\t  Philip Wadler. 1990. Recursive types for free!. http:\/\/homepages.inf.ed.ac.uk\/wadler\/papers\/free-rectypes\/free-rectypes.txt Draft"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001560"},{"key":"e_1_2_1_57_1","unstructured":"Philip Wadler. 1998. The Expression Problem. http:\/\/homepages.inf.ed.ac.uk\/wadler\/papers\/expression\/expression.txt Email correspondence \t\t\t\t  Philip Wadler. 1998. The Expression Problem. http:\/\/homepages.inf.ed.ac.uk\/wadler\/papers\/expression\/expression.txt Email correspondence"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3409002"},{"key":"e_1_2_1_59_1","unstructured":"Li-yao Xia. 2019. Free applicative functors in Coq. https:\/\/blog.poisson.chat\/posts\/2019-07-14-free-applicative-functors.html Blog post \t\t\t\t  Li-yao Xia. 2019. Free applicative functors in Coq. https:\/\/blog.poisson.chat\/posts\/2019-07-14-free-applicative-functors.html Blog post"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371119"},{"key":"e_1_2_1_61_1","volume-title":"The 23rd International Conference on Formal Engineering Methods. Springer Science and Business Media Deutschland GmbH. https:\/\/eprints.whiterose.ac.uk\/188566\/","author":"Ye Kangfeng","year":"2022","unstructured":"Kangfeng Ye , Simon Foster , and Jim Woodcock . 2022 . Formally Verified Animation for RoboChart using Interaction Trees . In The 23rd International Conference on Formal Engineering Methods. Springer Science and Business Media Deutschland GmbH. https:\/\/eprints.whiterose.ac.uk\/188566\/ Kangfeng Ye, Simon Foster, and Jim Woodcock. 2022. Formally Verified Animation for RoboChart using Interaction Trees. In The 23rd International Conference on Formal Engineering Methods. Springer Science and Business Media Deutschland GmbH. https:\/\/eprints.whiterose.ac.uk\/188566\/"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547632"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473572"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373813"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2021.32"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3547632","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3547632","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3547632","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T14:43:29Z","timestamp":1750257809000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3547632"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8,29]]},"references-count":65,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2022,8,29]]}},"alternative-id":["10.1145\/3547632"],"URL":"https:\/\/doi.org\/10.1145\/3547632","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,8,29]]},"assertion":[{"value":"2022-08-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}