{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,11]],"date-time":"2026-05-11T17:24:40Z","timestamp":1778520280515,"version":"3.51.4"},"reference-count":63,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2023,8,30]],"date-time":"2023-08-30T00:00:00Z","timestamp":1693353600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,8,30]]},"abstract":"<jats:p>Functional logic languages have a rich literature, but it is tricky  \n to give them a satisfying semantics. In this paper we describe the  \n Verse calculus, VC, a new core calculus for deterministic functional  \n logic programming. Our main contribution is to equip VC with a  \n small-step rewrite semantics, so that we can reason  \n about a VC program in the same way as one does with lambda  \n calculus; that is, by applying successive rewrites to it.  \n We also show that the rewrite system is confluent for well-behaved terms.<\/jats:p>","DOI":"10.1145\/3607845","type":"journal-article","created":{"date-parts":[[2023,8,31]],"date-time":"2023-08-31T17:40:31Z","timestamp":1693503631000},"page":"417-447","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["The Verse Calculus: A Core Calculus for Deterministic Functional Logic Programming"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-6894-4020","authenticated-orcid":false,"given":"Lennart","family":"Augustsson","sequence":"first","affiliation":[{"name":"Epic Games, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3753-6821","authenticated-orcid":false,"given":"Joachim","family":"Breitner","sequence":"additional","affiliation":[{"name":"Unaffiliated, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8113-4478","authenticated-orcid":false,"given":"Koen","family":"Claessen","sequence":"additional","affiliation":[{"name":"Epic Games, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1802-9421","authenticated-orcid":false,"given":"Ranjit","family":"Jhala","sequence":"additional","affiliation":[{"name":"Epic Games, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6085-1435","authenticated-orcid":false,"given":"Simon","family":"Peyton Jones","sequence":"additional","affiliation":[{"name":"Epic Games, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8171-386X","authenticated-orcid":false,"given":"Olin","family":"Shivers","sequence":"additional","affiliation":[{"name":"Epic Games, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1421-3811","authenticated-orcid":false,"given":"Guy L.","family":"Steele Jr.","sequence":"additional","affiliation":[{"name":"Oracle Labs, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-0230-0605","authenticated-orcid":false,"given":"Tim","family":"Sweeney","sequence":"additional","affiliation":[{"name":"Epic Games, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,8,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2004.01.001"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068411000263"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.10.026"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1599410.1599420"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1721654.1721675"},{"key":"e_1_2_1_6_1","volume-title":"Curry: A Tutorial Introduction","author":"Antoy Sergio","year":"2021","unstructured":"Sergio Antoy and Michael Hanus. 2021. Curry: A Tutorial Introduction. Kiel University (Christian-Albrechts-Universit\u00e4t zu Kiel). https:\/\/web.archive.org\/web\/20220121070135\/https:\/\/www.informatik.uni-kiel.de\/~curry\/tutorial\/tutorial.pdf"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(01)00104-X"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1994.316066"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1997.2651"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199507"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951948"},{"key":"e_1_2_1_12_1","volume-title":"The Optimal Implementation of Functional Programming Languages","author":"Asperti Andrea","unstructured":"Andrea Asperti and Stefano Guerrini. 1999. The Optimal Implementation of Functional Programming Languages. Cambridge University Press."},{"key":"e_1_2_1_13_1","volume-title":"Olin Shivers, Guy Steele, and Tim Sweeney.","author":"Augustsson Lennart","year":"2023","unstructured":"Lennart Augustsson, Joachim Breitner, Koen Claessen, Ranjit Jhala, Simon Peyton Jones, Olin Shivers, Guy Steele, and Tim Sweeney. 2023. The Verse Calculus: A Core Calculus for Deterministic Functional Logic Programming. Epic Games. https:\/\/simon.peytonjones.org\/verse-calculus\/"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2016.2"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-64276-1_13"},{"key":"e_1_2_1_16_1","volume-title":"Semantics of a Relational \u03bb -Calculus (Extended Version), version 4. CoRR, abs\/2009.10929","author":"Barenbaum Pablo","year":"2021","unstructured":"Pablo Barenbaum, Federico Lochbaum, and Mariana Milicich. 2021. Semantics of a Relational \u03bb -Calculus (Extended Version), version 4. CoRR, abs\/2009.10929 (2021), 28 Feb., 51 pages. arXiv:2009.10929. arxiv:2009.10929"},{"key":"e_1_2_1_17_1","volume-title":"The Lambda Calculus: Its Syntax and Semantics (revised ed.) (Studies in Logic and the Foundations of Mathematics","author":"Hendrik H. P.","unstructured":"H. P. (Hendrik Pieter) Barendregt. 1984. The Lambda Calculus: Its Syntax and Semantics (revised ed.) (Studies in Logic and the Foundations of Mathematics, Vol. 103). North-Holland (Elsevier Science Publishers), Amsterdam. isbn:0444867481 lccn:84005966"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428209"},{"key":"e_1_2_1_19_1","article-title":"Encapsulating Non-Determinism in Functional Logic Computations [extended journal version]","volume":"2004","author":"Bernd Bra\u00df","year":"2004","unstructured":"Bernd Bra\u00df el, Michael Hanus, and Frank Huch. 2004. Encapsulating Non-Determinism in Functional Logic Computations [extended journal version]. Journal of Functional and Logic Programming, 2004, 6 (2004), Dec., 28 pages. http:\/\/danae.uni-muenster.de\/lehre\/kuchen\/JFLP\/articles\/2004\/S04-01\/A2004-06\/JFLP-A2004-06.pdf Special Issue 1. Archived at","journal-title":"Journal of Functional and Logic Programming"},{"key":"e_1_2_1_20_1","volume-title":"13th International Workshop on Functional and (Constraint) Logic Programming (WFLP\u201904)","author":"Bernd Bra\u00df","year":"2004","unstructured":"Bernd Bra\u00df el, Michael Hanus, and Frank Huch. 2004. Encapsulating Non-Determinism in Functional Logic Computations [workshop version]. In 13th International Workshop on Functional and (Constraint) Logic Programming (WFLP\u201904). 74\u201390. issn:0935-3232 Full proceedings available at http:\/\/www-i2.informatik.rwth-aachen.de\/WFLP04\/WFLP-proceedings.pdf"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-76637-7_9"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00675-3_13"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/69.43410"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(97)00010-5"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351266"},{"key":"e_1_2_1_26_1","volume-title":"Mellish","author":"Clocksin William F.","year":"2003","unstructured":"William F. Clocksin and Christopher S. Mellish. 2003. Programming in Prolog (Using the ISO Standard) (fifth ed.). Springer-Verlag New York Berlin Heidelberg. isbn:0-387-00678-8"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45231-5_8"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1145"},{"key":"e_1_2_1_29_1","volume-title":"Robert Bruce Findler, and Matthew Flatt","author":"Felleisen Matthias","year":"2009","unstructured":"Matthias Felleisen, Robert Bruce Findler, and Matthew Flatt. 2009. Semantics Engineering with PLT Redex. MIT Press, Cambridge, Massachusetts, USA. isbn:978-0-262-06275-6 https:\/\/mitpress.mit.edu\/9780262062756\/semantics-engineering-with-plt-redex\/"},{"key":"e_1_2_1_30_1","volume-title":"Formal Description of Programming Concepts III: Proceedings of the IFIP TC 2\/WG 2.2 Working Conference. Elsevier Science Publishers (North-Holland), 193\u2013217","author":"Felleisen Matthias","year":"2022","unstructured":"Matthias Felleisen and Daniel P. Friedman. 1986. Control Operators, the SECD Machine, and the \u03bb -Calculus. In Formal Description of Programming Concepts III: Proceedings of the IFIP TC 2\/WG 2.2 Working Conference. Elsevier Science Publishers (North-Holland), 193\u2013217. isbn:978-0444702531 https:\/\/web.archive.org\/web\/20220709064643\/https:\/\/www.cs.tufts.edu\/~nr\/cs257\/archive\/matthias-felleisen\/cesk.pdf"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90109-5"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0743-1066(98)10029-8"},{"key":"e_1_2_1_33_1","volume-title":"User\u2019s Manual for the Icon Programming Language. Department of Computer Science","author":"Griswold Ralph E.","unstructured":"Ralph E. Griswold. 1979. User\u2019s Manual for the Icon Programming Language. Department of Computer Science, University of Arizona. https:\/\/www2.cs.arizona.edu\/icon\/ftp\/doc\/tr78_14.pdf"},{"key":"e_1_2_1_34_1","volume-title":"Griswold","author":"Griswold Ralph E.","year":"1983","unstructured":"Ralph E. Griswold and Madge T. Griswold. 1983. The Icon Programming Language. Prentice-Hall, Englewood Cliffs, New Jersey."},{"key":"e_1_2_1_35_1","volume-title":"Griswold","author":"Griswold Ralph E.","year":"2002","unstructured":"Ralph E. Griswold and Madge T. Griswold. 2002. The Icon Programming Language (third ed.). Peer-to-Peer Communications. https:\/\/web.archive.org\/web\/20040723085807\/https:\/\/www2.cs.arizona.edu\/icon\/ftp\/doc\/lb1up.pdf"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/988078.988082"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/357133.357136"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37651-1_6"},{"key":"e_1_2_1_39_1","volume-title":"Bj\u00f6rn Peem\u00f6ller, and Frank Steiner.","author":"Hanus Michael","year":"2016","unstructured":"Michael Hanus, Sergio Antoy, Bernd Bra\u00df el, Herbert Kuchen, Francisco J. L\u00f3pez-Fraguas, Wolfgang Lux, Juan Jos\u00e9 Moreno Navarro, Bj\u00f6rn Peem\u00f6ller, and Frank Steiner. 2016. Curry: An Integrated Functional Logic Language (Version 0.9.0). University of Kiel. https:\/\/web.archive.org\/web\/20161020144634\/https:\/\/www-ps.informatik.uni-kiel.de\/currywiki\/_media\/documentation\/report.pdf"},{"key":"e_1_2_1_40_1","volume-title":"The Church-Rosser Property and a Result in Combinatory Logic. Ph. D. Dissertation","author":"Hindley J. Roger","unstructured":"J. Roger Hindley. 1964. The Church-Rosser Property and a Result in Combinatory Logic. Ph. D. Dissertation. University of Newcastle-upon-Tyne. United Kingdom."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/322217.322230"},{"key":"e_1_2_1_42_1","unstructured":"1980. Programming Corner from Icon Newsletter 4. https:\/\/www2.cs.arizona.edu\/icon\/progcorn\/pc_inl04.htm"},{"key":"e_1_2_1_43_1","volume-title":"Lambda lifting: Transforming programs to recursive equations","author":"Johnsson Thomas","unstructured":"Thomas Johnsson. 1985. Lambda lifting: Transforming programs to recursive equations. In Functional Programming Languages and Computer Architecture, Jean-Pierre Jouannaud (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 190\u2013203. isbn:978-3-540-39677-2"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086390"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289462"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96711"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158618"},{"key":"e_1_2_1_48_1","unstructured":"Jean-Jacques L\u00e9vy. 1978. R\u00e9ductions Correctes et Optimales dans le Lambda-calcul. Ph. D. Dissertation. Universit\u00e9 Paris vii. https:\/\/web.archive.org\/web\/20051016053439\/http:\/\/pauillac.inria.fr\/~levy\/pubs\/78phd.pdf"},{"key":"e_1_2_1_49_1","article-title":"Programming in an Integrated Functional and Logic Language","volume":"1999","author":"Lloyd John W.","year":"1999","unstructured":"John W. Lloyd. 1999. Programming in an Integrated Functional and Logic Language. Journal of Functional and Logic Programming, 1999, 3 (1999), March, issn:1080\u20135230 http:\/\/danae.uni-muenster.de\/lehre\/kuchen\/JFLP\/\/articles\/1999\/A99-03\/JFLP-A99-03.pdf Archived at","journal-title":"Journal of Functional and Logic Programming"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068412000373"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/1273920.1273947"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908096"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2022.7"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000319"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/800194.805852"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/141471.141563"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96733"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/224164.224208"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70590-1_22"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.5555\/866084"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.5555\/889478"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/800228.806939"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3607845","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3607845","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:37:06Z","timestamp":1750178226000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3607845"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,8,30]]},"references-count":63,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2023,8,30]]}},"alternative-id":["10.1145\/3607845"],"URL":"https:\/\/doi.org\/10.1145\/3607845","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,8,30]]},"assertion":[{"value":"2023-08-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}