{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:05:04Z","timestamp":1779836704542,"version":"3.53.1"},"reference-count":0,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2001,5,31]],"date-time":"2001-05-31T00:00:00Z","timestamp":991267200000},"content-version":"unspecified","delay-in-days":30,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2001,5]]},"abstract":"<jats:p>A fair amount has been written on the subject of reasoning about pointer algorithms. \nThere was a peak about 1980 when everyone seemed to be tackling the formal \nverification of the Schorr\u2013Waite marking algorithm, including Gries (1979, Morris \n(1982) and Topor (1979). Bornat (2000) writes: \u201cThe Schorr\u2013Waite algorithm is the \nfirst mountain that any formalism for pointer aliasing should climb\u201d. Then it went \nmore or less quiet for a while, but in the last few years there has been a resurgence of \ninterest, driven by new ideas in relational algebras (M\u00f6eller, 1993), in data refinement \nButler (1999), in type theory (Hofmann, 2000; Walker and Morrisett, 2000), in novel \nkinds of assertion (Reynolds, 2000), and by the demands of mechanised reasoning \n(Bornat, 2000). Most approaches end up being based in the Floyd\u2013Dijkstra\u2013Hoare \ntradition with loops and invariant assertions. To be sure, when dealing with any \nrecursively-defined linked structure some declarative notation has to be brought in to \nspecify the problem, but no one to my knowledge has advocated a purely functional \napproach throughout. Mason (1988) comes close, but his Lisp expressions can be \nvery impure. M\u00f6ller (1999) also exploits an algebraic approach, and the structure of \nhis paper has much in common with what follows.<\/jats:p>\n                  <jats:p>This pearl explores the possibility of a simple functional approach to pointer \nmanipulation algorithms.<\/jats:p>","DOI":"10.1017\/s0956796801003914","type":"journal-article","created":{"date-parts":[[2002,7,27]],"date-time":"2002-07-27T09:17:11Z","timestamp":1027761431000},"page":"347-358","source":"Crossref","is-referenced-by-count":5,"title":["FUNCTIONAL PEARL\n                    <i>Unfolding pointer algorithms<\/i>"],"prefix":"10.1017","volume":"11","author":[{"given":"RICHARD S.","family":"BIRD","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2001,5,31]]},"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796801003914","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:34:50Z","timestamp":1779834890000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796801003914\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,5]]},"references-count":0,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2001,5]]}},"alternative-id":["S0956796801003914"],"URL":"https:\/\/doi.org\/10.1017\/s0956796801003914","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2001,5]]}}}