Abstract Consider the following puzzle: given a number, remove k 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.

@article{paperbot1225,
  title = {A greedy algorithm for dropping digits},
  author = {RICHARD BIRD and SHIN-CHENG MU},
  journal = {Journal of Functional Programming},
  volume = {31},
  year = {2021},
  doi = {10.1017/s0956796821000198}
}