{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:05:08Z","timestamp":1779836708981,"version":"3.53.1"},"reference-count":0,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[1999,1]]},"abstract":"<jats:p>\n                    \u201cI have no data yet. It is a capital mistake to \ntheorise before one has data.\u201d\n                    <jats:bold>Sir Arthur Conan Doyle<\/jats:bold>\n                    <jats:italic>The Adventures of Sherlock Holmes<\/jats:italic>\n                  <\/jats:p>\n                  <jats:p>\n                    de Bruijn notation is a coding of lambda terms in which each occurrence of a bound variable\n                    <jats:italic>x<\/jats:italic>\n                    is replaced by a natural number, indicating the \u2018distance\u2019 \nfrom the occurrence to the abstraction \nthat introduced\n                    <jats:italic>x<\/jats:italic>\n                    . One might suppose that in any datatype for representing de Bruijn terms, \nthe distance restriction on numbers would have to be maintained as an explicit datatype invariant. \nHowever, by using a nested (or non-regular) datatype, we can define a representation in which\n                    <jats:italic>all<\/jats:italic>\n                    terms are well-formed, so that the invariant is enforced automatically by the type system. \nProgramming with nested types is only a little more difficult than programming with regular \ntypes, provided we stick to well-established structuring techniques. These involve expressing \ninductively defined functions in terms of an appropriate fold function for the type, and using \nfusion laws to establish their properties. In particular, the definition of lambda abstraction \nand beta reduction is particularly simple, and the proof of their associated properties is \nentirely mechanical.\n                  <\/jats:p>","DOI":"10.1017\/s0956796899003366","type":"journal-article","created":{"date-parts":[[2002,7,27]],"date-time":"2002-07-27T09:29:39Z","timestamp":1027762179000},"page":"77-91","source":"Crossref","is-referenced-by-count":105,"title":["de Bruijn notation as a nested datatype"],"prefix":"10.1017","volume":"9","author":[{"given":"RICHARD S.","family":"BIRD","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"ROSS","family":"PATERSON","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[1999,1,1]]},"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796899003366","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:34:59Z","timestamp":1779834899000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796899003366\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,1]]},"references-count":0,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1999,1]]}},"alternative-id":["S0956796899003366"],"URL":"https:\/\/doi.org\/10.1017\/s0956796899003366","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[1999,1]]}}}