The automated proof of a trace transformation for a bitonic sort (Q1822503)

In his third volume of The Art of Computer Programming (1973; Zbl 0302.68010), \textit{D. E. Knuth} presents Batcher's bitonic sorting network. With concurrency, this sorting network can be executed in logarithmic time. Knuth suggests a formal argument for the correctness of the bitonic sorting algorithm (as an exercise), but addresses the question of concurrency only informally. We develop a program for the bitonic sort by (1) deriving a stepwise refinement from Knuth's informal description of the algorithm, (2) deriving from the refinement a sequential execution or 'trace' of order O(n log n) in the length n of the sequence to be sorted, and (3) transforming the sequential trace into a parallel trace of order O(log n) while preserving its semantics. We shall be informal in Steps 1 and 2 - although these steps can be formalized. But we will provide a formal treatment of Step 3 and report on the certification of this treatment in a mechanized logic. This work is a contribution to the optimization of programs (via concurrency) through transformation and the automation of program proofs.