{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:16:53Z","timestamp":1754482613392,"version":"3.40.3"},"reference-count":6,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2025,4,3]],"date-time":"2025-04-03T00:00:00Z","timestamp":1743638400000},"content-version":"unspecified","delay-in-days":92,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:p>The setting is a tutorial on program verification in Agda. Please consult the programme for further details. [<jats:italic>See also<\/jats:italic><jats:italic>Appendix<\/jats:italic><jats:italic>A<\/jats:italic>.]<\/jats:p>","DOI":"10.1017\/s0956796825000061","type":"journal-article","created":{"date-parts":[[2025,4,3]],"date-time":"2025-04-03T09:33:18Z","timestamp":1743672798000},"update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":1,"title":["Binary search\u2014think positive"],"prefix":"10.1017","volume":"35","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-1694-4567","authenticated-orcid":false,"given":"ALEXANDER","family":"DINGES","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5678-0286","authenticated-orcid":false,"given":"RALF","family":"HINZE","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2025,4,3]]},"reference":[{"key":"S0956796825000061_ref4","unstructured":"Erickson, J. (2011) Algorithms."},{"key":"S0956796825000061_ref3","unstructured":"Dijkstra, E. W. (1982) Why numbering should start at zero. circulated privately."},{"key":"S0956796825000061_ref5","volume-title":"Prentice-Hall International Series in Computer Science","author":"Kaldewaij","year":"1990"},{"key":"S0956796825000061_ref1","volume-title":"Series in Computer Science","author":"Bird","year":"1988"},{"key":"S0956796825000061_ref6","volume-title":"The Art of Computer Programming, Volume 3: Sorting and Searching","author":"Knuth","year":"1973"},{"key":"S0956796825000061_ref2","unstructured":"Bloch, J. (2006) Extra, extra \u2014 read all about it: Nearly all binary searches and mergesorts are broken."}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796825000061","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,3]],"date-time":"2025-04-03T09:33:18Z","timestamp":1743672798000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796825000061\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"references-count":6,"alternative-id":["S0956796825000061"],"URL":"https:\/\/doi.org\/10.1017\/s0956796825000061","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"\u00a9 The Author(s), 2025. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (https:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}],"article-number":"e10"}}