Programming and Theorem Proving

The following links contain the implementation of orderedness related algorithms in ATS with correctness proof.
  1. ATS source code for merge sort:
  2. ATS source code for quick sort:
  3. ATS source code for heap operation:

For illustration of this methodology of combining programming with theorem proving, please refer to the following paper:

Zhiqiang Ren and Hongwei Xi, A Programmer-Centric Approach to Program Verification in ATS, Automated Reasoning in Security and Software Verification (a workshop with CADE24), Lake Placid, New York, June 9, 2013. (bibtex) (pdf) (ps)