{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:05:56Z","timestamp":1779836756575,"version":"3.53.1"},"reference-count":8,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2021,11,4]],"date-time":"2021-11-04T00:00:00Z","timestamp":1635984000000},"content-version":"unspecified","delay-in-days":307,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Consider the following puzzle: given a number, remove\n                    <jats:italic>k<\/jats:italic>\n                    digits such that the resulting number is as large as possible. Various techniques are employed to derive a linear-time solution to the puzzle: we justify the structure of a greedy algorithm by predicate logic, give a constructive proof of the greedy condition using a dependently typed proof assistant and calculate the greedy step as well as the final, linear-time optimisation by equational reasoning.\n                  <\/jats:p>","DOI":"10.1017\/s0956796821000198","type":"journal-article","created":{"date-parts":[[2021,11,4]],"date-time":"2021-11-04T04:33:27Z","timestamp":1636000407000},"update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":1,"title":["A greedy algorithm for dropping digits"],"prefix":"10.1017","volume":"31","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3901-742X","authenticated-orcid":false,"given":"RICHARD","family":"BIRD","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4755-601X","authenticated-orcid":false,"given":"SHIN-CHENG","family":"MU","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2021,11,4]]},"reference":[{"key":"S0956796821000198_ref3","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2003.09.001"},{"key":"S0956796821000198_ref6","unstructured":"Lawler, E. L. (1976) Combinatorial Optimization: Networks and Matroids. Holt, Rinehart, and Winston."},{"key":"S0956796821000198_ref4","doi-asserted-by":"publisher","DOI":"10.1080\/00029890.1974.11993624"},{"key":"S0956796821000198_ref2","volume-title":"Introduction to Algorithms","author":"Cormen","year":"2001"},{"key":"S0956796821000198_ref8","doi-asserted-by":"publisher","DOI":"10.1145\/1481861.1481862"},{"key":"S0956796821000198_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-58191-5"},{"key":"S0956796821000198_ref1","volume-title":"International Series in Computer Science","author":"Bird","year":"1997"},{"key":"S0956796821000198_ref7","unstructured":"LeetCode. (2016) 402. Remove k digits. https:\/\/leetcode.com\/problems\/remove-k-digits\/."}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796821000198","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:36:57Z","timestamp":1779835017000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796821000198\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"references-count":8,"alternative-id":["S0956796821000198"],"URL":"https:\/\/doi.org\/10.1017\/s0956796821000198","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"\u00a9 The Author(s), 2021. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}}],"article-number":"e29"}}