Authors: Ana Bove, Thierry Coquand
Title: Formalising Bitonic Sort
Abstract: 
Bitonic sort (Batcher, 1968) is one of the fastest sorting networks. A
sorting network is a sorting algorithm performing only
comparison-and-swap operation on its data. This makes sorting
networks, and in particular bitonic sort, very suitable for
implementation in hardware or in parallel processor arrays.
                                                                                
Although the algorithm is short and computationally simple, its
correctness proof is not very intuitive. In addition, previous formal
proofs of the correctness of this algorithm needed to consider around
50 different cases.
                                                                                
In this talk we show how basic notions of distributive lattices help
in specifying and proving the correctness of bitonic sort.