Certification of Bilateral Patience Sort in Theorema and Rocq

Isabela Drǎmnesc, Tudor Jebelean, Sorin Stratulat

This is a case study on a specific version of the Patience Sort algorithm in which we illustrate the evolution of it from an intuitive but inefficient nested recursion into a more…